* Overture.ma half completed up to truncations.
* PathGroupoids.ma is next and should depend only on
the part of Overture that has been ported.
--- /dev/null
+include "types.ma".
+
+(* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
+
+definition relation ≝ λA : Type[0]. A → A → Type[0].
+
+record Reflexive (A) (R : relation A) : Type[0] ≝ {
+ reflexivity : ∀x : A. R x x
+}.
+
+record Symmetric (A) (R : relation A) : Type[0] ≝ {
+ symmetry : ∀x,y. R x y → R y x
+}.
+
+record Transitive (A) (R : relation A) : Type[0] ≝ {
+ transitivity : ∀x,y,z. R x y → R y z → R x z
+}.
+
+(*Tactic Notation "etransitivity" open_constr(y) :=
+ let R := match goal with |- ?R ?x ?z => constr:(R) end in
+ let x := match goal with |- ?R ?x ?z => constr:(x) end in
+ let z := match goal with |- ?R ?x ?z => constr:(z) end in
+ refine (@transitivity _ R _ x y z _ _).*)
+
+(*Tactic Notation "etransitivity" := etransitivity _.*)
+
+(* * We would like to redefine [symmetry], which is too smart for its own good, as follows:
+
+<<
+Ltac symmetry := refine (@symmetry _ _ _ _ _ _).
+>>
+
+But this gives "Error: in Tacinterp.add_tacdef: Reserved Ltac name symmetry.". This might be fixed with https://coq.inria.fr/bugs/show_bug.cgi?id=3113. For now, you can [apply symmetry] or [eapply symmetry]. (Note that we can get around this error message by using [Tactic Notation "symmetry"], but, confusingly, this tactic notation never gets called. *)
+
+(* * ** Basic definitions *)
+
+(*CSC: was a Notation in Coq *)
+definition idmap : ∀A:Type[0]. A → A ≝ λA,x.x.
+
+(* * Composition of functions. *)
+definition compose ≝ λA,B,C: Type[0]. λg : B → C. λf : A → B.
+ λx. g (f x).
+
+interpretation "compose" 'compose g f = (compose ??? g f).
+
+(* * ** The groupoid structure of identity types. *)
+
+(* * The results in this file are used everywhere else, so we need to be extra
+ careful about how we define and prove things. We prefer hand-written terms,
+ or at least tactics that allow us to retain clear control over the
+ proof-term produced. *)
+
+(* * We define our own identity type, rather than using the one in the Coq
+ standard library, so as to have more control over transitivity, symmetry
+ and inverse. It seems impossible to change these for the standard
+ eq/identity type (or its Type-valued version) because it breaks various
+ other standard things. Merely changing notations also doesn't seem to
+ quite work. *)
+inductive paths (A : Type[0]) (a : A) : A → Type[0] ≝
+ idpath : paths A a a.
+
+interpretation "paths" 'eq t a b = (paths t a b).
+
+(*CSC: MANCANO GLI HINT *)
+definition reflexive_paths: ∀A:Type[0]. Reflexive … (paths A) ≝
+ λA. mk_Reflexive … (idpath A).
+
+(* * We define equality concatenation by destructing on both its arguments, so
+ that it only computes when both arguments are [idpath]. This makes proofs
+ more robust and symmetrical. Compare with the definition of [identity_trans]. *)
+
+definition concat : ∀A : Type[0]. ∀x,y,z: A. x = y → y = z → x = z.
+ #A #x #y #z #p #q cases q cases p %
+qed.
+
+(*CSC: MANCANO GLI HINT *)
+definition transitive_paths: ∀A:Type[0]. Transitive … (paths A) ≝
+ λA.mk_Transitive … (concat A).
+
+(* * The inverse of a path. *)
+definition inverse : ∀A : Type[0]. ∀x,y : A. x = y → y = x.
+ #A #x #y * %
+qed.
+
+(*CSC: MANCANO GLI HINT *)
+definition symmetric_paths: ∀A:Type[0]. Symmetric … (paths A) ≝
+ λA. mk_Symmetric … (inverse A).
+
+(* * Note that you can use the built-in Coq tactics [reflexivity] and [transitivity]
+ when working with paths, but not [symmetry], because it is too smart for its
+ own good. Instead, you can write [apply symmetry] or [eapply symmetry]. *)
+
+(* * The identity path. *)
+interpretation "idpath" 'idpath = (idpath ??).
+
+interpretation "concat" 'append g f = (concat ???? g f).
+
+interpretation "inverse" 'invert p = (inverse ??? p).
+
+(* * An important instance of [paths_rect] is that given any dependent type, one
+ can _transport_ elements of instances of the type along equalities in the base.
+
+ [transport P p u] transports [u : P x] to [P y] along [p : x = y]. *)
+definition transport: ∀A : Type[0]. ∀P: A → Type[0]. ∀x,y : A. x=y → P x → P y.
+ #A #P #x #y * //
+qed.
+
+(* * Transport is very common so it is worth introducing a parsing notation for it.
+ However, we do not use the notation for output because it hides the fibration,
+ and so makes it very hard to read involved transport expression.*)
+
+interpretation "transport" 'transport F p x = (transport ? F ?? p x).
+
+(* * Having defined transport, we can use it to talk about what a homotopy
+ theorist might see as "paths in a fibration over paths in the base"; and what
+ a type theorist might see as "heterogeneous eqality in a dependent type".
+
+ We will first see this appearing in the type of [apD]. *)
+
+(* * Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A],
+ then [ap f p : f x = f y].
+
+ We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)
+
+definition ap: ∀A,B: Type[0]. ∀f:A → B. ∀x,y: A. x = y → f x = f y.
+ #A #B #f #x #y * %
+qed.
+
+(* * We introduce the convention that [apKN] denotes the application of a K-path
+ between functions to an N-path between elements, where a 0-path is simply a
+ function or an element. Thus, [ap] is a shorthand for [ap01]. *)
+(*CSC: WAS A NOTATION *)
+definition ap01 := ap.
+
+definition pointwise_paths:
+ ∀A:Type[0]. ∀P:A → Type[0]. ∀f,g: ∀x:A. P x. Type[0] ≝
+ λA,P,f,g. ∀x. f x = g x.
+
+interpretation "pointwise_paths" 'congruent f g T = (pointwise_paths ? T f g).
+
+definition apD10: ∀A:Type[0]. ∀B:A→Type[0]. ∀f,g: ∀x. B x. f = g → f ≅ g.
+ #A #B #f #g * #x %
+qed.
+
+definition ap10: ∀A,B: Type[0]. ∀f,g:A → B. f=g → f ≅ g ≝
+ λA,B,f. apD10 … f.
+
+definition ap11: ∀A,B: Type[0]. ∀f,g: A → B. f=g → ∀x,y:A. x=y → f x = g y.
+ #A #B #f #g * #x #y * %
+qed.
+
+(* * Similarly, dependent functions act on paths; but the type is a bit more
+ subtle. If [f : forall a:A, B a] and [p : x = y] is a path in [A], then
+ [apD f p] should somehow be a path between [f x : B x] and [f y : B y].
+ Since these live in different types, we use transport along [p] to make them
+ comparable: [apD f p : p # f x = f y].
+
+ The type [p # f x = f y] can profitably be considered as a heterogeneous or
+ dependent equality type, of "paths from [f x] to [f y] over [p]". *)
+
+definition apD:
+ ∀A:Type[0]. ∀B:A → Type[0]. ∀f:∀a:A. B a. ∀x,y:A.
+ ∀p:x=y. p # (f x) = f y.
+ #A #B #f #x #y * %
+qed.
+
+(* * ** Equivalences *)
+
+(* * Homotopy equivalences are a central concept in homotopy type theory.
+ Before we define equivalences, let us consider when two types [A] and [B]
+ should be considered "the same".
+
+ The first option is to require existence of [f : A -> B] and [g : B -> A]
+ which are inverses of each other, up to homotopy. Homotopically speaking, we
+ should also require a certain condition on these homotopies, which is one of
+ the triangle identities for adjunctions in category theory. Thus, we call
+ this notion an *adjoint equivalence*.
+
+ The other triangle identity is provable from the first one, along with all the
+ higher coherences, so it is reasonable to only assume one of them. Moreover,
+ as we will see, if we have maps which are inverses up to homotopy, it is always
+ possible to make the triangle identity hold by modifying one of the homotopies.
+
+ The second option is to use Vladimir Voevodsky's definition of an equivalence
+ as a map whose homotopy fibers are contractible. We call this notion a
+ *homotopy bijection*.
+
+ An interesting third option was suggested by André Joyal: a map [f] which has
+ separate left and right homotopy inverses. We call this notion a
+ *homotopy isomorphism*.
+
+ While the second option was the one used originally, and it is the most
+ concise one, it makes more sense to use the first one in a formalized
+ development, since it exposes most directly equivalence as a structure.
+ In particular, it is easier to extract directly from it the data of a homotopy
+ inverse to [f], which is what we care about having most in practice. Thus,
+ adjoint equivalences are what we will refer to merely as *equivalences*. *)
+
+(* * Naming convention: we use [equiv] and [Equiv] systematically to denote types
+ of equivalences, and [isequiv] and [IsEquiv] systematically to denote the
+ assertion that a given map is an equivalence. *)
+
+(* * The fact that [r] is a left inverse of [s]. As a mnemonic, note that the
+ partially applied type [Sect s] is the type of proofs that [s] is a section. *)
+definition Sect: ∀A,B : Type[0]. (A → B) → (B → A) → Type[0] ≝
+ λA,B,s,r. ∀x : A. r (s x) = x.
+
+(* * A typeclass that includes the data making [f] into an adjoint equivalence. *)
+record IsEquiv (A,B : Type[0]) (f : A → B) : Type[0] ≝ {
+ equiv_inv : B → A ;
+ eisretr : Sect … equiv_inv f;
+ eissect : Sect … f equiv_inv;
+ eisadj : ∀x:A. eisretr (f x) = (* f (equiv_inv (f x)) = f x *) ap … f … (eissect x)
+}.
+
+(* * A record that includes all the data of an adjoint equivalence. *)
+record Equiv (A,B) : Type[0] ≝ {
+ equiv_fun :1> A → B ;
+ equiv_isequiv :> IsEquiv … equiv_fun
+}.
+
+interpretation "Equiv" 'equiv A B p = (Equiv A B).
+
+(* * A notation for the inverse of an equivalence. We can apply this to a
+ function as long as there is a typeclass instance asserting it to be an
+ equivalence. We can also apply it to an element of [A <~> B], since there is
+ an implicit coercion to [A -> B] and also an existing instance of [IsEquiv]. *)
+
+(*CSC: PROBABLY WE NEED TO INTERPRET 'invert_appl TOO *)
+interpretation "equiv_inv" 'invert f = (equiv_inv ?? f ?).
+
+(*
+(** ** Contractibility and truncation levels *)
+
+(** Truncation measures how complicated a type is. In this library, a witness that a type is n-truncated is formalized by the [IsTrunc n] typeclass. In many cases, the typeclass machinery of Coq can automatically infer a witness for a type being n-truncated. Because [IsTrunc n A] itself has no computational content (that is, all witnesses of n-truncation of a type are provably equal), it does not matter much which witness Coq infers. Therefore, the primary concerns in making use of the typeclass machinery are coverage (how many goals can be automatically solved) and speed (how long does it take to solve a goal, and how long does it take to error on a goal we cannot automatically solve). Careful use of typeclass instances and priorities, which determine the order of typeclass resolution, can be used to effectively increase both the coverage and the speed in cases where the goal is solvable. Unfortunately, typeclass resolution tends to spin for a while before failing unless you're very, very, very careful. We currently aim to achieve moderate coverage and fast speed in solvable cases. How long it takes to fail typeclass resolution is not currently considered, though it would be nice someday to be even more careful about things.
+
+In order to achieve moderate coverage and speedy resolution, we currently follow the following principles. They set up a kind of directed flow of information, intended to prevent cycles and potentially infinite chains, which are often the ways that typeclass resolution gets stuck.
+
+- We prefer to reason about [IsTrunc (S n) A] rather than [IsTrunc n (@paths A a b)]. Whenever we see a statement (or goal) about truncation of paths, we try to turn it into a statement (or goal) about truncation of a (non-[paths]) type. We do not allow typeclass resolution to go in the reverse direction from [IsTrunc (S n) A] to [forall a b : A, IsTrunc n (a = b)].
+
+- We prefer to reason about syntactically smaller types. That is, typeclass instances should turn goals of type [IsTrunc n (forall a : A, P a)] into goals of type [forall a : A, IsTrunc n (P a)]; and goals of type [IsTrunc n (A * B)] into the pair of goals of type [IsTrunc n A] and [IsTrunc n B]; rather than the other way around. Ideally, we would add similar rules to transform hypotheses in the cases where we can do so. This rule is not always the one we want, but it seems to heuristically capture the shape of most cases that we want the typeclass machinery to automatically infer. That is, we often want to infer [IsTrunc n (A * B)] from [IsTrunc n A] and [IsTrunc n B], but we (probably) don't often need to do other simple things with [IsTrunc n (A * B)] which are broken by that reduction.
+*)
+
+(** *** Contractibility *)
+
+(** A space [A] is contractible if there is a point [x : A] and a (pointwise) homotopy connecting the identity on [A] to the constant map at [x]. Thus an element of [contr A] is a pair whose first component is a point [x] and the second component is a pointwise retraction of [A] to [x]. *)
+
+(** We use the [Contr_internal] record so as not to pollute typeclass search; we only do truncation typeclass search on the [IsTrunc] datatype, usually. We will define a notation [Contr] which is equivalent to [Contr_internal], but picked up by typeclass search. However, we must make [Contr_internal] a class so that we pick up typeclasses on [center] and [contr]. However, the only typeclass rule we register is the one that turns it into a [Contr]/[IsTrunc]. Unfortunately, this means that declaring an instance like [Instance contr_foo : Contr foo := { center := bar }.] will fail with mismatched instances/contexts. Instead, we must iota expand such definitions to get around Coq's deficiencies, and write [Instance contr_foo : Contr foo := let x := {| center := bar |} in x.] *)
+Class Contr_internal (A : Type) := BuildContr {
+ center : A ;
+ contr : (forall y : A, center = y)
+}.
+
+Arguments center A {_}.
+
+(** *** Truncation levels *)
+
+(** Truncation measures how complicated a type is in terms of higher path spaces. The (-2)-truncated types are the contractible ones, whose homotopy is completely trivial. The (n+1)-truncated types are those whose path spaces are n-truncated.
+
+ Thus, (-1)-truncated means "the space of paths between any two points is contactible". Such a space is necessarily a sub-singleton: any two points are connected by a path which is unique up to homotopy. In other words, (-1)-truncated spaces are truth values (we call them "propositions").
+
+ Next, 0-truncated means "the space of paths between any two points is a sub-singleton". Thus, two points might not have any paths between them, or they have a unique path. Such a space may have many points but it is discrete in the sense that all paths are trivial. We call such spaces "sets".
+*)
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+(** We will use [Notation] for [trunc_index]es, so define a scope for them here. *)
+Delimit Scope trunc_scope with trunc.
+Bind Scope trunc_scope with trunc_index.
+Arguments trunc_S _%trunc_scope.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+ := match n with
+ | 0 => trunc_S (trunc_S minus_two)
+ | S n' => trunc_S (nat_to_trunc_index n')
+ end.
+
+Coercion nat_to_trunc_index : nat >-> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+ match n with
+ | minus_two => Contr_internal A
+ | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+ end.
+
+Notation minus_one:=(trunc_S minus_two).
+(** Include the basic numerals, so we don't need to go through the coercion from [nat], and so that we get the right binding with [trunc_scope]. *)
+Notation "0" := (trunc_S minus_one) : trunc_scope.
+Notation "1" := (trunc_S 0) : trunc_scope.
+Notation "2" := (trunc_S 1) : trunc_scope.
+
+Arguments IsTrunc_internal n A : simpl nomatch.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+ Trunc_is_trunc : IsTrunc_internal n A.
+
+(** We use the priciple that we should always be doing typeclass resolution on truncation of non-equality types. We try to change the hypotheses and goals so that they never mention something like [IsTrunc n (_ = _)] and instead say [IsTrunc (S n) _]. If you're evil enough that some of your paths [a = b] are n-truncated, but others are not, then you'll have to either reason manually or add some (local) hints with higher priority than the hint below, or generalize your equality type so that it's not a path anymore. *)
+
+Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
+
+Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
+
+Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
+: IsTrunc n (x = y)
+ := H x y. (* but do fold [IsTrunc] *)
+
+Hint Extern 0 => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
+
+(** Picking up the [forall x y, IsTrunc n (x = y)] instances in the hypotheses is much tricker. We could do something evil where we declare an empty typeclass like [IsTruncSimplification] and use the typeclass as a proxy for allowing typeclass machinery to factor nested [forall]s into the [IsTrunc] via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases. It should be clear how to extend the pattern. *)
+Hint Extern 10 =>
+progress match goal with
+ | [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ]
+ => change (IsTrunc (trunc_S n) T) in H
+ | [ H : forall (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]
+ => change (forall a : A, IsTrunc (trunc_S n) (T a)) in H; cbv beta in H
+ | [ H : forall (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]
+ => change (forall (a : A) (b : B a), IsTrunc (trunc_S n) (T a b)) in H; cbv beta in H
+ | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]
+ => change (forall (a : A) (b : B a) (c : C a b), IsTrunc (trunc_S n) (T a b c)) in H; cbv beta in H
+ | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (d : @?D a b c) (x y : @?T a b c d), IsTrunc ?n (x = y) |- _ ]
+ => change (forall (a : A) (b : B a) (c : C a b) (d : D a b c), IsTrunc (trunc_S n) (T a b c d)) in H; cbv beta in H
+ end.
+
+Notation Contr := (IsTrunc minus_two).
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+
+Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+
+(** *** Function extensionality *)
+
+(** The function extensionality axiom is formulated as a class. To use it in a theorem, just assume it with [`{Funext}], and then you can use [path_forall], defined below. If you need function extensionality for a whole development, you can assume it for an entire Section with [Context `{Funext}]. *)
+Class Funext :=
+ { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
+ f == g -> f = g
+ :=
+ (@apD10 A P f g)^-1.
+
+Definition path_forall2 `{Funext} {A B : Type} {P : A -> B -> Type} (f g : forall x y, P x y) :
+ (forall x y, f x y = g x y) -> f = g
+ :=
+ (fun E => path_forall f g (fun x => path_forall (f x) (g x) (E x))).
+
+
+(** *** Tactics *)
+
+(** We declare some more [Hint Resolve] hints, now in the "hint database" [path_hints]. In general various hints (resolve, rewrite, unfold hints) can be grouped into "databases". This is necessary as sometimes different kinds of hints cannot be mixed, for example because they would cause a combinatorial explosion or rewriting cycles.
+
+ A specific [Hint Resolve] database [db] can be used with [auto with db].
+
+ The hints in [path_hints] are designed to push concatenation *outwards*, eliminate identities and inverses, and associate to the left as far as possible. *)
+
+(** TODO: think more carefully about this. Perhaps associating to the right would be more convenient? *)
+Hint Resolve
+ @idpath @inverse
+ : path_hints.
+
+Hint Resolve @idpath : core.
+
+Ltac path_via mid :=
+ apply @concat with (y := mid); auto with path_hints.
+
+(** We put [Empty] here, instead of in [Empty.v], because [Ltac done] uses it. *)
+Inductive Empty : Type := .
+
+Definition not (A:Type) : Type := A -> Empty.
+Notation "~ x" := (not x) : type_scope.
+Hint Unfold not: core.
+
+(** *** Pointed types *)
+
+(** A space is pointed if that space has a point. *)
+Class IsPointed (A : Type) := point : A.
+Definition pointedType := { u : Type & IsPointed u }.
+
+(** Ssreflect tactics, adapted by Robbert Krebbers *)
+Ltac done :=
+ trivial; intros; solve
+ [ repeat first
+ [ solve [trivial]
+ | solve [eapply symmetry; trivial]
+ | reflexivity
+ (* Discriminate should be here, but it doesn't work yet *)
+ (* | discriminate *)
+ | contradiction
+ | split ]
+ | match goal with
+ H : ~ _ |- _ => solve [destruct H; trivial]
+ end ].
+Tactic Notation "by" tactic(tac) :=
+ tac; done.
+
+(** A convenient tactic for using function extensionality. *)
+Ltac by_extensionality x :=
+ intros; unfold compose;
+ match goal with
+ | [ |- ?f = ?g ] => eapply path_forall; intro x;
+ match goal with
+ | [ |- forall (_ : prod _ _), _ ] => intros [? ?]
+ | [ |- forall (_ : sigT _ _), _ ] => intros [? ?]
+ | _ => intros
+ end;
+ simpl; auto with path_hints
+ end.
+
+(** Removed auto. We can write "by (path_induction;auto with path_hints)"
+ if we want to.*)
+Ltac path_induction :=
+ intros; repeat progress (
+ match goal with
+ | [ p : _ = _ |- _ ] => induction p
+ | _ => idtac
+ end
+ ).
+
+(** The tactic [f_ap] is a replacement for the previously existing standard library tactic [f_equal]. This tactic works by repeatedly applying the fact that [f = g -> x = y -> f x = g y] to turn, e.g., [f x y = f z w] first into [f x = f z] and [y = w], and then turns the first of these into [f = f] and [x = z]. The [done] tactic is used to detect the [f = f] case and finish, and the [trivial] is used to solve, e.g., [x = x] when using [f_ap] on [f y x = f z x]. This tactic only works for non-dependently-typed functions; we cannot express [y = w] in the first example if [y] and [w] have different types. If and when Arnaud's new-tacticals branch lands, and we can have a goal which depends on the term used to discharge another goal, then this tactic should probably be generalized to deal with dependent functions. *)
+Ltac f_ap :=
+ lazymatch goal with
+ | [ |- ?f ?x = ?g ?x ] => apply (@apD10 _ _ f g);
+ try (done || f_ap)
+ | _ => apply ap11;
+ [ done || f_ap
+ | trivial ]
+ end.
+
+(** [expand] replaces both terms of an equality (either [paths] or [pointwise_paths] in the goal with their head normal forms *)
+Ltac expand :=
+ match goal with
+ | [ |- ?X = ?Y ] =>
+ let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')
+ | [ |- ?X == ?Y ] =>
+ let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')
+ end; simpl.
+
+(** [atomic x] is the same as [idtac] if [x] is a variable or hypothesis, but is [fail 0] if [x] has internal structure. *)
+Ltac atomic x :=
+ match x with
+ | ?f _ => fail 1 x "is not atomic"
+ | (fun _ => _) => fail 1 x "is not atomic"
+ | forall _, _ => fail 1 x "is not atomic"
+ | _ => idtac
+ end.
+*)
\ No newline at end of file
--- /dev/null
+(*
+(** * The groupid structure of paths *)
+
+Require Import Overture.
+
+Local Open Scope path_scope.
+
+(** ** Naming conventions
+
+ We need good naming conventions that allow us to name theorems without looking them up. The names should indicate the structure of the theorem, but they may sometimes be ambiguous, in which case you just have to know what is going on. We shall adopt the following principles:
+
+ - we are not afraid of long names
+ - we are not afraid of short names when they are used frequently
+ - we use underscores
+ - name of theorems and lemmas are lower-case
+ - records and other types may be upper or lower case
+
+ Theorems about concatenation of paths are called [concat_XXX] where [XXX] tells us what is on the left-hand side of the equation. You have to guess the right-hand side. We use the following symbols in [XXX]:
+
+ - [1] means the identity path
+ - [p] means 'the path'
+ - [V] means 'the inverse path'
+ - [A] means '[ap]'
+ - [M] means the thing we are moving across equality
+ - [x] means 'the point' which is not a path, e.g. in [transport p x]
+ - [2] means relating to 2-dimensional paths
+ - [3] means relating to 3-dimensional paths, and so on
+
+ Associativity is indicated with an underscore. Here are some examples of how the name gives hints about the left-hand side of the equation.
+
+ - [concat_1p] means [1 * p]
+ - [concat_Vp] means [p^ * p]
+ - [concat_p_pp] means [p * (q * r)]
+ - [concat_pp_p] means [(p * q) * r]
+ - [concat_V_pp] means [p^ * (p * q)]
+ - [concat_pV_p] means [(q * p^) * p] or [(p * p^) * q], but probably the former because for the latter you could just use [concat_pV].
+
+ Laws about inverse of something are of the form [inv_XXX], and those about [ap] are of the form [ap_XXX], and so on. For example:
+
+ - [inv_pp] is about [(p @ q)^]
+ - [inv_V] is about [(p^)^]
+ - [inv_A] is about [(ap f p)^]
+ - [ap_V] is about [ap f (p^)]
+ - [ap_pp] is about [ap f (p @ q)]
+ - [ap_idmap] is about [ap idmap p]
+ - [ap_1] is about [ap f 1]
+ - [ap02_p2p] is about [ap02 f (p @@ q)]
+
+ Then we have laws which move things around in an equation. The naming scheme here is [moveD_XXX]. The direction [D] indicates where to move to: [L] means that we move something to the left-hand side, whereas [R] means we are moving something to the right-hand side. The part [XXX] describes the shape of the side _from_ which we are moving where the thing that is getting moves is called [M]. The presence of 1 next to an [M] generally indicates an *implied* identity path which is inserted automatically after the movement. Examples:
+
+ - [moveL_pM] means that we transform [p = q @ r] to [p @ r^ = q]
+ because we are moving something to the left-hand side, and we are
+ moving the right argument of concat.
+
+ - [moveR_Mp] means that we transform [p @ q = r] to [q = p^ @ r]
+ because we move to the right-hand side, and we are moving the left
+ argument of concat.
+
+ - [moveR_1M] means that we transform [p = q] (rather than [p = 1 @ q]) to [p * q^ = 1].
+
+ There are also cancellation laws called [cancelR] and [cancelL], which are inverse to the 2-dimensional 'whiskering' operations [whiskerR] and [whiskerL].
+
+ We may now proceed with the groupoid structure proper.
+*)
+
+(** ** The 1-dimensional groupoid structure. *)
+
+(** The identity path is a right unit. *)
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+ p @ 1 = p
+ :=
+ match p with idpath => 1 end.
+
+(** The identity is a left unit. *)
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+ 1 @ p = p
+ :=
+ match p with idpath => 1 end.
+
+(** Concatenation is associative. *)
+Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+ p @ (q @ r) = (p @ q) @ r :=
+ match r with idpath =>
+ match q with idpath =>
+ match p with idpath => 1
+ end end end.
+
+Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+ (p @ q) @ r = p @ (q @ r) :=
+ match r with idpath =>
+ match q with idpath =>
+ match p with idpath => 1
+ end end end.
+
+(** The left inverse law. *)
+Definition concat_pV {A : Type} {x y : A} (p : x = y) :
+ p @ p^ = 1
+ :=
+ match p with idpath => 1 end.
+
+(** The right inverse law. *)
+Definition concat_Vp {A : Type} {x y : A} (p : x = y) :
+ p^ @ p = 1
+ :=
+ match p with idpath => 1 end.
+
+(** Several auxiliary theorems about canceling inverses across associativity. These are somewhat redundant, following from earlier theorems. *)
+
+Definition concat_V_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
+ p^ @ (p @ q) = q
+ :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition concat_p_Vp {A : Type} {x y z : A} (p : x = y) (q : x = z) :
+ p @ (p^ @ q) = q
+ :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition concat_pp_V {A : Type} {x y z : A} (p : x = y) (q : y = z) :
+ (p @ q) @ q^ = p
+ :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) :
+ (p @ q^) @ q = p
+ :=
+ (match q as i return forall p, (p @ i^) @ i = p with
+ idpath =>
+ fun p =>
+ match p with idpath => 1 end
+ end) p.
+
+(** Inverse distributes over concatenation *)
+Definition inv_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
+ (p @ q)^ = q^ @ p^
+ :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition inv_Vp {A : Type} {x y z : A} (p : y = x) (q : y = z) :
+ (p^ @ q)^ = q^ @ p
+ :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition inv_pV {A : Type} {x y z : A} (p : x = y) (q : z = y) :
+ (p @ q^)^ = q @ p^.
+Proof.
+ destruct p. destruct q. reflexivity.
+Defined.
+
+Definition inv_VV {A : Type} {x y z : A} (p : y = x) (q : z = y) :
+ (p^ @ q^)^ = q @ p.
+Proof.
+ destruct p. destruct q. reflexivity.
+Defined.
+
+(** Inverse is an involution. *)
+Definition inv_V {A : Type} {x y : A} (p : x = y) :
+ p^^ = p
+ :=
+ match p with idpath => 1 end.
+
+
+(* *** Theorems for moving things around in equations. *)
+
+Definition moveR_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
+ p = r^ @ q -> r @ p = q.
+Proof.
+ destruct r.
+ intro h. exact (concat_1p _ @ h @ concat_1p _).
+Defined.
+
+Definition moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
+ r = q @ p^ -> r @ p = q.
+Proof.
+ destruct p.
+ intro h. exact (concat_p1 _ @ h @ concat_p1 _).
+Defined.
+
+Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
+ p = r @ q -> r^ @ p = q.
+Proof.
+ destruct r.
+ intro h. exact (concat_1p _ @ h @ concat_1p _).
+Defined.
+
+Definition moveR_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
+ r = q @ p -> r @ p^ = q.
+Proof.
+ destruct p.
+ intro h. exact (concat_p1 _ @ h @ concat_p1 _).
+Defined.
+
+Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
+ r^ @ q = p -> q = r @ p.
+Proof.
+ destruct r.
+ intro h. exact ((concat_1p _)^ @ h @ (concat_1p _)^).
+Defined.
+
+Definition moveL_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
+ q @ p^ = r -> q = r @ p.
+Proof.
+ destruct p.
+ intro h. exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
+Defined.
+
+Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
+ r @ q = p -> q = r^ @ p.
+Proof.
+ destruct r.
+ intro h. exact ((concat_1p _)^ @ h @ (concat_1p _)^).
+Defined.
+
+Definition moveL_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
+ q @ p = r -> q = r @ p^.
+Proof.
+ destruct p.
+ intro h. exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
+Defined.
+
+Definition moveL_1M {A : Type} {x y : A} (p q : x = y) :
+ p @ q^ = 1 -> p = q.
+Proof.
+ destruct q.
+ intro h. exact ((concat_p1 _)^ @ h).
+Defined.
+
+Definition moveL_M1 {A : Type} {x y : A} (p q : x = y) :
+ q^ @ p = 1 -> p = q.
+Proof.
+ destruct q.
+ intro h. exact ((concat_1p _)^ @ h).
+Defined.
+
+Definition moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
+ p @ q = 1 -> p = q^.
+Proof.
+ destruct q.
+ intro h. exact ((concat_p1 _)^ @ h).
+Defined.
+
+Definition moveL_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
+ q @ p = 1 -> p = q^.
+Proof.
+ destruct q.
+ intro h. exact ((concat_1p _)^ @ h).
+Defined.
+
+Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) :
+ 1 = p^ @ q -> p = q.
+Proof.
+ destruct p.
+ intro h. exact (h @ (concat_1p _)).
+Defined.
+
+Definition moveR_1M {A : Type} {x y : A} (p q : x = y) :
+ 1 = q @ p^ -> p = q.
+Proof.
+ destruct p.
+ intro h. exact (h @ (concat_p1 _)).
+Defined.
+
+Definition moveR_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
+ 1 = q @ p -> p^ = q.
+Proof.
+ destruct p.
+ intro h. exact (h @ (concat_p1 _)).
+Defined.
+
+Definition moveR_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
+ 1 = p @ q -> p^ = q.
+Proof.
+ destruct p.
+ intro h. exact (h @ (concat_1p _)).
+Defined.
+
+Definition moveR_transport_p {A : Type} (P : A -> Type) {x y : A}
+ (p : x = y) (u : P x) (v : P y)
+ : u = p^ # v -> p # u = v.
+Proof.
+ destruct p.
+ exact idmap.
+Defined.
+
+Definition moveR_transport_V {A : Type} (P : A -> Type) {x y : A}
+ (p : y = x) (u : P x) (v : P y)
+ : u = p # v -> p^ # u = v.
+Proof.
+ destruct p.
+ exact idmap.
+Defined.
+
+Definition moveL_transport_V {A : Type} (P : A -> Type) {x y : A}
+ (p : x = y) (u : P x) (v : P y)
+ : p # u = v -> u = p^ # v.
+Proof.
+ destruct p.
+ exact idmap.
+Defined.
+
+Definition moveL_transport_p {A : Type} (P : A -> Type) {x y : A}
+ (p : y = x) (u : P x) (v : P y)
+ : p^ # u = v -> u = p # v.
+Proof.
+ destruct p.
+ exact idmap.
+Defined.
+
+(** *** Functoriality of functions *)
+
+(** Here we prove that functions behave like functors between groupoids, and that [ap] itself is functorial. *)
+
+(** Functions take identity paths to identity paths. *)
+Definition ap_1 {A B : Type} (x : A) (f : A -> B) :
+ ap f 1 = 1 :> (f x = f x)
+ :=
+ 1.
+
+(** Functions commute with concatenation. *)
+Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+ ap f (p @ q) = (ap f p) @ (ap f q)
+ :=
+ match q with
+ idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition ap_p_pp {A B : Type} (f : A -> B) {w x y z : A}
+ (r : f w = f x) (p : x = y) (q : y = z) :
+ r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q).
+Proof.
+ destruct p, q. simpl. exact (concat_p_pp r 1 1).
+Defined.
+
+Definition ap_pp_p {A B : Type} (f : A -> B) {w x y z : A}
+ (p : x = y) (q : y = z) (r : f z = f w) :
+ (ap f (p @ q)) @ r = (ap f p) @ (ap f q @ r).
+Proof.
+ destruct p, q. simpl. exact (concat_pp_p 1 1 r).
+Defined.
+
+(** Functions commute with path inverses. *)
+Definition inverse_ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
+ (ap f p)^ = ap f (p^)
+ :=
+ match p with idpath => 1 end.
+
+Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
+ ap f (p^) = (ap f p)^
+ :=
+ match p with idpath => 1 end.
+
+(** [ap] itself is functorial in the first argument. *)
+
+Definition ap_idmap {A : Type} {x y : A} (p : x = y) :
+ ap idmap p = p
+ :=
+ match p with idpath => 1 end.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+ ap (g o f) p = ap g (ap f p)
+ :=
+ match p with idpath => 1 end.
+
+(* Sometimes we don't have the actual function [compose]. *)
+Definition ap_compose' {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+ ap (fun a => g (f a)) p = ap g (ap f p)
+ :=
+ match p with idpath => 1 end.
+
+(** The action of constant maps. *)
+Definition ap_const {A B : Type} {x y : A} (p : x = y) (z : B) :
+ ap (fun _ => z) p = 1
+ :=
+ match p with idpath => idpath end.
+
+(** Naturality of [ap]. *)
+Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) :
+ (ap f q) @ (p y) = (p x) @ (ap g q)
+ :=
+ match q with
+ | idpath => concat_1p _ @ ((concat_p1 _) ^)
+ end.
+
+(** Naturality of [ap] at identity. *)
+Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
+ (ap f q) @ (p y) = (p x) @ q
+ :=
+ match q with
+ | idpath => concat_1p _ @ ((concat_p1 _) ^)
+ end.
+
+Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A} (q : x = y) :
+ (p x) @ (ap f q) = q @ (p y)
+ :=
+ match q as i in (_ = y) return (p x @ ap f i = i @ p y) with
+ | idpath => concat_p1 _ @ (concat_1p _)^
+ end.
+
+(** Naturality with other paths hanging around. *)
+Definition concat_pA_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
+ {x y : A} (q : x = y)
+ {w z : B} (r : w = f x) (s : g y = z)
+ :
+ (r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s).
+Proof.
+ destruct q, s; simpl.
+ repeat rewrite concat_p1.
+ reflexivity.
+Defined.
+
+Definition concat_pA_p {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
+ {x y : A} (q : x = y)
+ {w : B} (r : w = f x)
+ :
+ (r @ ap f q) @ p y = (r @ p x) @ ap g q.
+Proof.
+ destruct q; simpl.
+ repeat rewrite concat_p1.
+ reflexivity.
+Defined.
+
+Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
+ {x y : A} (q : x = y)
+ {z : B} (s : g y = z)
+ :
+ (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).
+Proof.
+ destruct q, s; simpl.
+ repeat rewrite concat_p1, concat_1p.
+ reflexivity.
+Defined.
+
+Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
+ {x y : A} (q : x = y)
+ {w z : A} (r : w = f x) (s : y = z)
+ :
+ (r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s).
+Proof.
+ destruct q, s; simpl.
+ repeat rewrite concat_p1.
+ reflexivity.
+Defined.
+
+Definition concat_pp_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
+ {x y : A} (q : x = y)
+ {w z : A} (r : w = x) (s : g y = z)
+ :
+ (r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s).
+Proof.
+ destruct q, s; simpl.
+ repeat rewrite concat_p1.
+ reflexivity.
+Defined.
+
+Definition concat_pA1_p {A : Type} {f : A -> A} (p : forall x, f x = x)
+ {x y : A} (q : x = y)
+ {w : A} (r : w = f x)
+ :
+ (r @ ap f q) @ p y = (r @ p x) @ q.
+Proof.
+ destruct q; simpl.
+ repeat rewrite concat_p1.
+ reflexivity.
+Defined.
+
+Definition concat_A1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
+ {x y : A} (q : x = y)
+ {z : A} (s : y = z)
+ :
+ (ap f q) @ (p y @ s) = (p x) @ (q @ s).
+Proof.
+ destruct q, s; simpl.
+ repeat rewrite concat_p1, concat_1p.
+ reflexivity.
+Defined.
+
+Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
+ {x y : A} (q : x = y)
+ {w : A} (r : w = x)
+ :
+ (r @ p x) @ ap g q = (r @ q) @ p y.
+Proof.
+ destruct q; simpl.
+ repeat rewrite concat_p1.
+ reflexivity.
+Defined.
+
+Definition concat_p_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
+ {x y : A} (q : x = y)
+ {z : A} (s : g y = z)
+ :
+ p x @ (ap g q @ s) = q @ (p y @ s).
+Proof.
+ destruct q, s; simpl.
+ repeat rewrite concat_p1, concat_1p.
+ reflexivity.
+Defined.
+
+(** *** Action of [apD10] and [ap10] on paths. *)
+
+(** Application of paths between functions preserves the groupoid structure *)
+
+Definition apD10_1 {A} {B:A->Type} (f : forall x, B x) (x:A)
+ : apD10 (idpath f) x = 1
+:= 1.
+
+Definition apD10_pp {A} {B:A->Type} {f f' f'' : forall x, B x}
+ (h:f=f') (h':f'=f'') (x:A)
+: apD10 (h @ h') x = apD10 h x @ apD10 h' x.
+Proof.
+ case h, h'; reflexivity.
+Defined.
+
+Definition apD10_V {A} {B:A->Type} {f g : forall x, B x} (h:f=g) (x:A)
+ : apD10 (h^) x = (apD10 h x)^
+:= match h with idpath => 1 end.
+
+Definition ap10_1 {A B} {f:A->B} (x:A) : ap10 (idpath f) x = 1
+ := 1.
+
+Definition ap10_pp {A B} {f f' f'':A->B} (h:f=f') (h':f'=f'') (x:A)
+ : ap10 (h @ h') x = ap10 h x @ ap10 h' x
+:= apD10_pp h h' x.
+
+Definition ap10_V {A B} {f g : A->B} (h : f = g) (x:A)
+ : ap10 (h^) x = (ap10 h x)^
+:= apD10_V h x.
+
+(** [ap10] also behaves nicely on paths produced by [ap] *)
+Lemma ap_ap10 {A B C} (f g : A -> B) (h : B -> C)
+ (p : f = g) (a : A) :
+ ap h (ap10 p a) = ap10 (ap (fun f' => h o f') p) a.
+Proof.
+ destruct p. exact 1.
+Defined.
+
+(** *** Transport and the groupoid structure of paths *)
+
+Definition transport_1 {A : Type} (P : A -> Type) {x : A} (u : P x)
+ : 1 # u = u
+:= 1.
+
+Definition transport_pp {A : Type} (P : A -> Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
+ p @ q # u = q # p # u :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition transport_pV {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P y)
+ : p # p^ # z = z
+ := (transport_pp P p^ p z)^
+ @ ap (fun r => transport P r z) (concat_Vp p).
+
+Definition transport_Vp {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P x)
+ : p^ # p # z = z
+ := (transport_pp P p p^ z)^
+ @ ap (fun r => transport P r z) (concat_pV p).
+
+(** In the future, we may expect to need some higher coherence for transport:
+ for instance, that transport acting on the associator is trivial. *)
+Definition transport_p_pp {A : Type} (P : A -> Type)
+ {x y z w : A} (p : x = y) (q : y = z) (r : z = w)
+ (u : P x)
+ : ap (fun e => e # u) (concat_p_pp p q r)
+ @ (transport_pp P (p@q) r u) @ ap (transport P r) (transport_pp P p q u)
+ = (transport_pp P p (q@r) u) @ (transport_pp P q r (p#u))
+ :> ((p @ (q @ r)) # u = r # q # p # u) .
+Proof.
+ destruct p, q, r. simpl. exact 1.
+Defined.
+
+(* Here is another coherence lemma for transport. *)
+Definition transport_pVp {A} (P : A -> Type) {x y:A} (p:x=y) (z:P x)
+ : transport_pV P p (transport P p z)
+ = ap (transport P p) (transport_Vp P p z).
+Proof.
+ destruct p; reflexivity.
+Defined.
+
+(** Dependent transport in a doubly dependent type. *)
+
+Definition transportD {A : Type} (B : A -> Type) (C : forall a:A, B a -> Type)
+ {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1 y)
+ : C x2 (p # y)
+ :=
+ match p with idpath => z end.
+
+(** Transporting along higher-dimensional paths *)
+
+Definition transport2 {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
+ (r : p = q) (z : P x)
+ : p # z = q # z
+ := ap (fun p' => p' # z) r.
+
+(** An alternative definition. *)
+Definition transport2_is_ap10 {A : Type} (Q : A -> Type) {x y : A} {p q : x = y}
+ (r : p = q) (z : Q x)
+ : transport2 Q r z = ap10 (ap (transport Q) r) z
+ := match r with idpath => 1 end.
+
+Definition transport2_p2p {A : Type} (P : A -> Type) {x y : A} {p1 p2 p3 : x = y}
+ (r1 : p1 = p2) (r2 : p2 = p3) (z : P x)
+ : transport2 P (r1 @ r2) z = transport2 P r1 z @ transport2 P r2 z.
+Proof.
+ destruct r1, r2; reflexivity.
+Defined.
+
+Definition transport2_V {A : Type} (Q : A -> Type) {x y : A} {p q : x = y}
+ (r : p = q) (z : Q x)
+ : transport2 Q (r^) z = (transport2 Q r z)^
+ := match r with idpath => 1 end.
+
+Definition concat_AT {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
+ {z w : P x} (r : p = q) (s : z = w)
+ : ap (transport P p) s @ transport2 P r w
+ = transport2 P r z @ ap (transport P q) s
+ := match r with idpath => (concat_p1 _ @ (concat_1p _)^) end.
+
+(* TODO: What should this be called? *)
+Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) :
+ f y (p # z) = (p # (f x z)).
+Proof.
+ by induction p.
+Defined.
+
+
+(** *** Transporting in particular fibrations. *)
+
+(** One frequently needs lemmas showing that transport in a certain dependent type is equal to some more explicitly defined operation, defined according to the structure of that dependent type. For most dependent types, we prove these lemmas in the appropriate file in the types/ subdirectory. Here we consider only the most basic cases. *)
+
+(** Transporting in a constant fibration. *)
+Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
+ : transport (fun x => B) p y = y.
+Proof.
+ destruct p. exact 1.
+Defined.
+
+Definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 = x2}
+ (r : p = q) (y : B)
+ : transport_const p y = transport2 (fun _ => B) r y @ transport_const q y
+ := match r with idpath => (concat_1p _)^ end.
+
+(** Transporting in a pulled back fibration. *)
+Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
+ (p : x = y) (z : P (f x))
+ : transport (fun x => P (f x)) p z = transport P (ap f p) z.
+Proof.
+ destruct p; reflexivity.
+Defined.
+
+(** A special case of [transport_compose] which seems to come up a lot. *)
+Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
+: transport P p u = transport idmap (ap P p) u
+ := match p with idpath => idpath end.
+
+(** *** The behavior of [ap] and [apD]. *)
+
+(** In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. *)
+Lemma apD_const {A B} {x y : A} (f : A -> B) (p: x = y) :
+ apD f p = transport_const p (f x) @ ap f p.
+Proof.
+ destruct p; reflexivity.
+Defined.
+
+(** ** The 2-dimensional groupoid structure *)
+
+(** Horizontal composition of 2-dimensional paths. *)
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+ : p @ q = p' @ q'
+:= match h, h' with idpath, idpath => 1 end.
+
+Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
+
+(** 2-dimensional path inversion *)
+Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
+ : p^ = q^
+:= match h with idpath => 1 end.
+
+(** *** Whiskering *)
+
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+ {q r : y = z} (h : q = r) : p @ q = p @ r
+:= 1 @@ h.
+
+Definition whiskerR {A : Type} {x y z : A} {p q : x = y}
+ (h : p = q) (r : y = z) : p @ r = q @ r
+:= h @@ 1.
+
+(** *** Unwhiskering, a.k.a. cancelling. *)
+
+Lemma cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
+ : (p @ q = p @ r) -> (q = r).
+Proof.
+ destruct p, r.
+ intro a.
+ exact ((concat_1p q)^ @ a).
+Defined.
+
+Lemma cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
+ : (p @ r = q @ r) -> (p = q).
+Proof.
+ destruct r, p.
+ intro a.
+ exact (a @ concat_p1 q).
+Defined.
+
+(** Whiskering and identity paths. *)
+
+Definition whiskerR_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
+ (concat_p1 p) ^ @ whiskerR h 1 @ concat_p1 q = h
+ :=
+ match h with idpath =>
+ match p with idpath =>
+ 1
+ end end.
+
+Definition whiskerR_1p {A : Type} {x y z : A} (p : x = y) (q : y = z) :
+ whiskerR 1 q = 1 :> (p @ q = p @ q)
+ :=
+ match q with idpath => 1 end.
+
+Definition whiskerL_p1 {A : Type} {x y z : A} (p : x = y) (q : y = z) :
+ whiskerL p 1 = 1 :> (p @ q = p @ q)
+ :=
+ match q with idpath => 1 end.
+
+Definition whiskerL_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
+ (concat_1p p) ^ @ whiskerL 1 h @ concat_1p q = h
+ :=
+ match h with idpath =>
+ match p with idpath =>
+ 1
+ end end.
+
+Definition concat2_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
+ h @@ 1 = whiskerR h 1 :> (p @ 1 = q @ 1)
+ :=
+ match h with idpath => 1 end.
+
+Definition concat2_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
+ 1 @@ h = whiskerL 1 h :> (1 @ p = 1 @ q)
+ :=
+ match h with idpath => 1 end.
+
+
+(** The interchange law for concatenation. *)
+Definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x = y} {q q' q'' : y = z}
+ (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') :
+ (a @@ c) @ (b @@ d) = (a @ b) @@ (c @ d).
+Proof.
+ case d.
+ case c.
+ case b.
+ case a.
+ reflexivity.
+Defined.
+
+(** The interchange law for whiskering. Special case of [concat_concat2]. *)
+Definition concat_whisker {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
+ (whiskerR a q) @ (whiskerL p' b) = (whiskerL p b) @ (whiskerR a q')
+ :=
+ match b with
+ idpath =>
+ match a with idpath =>
+ (concat_1p _)^
+ end
+ end.
+
+(** Structure corresponding to the coherence equations of a bicategory. *)
+
+(** The "pentagonator": the 3-cell witnessing the associativity pentagon. *)
+Definition pentagon {A : Type} {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z)
+ : whiskerL p (concat_p_pp q r s)
+ @ concat_p_pp p (q@r) s
+ @ whiskerR (concat_p_pp p q r) s
+ = concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s.
+Proof.
+ case p, q, r, s. reflexivity.
+Defined.
+
+(** The 3-cell witnessing the left unit triangle. *)
+Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z)
+ : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q
+ = whiskerL p (concat_1p q).
+Proof.
+ case p, q. reflexivity.
+Defined.
+
+(** The Eckmann-Hilton argument *)
+Definition eckmann_hilton {A : Type} {x:A} (p q : 1 = 1 :> (x = x)) : p @ q = q @ p :=
+ (whiskerR_p1 p @@ whiskerL_1p q)^
+ @ (concat_p1 _ @@ concat_p1 _)
+ @ (concat_1p _ @@ concat_1p _)
+ @ (concat_whisker _ _ _ _ p q)
+ @ (concat_1p _ @@ concat_1p _)^
+ @ (concat_p1 _ @@ concat_p1 _)^
+ @ (whiskerL_1p q @@ whiskerR_p1 p).
+
+(** The action of functions on 2-dimensional paths *)
+
+Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
+ := match r with idpath => 1 end.
+
+Definition ap02_pp {A B} (f:A->B) {x y:A} {p p' p'':x=y} (r:p=p') (r':p'=p'')
+ : ap02 f (r @ r') = ap02 f r @ ap02 f r'.
+Proof.
+ case r, r'; reflexivity.
+Defined.
+
+Definition ap02_p2p {A B} (f:A->B) {x y z:A} {p p':x=y} {q q':y=z} (r:p=p') (s:q=q')
+ : ap02 f (r @@ s) = ap_pp f p q
+ @ (ap02 f r @@ ap02 f s)
+ @ (ap_pp f p' q')^.
+Proof.
+ case r, s, p, q. reflexivity.
+Defined.
+
+Definition apD02 {A : Type} {B : A -> Type} {x y : A} {p q : x = y}
+ (f : forall x, B x) (r : p = q)
+ : apD f p = transport2 B r (f x) @ apD f q
+ := match r with idpath => (concat_1p _)^ end.
+
+(* And now for a lemma whose statement is much longer than its proof. *)
+Definition apD02_pp {A} (B : A -> Type) (f : forall x:A, B x) {x y : A}
+ {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3)
+ : apD02 f (r1 @ r2)
+ = apD02 f r1
+ @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
+ @ concat_p_pp _ _ _
+ @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)).
+Proof.
+ destruct r1, r2. destruct p1. reflexivity.
+Defined.
+
+(** ** Tactics, hints, and aliases *)
+
+(** [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. Given as a notation not a definition so that the resultant terms are literally instances of [concat], with no unfolding required. *)
+Notation concatR := (fun p q => concat q p).
+
+Hint Resolve
+ concat_1p concat_p1 concat_p_pp
+ inv_pp inv_V
+ : path_hints.
+
+(* First try at a paths db
+We want the RHS of the equation to become strictly simpler *)
+Hint Rewrite
+@concat_p1
+@concat_1p
+@concat_p_pp (* there is a choice here !*)
+@concat_pV
+@concat_Vp
+@concat_V_pp
+@concat_p_Vp
+@concat_pp_V
+@concat_pV_p
+(*@inv_pp*) (* I am not sure about this one *)
+@inv_V
+@moveR_Mp
+@moveR_pM
+@moveL_Mp
+@moveL_pM
+@moveL_1M
+@moveL_M1
+@moveR_M1
+@moveR_1M
+@ap_1
+(* @ap_pp
+@ap_p_pp ?*)
+@inverse_ap
+@ap_idmap
+(* @ap_compose
+@ap_compose'*)
+@ap_const
+(* Unsure about naturality of [ap], was absent in the old implementation*)
+@apD10_1
+:paths.
+
+Ltac hott_simpl :=
+ autorewrite with paths in * |- * ; auto with path_hints.
+*)
--- /dev/null
+notation "1" with precedence 90 for @{'idpath}.
+
+notation < "hvbox(l1 break # _(term 90 F) (term 47 l2))"
+ non associative with precedence 47
+ for @{'transport $F $l1 $l2 }.
+
+notation > "hvbox(l1 break # l2)"
+ right associative with precedence 47
+ for @{'transport ? $l1 $l2 }.
+
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 49
+ for @{'append $l1 $l2 }.
+
+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+notation "hvbox(〈term 19 a, break term 19 b〉)"
+with precedence 90 for @{ 'mk_exists $a $b }.
+
+(*
+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'exists ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+ }.
+
+(*
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
+
+(* sigma ********************************************************************)
+
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'sigma ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
+ }.
+
+notation "hvbox(« term 19 a, break term 19 b»)"
+with precedence 90 for @{ 'dp $a $b }.
+
+(* dependent pairs (i.e. Sigma with predicate in Type[0]) ********************)
+
+notation < "hvbox(𝚺 ident i : ty break . p)"
+ left associative with precedence 20
+for @{'dpair (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(𝚺 ident i break . p)"
+ with precedence 20
+for @{'dpair (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(𝚺 ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'dpair ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "𝚺 list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}.$acc)} } }
+ }.
+
+notation "hvbox(❬ term 19 a, break term 19 b❭)"
+with precedence 90 for @{ 'mk_DPair $a $b }.
+*)
+
+(* equality, conguence ******************************************************)
+
+notation > "hvbox(a break = b)"
+ non associative with precedence 45
+for @{ 'eq ? $a $b }.
+
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
+ non associative with precedence 45
+for @{ 'eq $t $a $b }.
+
+notation > "hvbox(n break ≅ m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m ? }.
+
+notation < "hvbox(term 46 n break ≅ _ term 90 p term 46 m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+notation "hvbox(n break ≡ m)"
+ non associative with precedence 45
+for @{ 'equiv $n $m }.
+
+(*
+(* other notations **********************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
+*)
+
+notation "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \Pi $_:$a.$b }.
+
+(*
+notation "hvbox(a break \leq b)"
+ non associative with precedence 45
+for @{ 'leq $a $b }.
+
+notation "hvbox(a break \geq b)"
+ non associative with precedence 45
+for @{ 'geq $a $b }.
+
+notation "hvbox(a break \lt b)"
+ non associative with precedence 45
+for @{ 'lt $a $b }.
+
+notation "hvbox(a break \gt b)"
+ non associative with precedence 45
+for @{ 'gt $a $b }.
+
+notation > "hvbox(a break \neq b)"
+ non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
+ non associative with precedence 45
+for @{ 'neq $t $a $b }.
+
+notation "hvbox(a break \nleq b)"
+ non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)"
+ non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)"
+ non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)"
+ non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
+notation "hvbox(a break \divides b)"
+ non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+ non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
+notation "hvbox(a break + b)"
+ left associative with precedence 55
+for @{ 'plus $a $b }.
+
+notation "hvbox(a break - b)"
+ left associative with precedence 55
+for @{ 'minus $a $b }.
+
+notation "hvbox(a break * b)"
+ left associative with precedence 60
+for @{ 'times $a $b }.
+
+notation "hvbox(a break \middot b)"
+ left associative with precedence 60
+ for @{ 'middot $a $b }.
+
+notation "hvbox(a break \mod b)"
+ left associative with precedence 60
+for @{ 'module $a $b }.
+
+notation < "a \frac b"
+ non associative with precedence 90
+for @{ 'divide $a $b }.
+
+notation "a \over b"
+ left associative with precedence 60
+for @{ 'divide $a $b }.
+
+notation "hvbox(a break / b)"
+ left associative with precedence 60
+for @{ 'divide $a $b }.
+
+notation "- term 65 a" with precedence 65
+for @{ 'uminus $a }.
+
+notation "a !"
+ non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "\sqrt a"
+ non associative with precedence 65
+for @{ 'sqrt $a }.
+
+notation "hvbox(a break \lor b)"
+ left associative with precedence 30
+for @{ 'or $a $b }.
+
+notation "hvbox(a break \land b)"
+ left associative with precedence 35
+for @{ 'and $a $b }.
+
+notation "hvbox(\lnot a)"
+ non associative with precedence 40
+for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ∉ b)" non associative with precedence 45
+for @{ 'notmem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" left associative with precedence 60
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" left associative with precedence 55
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45
+ for @{ 'napart $a $b}.
+
+notation "hvbox(a break # b)" non associative with precedence 45
+ for @{ 'apart $a $b}.
+*)
+
+notation "hvbox(a break \circ b)"
+ left associative with precedence 60
+for @{ 'compose $a $b }.
+
+(*
+notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
+notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
+
+notation "↑a" with precedence 60 for @{ 'uparrow $a }.
+
+notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $a $b }.
+
+notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+*)
+notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
+(*
+notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
+
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 65 for @{'Vdash ?}.
+notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
+
+notation < "maction (mstyle color #ff0000 (…)) (t)"
+non associative with precedence 90 for @{'hide $t}.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "notations.ma".
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint Type[2] < Type[3].
+(*universe constraint Type[3] < Type[4].
+universe constraint Type[4] < Type[5].*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "pts.ma".
+
+record Exists (A: Type[0]) (P: A → Type[0]) : Type[0] ≝ {
+ pr1: A;
+ pr2: P pr1
+}.
+
+interpretation "Exists" 'exists x = (Exists ? x).
+interpretation "mk_Exists" 'mk_exists w p = (mk_Exists ?? w p).
projects / helm.git / commitdiff