1 include "hott/types.ma".
2 include "basics/core_notation/compose_2.ma".
4 (* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
6 definition relation ≝ λA : Type[0]. A → A → Type[0].
8 record Reflexive (A) (R : relation A) : Type[0] ≝ {
9 reflexivity : ∀x : A. R x x
12 record Symmetric (A) (R : relation A) : Type[0] ≝ {
13 symmetry : ∀x,y. R x y → R y x
16 record Transitive (A) (R : relation A) : Type[0] ≝ {
17 transitivity : ∀x,y,z. R x y → R y z → R x z
20 (*Tactic Notation "etransitivity" open_constr(y) :=
21 let R := match goal with |- ?R ?x ?z => constr:(R) end in
22 let x := match goal with |- ?R ?x ?z => constr:(x) end in
23 let z := match goal with |- ?R ?x ?z => constr:(z) end in
24 refine (@transitivity _ R _ x y z _ _).*)
26 (*Tactic Notation "etransitivity" := etransitivity _.*)
28 (* * We would like to redefine [symmetry], which is too smart for its own good, as follows:
31 Ltac symmetry := refine (@symmetry _ _ _ _ _ _).
34 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. *)
36 (* * ** Basic definitions *)
38 (*CSC: was a Notation in Coq *)
39 definition idmap : ∀A:Type[0]. A → A ≝ λA,x.x.
41 (* * Composition of functions. *)
42 definition compose ≝ λA,B,C: Type[0]. λg : B → C. λf : A → B.
45 interpretation "compose" 'compose g f = (compose ??? g f).
47 (* * ** The groupoid structure of identity types. *)
49 (* * The results in this file are used everywhere else, so we need to be extra
50 careful about how we define and prove things. We prefer hand-written terms,
51 or at least tactics that allow us to retain clear control over the
52 proof-term produced. *)
54 (* * We define our own identity type, rather than using the one in the Coq
55 standard library, so as to have more control over transitivity, symmetry
56 and inverse. It seems impossible to change these for the standard
57 eq/identity type (or its Type-valued version) because it breaks various
58 other standard things. Merely changing notations also doesn't seem to
60 inductive paths (A : Type[0]) (a : A) : A → Type[0] ≝
63 interpretation "paths" 'eq t a b = (paths t a b).
65 (*CSC: MANCANO GLI HINT *)
66 definition reflexive_paths: ∀A:Type[0]. Reflexive … (paths A) ≝
67 λA. mk_Reflexive … (idpath A).
69 (* * We define equality concatenation by destructing on both its arguments, so
70 that it only computes when both arguments are [idpath]. This makes proofs
71 more robust and symmetrical. Compare with the definition of [identity_trans]. *)
73 definition concat : ∀A : Type[0]. ∀x,y,z: A. x = y → y = z → x = z.
74 #A #x #y #z #p #q cases q cases p %
77 (*CSC: MANCANO GLI HINT *)
78 definition transitive_paths: ∀A:Type[0]. Transitive … (paths A) ≝
79 λA.mk_Transitive … (concat A).
81 (* * The inverse of a path. *)
82 definition inverse : ∀A : Type[0]. ∀x,y : A. x = y → y = x.
86 (*CSC: MANCANO GLI HINT *)
87 definition symmetric_paths: ∀A:Type[0]. Symmetric … (paths A) ≝
88 λA. mk_Symmetric … (inverse A).
90 (* * Note that you can use the built-in Coq tactics [reflexivity] and [transitivity]
91 when working with paths, but not [symmetry], because it is too smart for its
92 own good. Instead, you can write [apply symmetry] or [eapply symmetry]. *)
94 (* * The identity path. *)
95 interpretation "idpath" 'idpath = (idpath ??).
97 interpretation "concat" 'append g f = (concat ???? g f).
99 interpretation "inverse" 'invert p = (inverse ??? p).
101 (* * An important instance of [paths_rect] is that given any dependent type, one
102 can _transport_ elements of instances of the type along equalities in the base.
104 [transport P p u] transports [u : P x] to [P y] along [p : x = y]. *)
105 definition transport: ∀A : Type[0]. ∀P: A → Type[0]. ∀x,y : A. x=y → P x → P y.
109 (* * Transport is very common so it is worth introducing a parsing notation for it.
110 However, we do not use the notation for output because it hides the fibration,
111 and so makes it very hard to read involved transport expression.*)
113 interpretation "transport" 'transport F p x = (transport ? F ?? p x).
115 (* * Having defined transport, we can use it to talk about what a homotopy
116 theorist might see as "paths in a fibration over paths in the base"; and what
117 a type theorist might see as "heterogeneous eqality in a dependent type".
119 We will first see this appearing in the type of [apD]. *)
121 (* * Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A],
122 then [ap f p : f x = f y].
124 We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)
126 definition ap: ∀A,B: Type[0]. ∀f:A → B. ∀x,y: A. x = y → f x = f y.
130 (* * We introduce the convention that [apKN] denotes the application of a K-path
131 between functions to an N-path between elements, where a 0-path is simply a
132 function or an element. Thus, [ap] is a shorthand for [ap01]. *)
133 (*CSC: WAS A NOTATION *)
134 definition ap01 := ap.
136 definition pointwise_paths:
137 ∀A:Type[0]. ∀P:A → Type[0]. ∀f,g: ∀x:A. P x. Type[0] ≝
138 λA,P,f,g. ∀x. f x = g x.
140 interpretation "pointwise_paths" 'congruent f g T = (pointwise_paths ? T f g).
142 definition apD10: ∀A:Type[0]. ∀B:A→Type[0]. ∀f,g: ∀x. B x. f = g → f ≅ g.
146 definition ap10: ∀A,B: Type[0]. ∀f,g:A → B. f=g → f ≅ g ≝
149 definition ap11: ∀A,B: Type[0]. ∀f,g: A → B. f=g → ∀x,y:A. x=y → f x = g y.
150 #A #B #f #g * #x #y * %
153 (* * Similarly, dependent functions act on paths; but the type is a bit more
154 subtle. If [f : forall a:A, B a] and [p : x = y] is a path in [A], then
155 [apD f p] should somehow be a path between [f x : B x] and [f y : B y].
156 Since these live in different types, we use transport along [p] to make them
157 comparable: [apD f p : p # f x = f y].
159 The type [p # f x = f y] can profitably be considered as a heterogeneous or
160 dependent equality type, of "paths from [f x] to [f y] over [p]". *)
163 ∀A:Type[0]. ∀B:A → Type[0]. ∀f:∀a:A. B a. ∀x,y:A.
164 ∀p:x=y. p # (f x) = f y.
168 (* * ** Equivalences *)
170 (* * Homotopy equivalences are a central concept in homotopy type theory.
171 Before we define equivalences, let us consider when two types [A] and [B]
172 should be considered "the same".
174 The first option is to require existence of [f : A -> B] and [g : B -> A]
175 which are inverses of each other, up to homotopy. Homotopically speaking, we
176 should also require a certain condition on these homotopies, which is one of
177 the triangle identities for adjunctions in category theory. Thus, we call
178 this notion an *adjoint equivalence*.
180 The other triangle identity is provable from the first one, along with all the
181 higher coherences, so it is reasonable to only assume one of them. Moreover,
182 as we will see, if we have maps which are inverses up to homotopy, it is always
183 possible to make the triangle identity hold by modifying one of the homotopies.
185 The second option is to use Vladimir Voevodsky's definition of an equivalence
186 as a map whose homotopy fibers are contractible. We call this notion a
187 *homotopy bijection*.
189 An interesting third option was suggested by André Joyal: a map [f] which has
190 separate left and right homotopy inverses. We call this notion a
191 *homotopy isomorphism*.
193 While the second option was the one used originally, and it is the most
194 concise one, it makes more sense to use the first one in a formalized
195 development, since it exposes most directly equivalence as a structure.
196 In particular, it is easier to extract directly from it the data of a homotopy
197 inverse to [f], which is what we care about having most in practice. Thus,
198 adjoint equivalences are what we will refer to merely as *equivalences*. *)
200 (* * Naming convention: we use [equiv] and [Equiv] systematically to denote types
201 of equivalences, and [isequiv] and [IsEquiv] systematically to denote the
202 assertion that a given map is an equivalence. *)
204 (* * The fact that [r] is a left inverse of [s]. As a mnemonic, note that the
205 partially applied type [Sect s] is the type of proofs that [s] is a section. *)
206 definition Sect: ∀A,B : Type[0]. (A → B) → (B → A) → Type[0] ≝
207 λA,B,s,r. ∀x : A. r (s x) = x.
209 (* * A typeclass that includes the data making [f] into an adjoint equivalence. *)
210 record IsEquiv (A,B : Type[0]) (f : A → B) : Type[0] ≝ {
212 eisretr : Sect … equiv_inv f;
213 eissect : Sect … f equiv_inv;
214 eisadj : ∀x:A. eisretr (f x) = (* f (equiv_inv (f x)) = f x *) ap … f … (eissect x)
217 (* * A record that includes all the data of an adjoint equivalence. *)
218 record Equiv (A,B) : Type[0] ≝ {
219 equiv_fun :1> A → B ;
220 equiv_isequiv :> IsEquiv … equiv_fun
223 interpretation "Equiv" 'equiv A B p = (Equiv A B).
225 (* * A notation for the inverse of an equivalence. We can apply this to a
226 function as long as there is a typeclass instance asserting it to be an
227 equivalence. We can also apply it to an element of [A <~> B], since there is
228 an implicit coercion to [A -> B] and also an existing instance of [IsEquiv]. *)
230 (*CSC: PROBABLY WE NEED TO INTERPRET 'invert_appl TOO *)
231 interpretation "equiv_inv" 'invert f = (equiv_inv ?? f ?).
234 (** ** Contractibility and truncation levels *)
236 (** 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.
238 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.
240 - 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)].
242 - 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.
245 (** *** Contractibility *)
247 (** 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]. *)
249 (** 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.] *)
250 Class Contr_internal (A : Type) := BuildContr {
252 contr : (forall y : A, center = y)
255 Arguments center A {_}.
257 (** *** Truncation levels *)
259 (** 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.
261 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").
263 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".
266 Inductive trunc_index : Type :=
267 | minus_two : trunc_index
268 | trunc_S : trunc_index -> trunc_index.
270 (** We will use [Notation] for [trunc_index]es, so define a scope for them here. *)
271 Delimit Scope trunc_scope with trunc.
272 Bind Scope trunc_scope with trunc_index.
273 Arguments trunc_S _%trunc_scope.
275 Fixpoint nat_to_trunc_index (n : nat) : trunc_index
277 | 0 => trunc_S (trunc_S minus_two)
278 | S n' => trunc_S (nat_to_trunc_index n')
281 Coercion nat_to_trunc_index : nat >-> trunc_index.
283 Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
285 | minus_two => Contr_internal A
286 | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
289 Notation minus_one:=(trunc_S minus_two).
290 (** 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]. *)
291 Notation "0" := (trunc_S minus_one) : trunc_scope.
292 Notation "1" := (trunc_S 0) : trunc_scope.
293 Notation "2" := (trunc_S 1) : trunc_scope.
295 Arguments IsTrunc_internal n A : simpl nomatch.
297 Class IsTrunc (n : trunc_index) (A : Type) : Type :=
298 Trunc_is_trunc : IsTrunc_internal n A.
300 (** 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. *)
302 Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
304 Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
306 Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
308 := H x y. (* but do fold [IsTrunc] *)
310 Hint Extern 0 => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
312 (** 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. *)
314 progress match goal with
315 | [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ]
316 => change (IsTrunc (trunc_S n) T) in H
317 | [ H : forall (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]
318 => change (forall a : A, IsTrunc (trunc_S n) (T a)) in H; cbv beta in H
319 | [ H : forall (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]
320 => change (forall (a : A) (b : B a), IsTrunc (trunc_S n) (T a b)) in H; cbv beta in H
321 | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]
322 => 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
323 | [ 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) |- _ ]
324 => 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
327 Notation Contr := (IsTrunc minus_two).
328 Notation IsHProp := (IsTrunc minus_one).
329 Notation IsHSet := (IsTrunc 0).
331 Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
333 (** *** Function extensionality *)
335 (** 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}]. *)
337 { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
339 Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
344 Definition path_forall2 `{Funext} {A B : Type} {P : A -> B -> Type} (f g : forall x y, P x y) :
345 (forall x y, f x y = g x y) -> f = g
347 (fun E => path_forall f g (fun x => path_forall (f x) (g x) (E x))).
352 (** 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.
354 A specific [Hint Resolve] database [db] can be used with [auto with db].
356 The hints in [path_hints] are designed to push concatenation *outwards*, eliminate identities and inverses, and associate to the left as far as possible. *)
358 (** TODO: think more carefully about this. Perhaps associating to the right would be more convenient? *)
363 Hint Resolve @idpath : core.
366 apply @concat with (y := mid); auto with path_hints.
368 (** We put [Empty] here, instead of in [Empty.v], because [Ltac done] uses it. *)
369 Inductive Empty : Type := .
371 Definition not (A:Type) : Type := A -> Empty.
372 Notation "~ x" := (not x) : type_scope.
373 Hint Unfold not: core.
375 (** *** Pointed types *)
377 (** A space is pointed if that space has a point. *)
378 Class IsPointed (A : Type) := point : A.
379 Definition pointedType := { u : Type & IsPointed u }.
381 (** Ssreflect tactics, adapted by Robbert Krebbers *)
383 trivial; intros; solve
386 | solve [eapply symmetry; trivial]
388 (* Discriminate should be here, but it doesn't work yet *)
393 H : ~ _ |- _ => solve [destruct H; trivial]
395 Tactic Notation "by" tactic(tac) :=
398 (** A convenient tactic for using function extensionality. *)
399 Ltac by_extensionality x :=
400 intros; unfold compose;
402 | [ |- ?f = ?g ] => eapply path_forall; intro x;
404 | [ |- forall (_ : prod _ _), _ ] => intros [? ?]
405 | [ |- forall (_ : sigT _ _), _ ] => intros [? ?]
408 simpl; auto with path_hints
411 (** Removed auto. We can write "by (path_induction;auto with path_hints)"
413 Ltac path_induction :=
414 intros; repeat progress (
416 | [ p : _ = _ |- _ ] => induction p
421 (** 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. *)
424 | [ |- ?f ?x = ?g ?x ] => apply (@apD10 _ _ f g);
431 (** [expand] replaces both terms of an equality (either [paths] or [pointwise_paths] in the goal with their head normal forms *)
435 let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')
437 let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')
440 (** [atomic x] is the same as [idtac] if [x] is a variable or hypothesis, but is [fail 0] if [x] has internal structure. *)
443 | ?f _ => fail 1 x "is not atomic"
444 | (fun _ => _) => fail 1 x "is not atomic"
445 | forall _, _ => fail 1 x "is not atomic"