From 15c2ee289fd633319d1a655ca1efce2f71051540 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 28 Apr 2015 17:31:26 -0400 Subject: [PATCH] feat(hott): make some fibrations in path.hlean implicit, and a bit of renaming in init --- hott/cubical/pathover.hlean | 2 +- hott/cubical/square.hlean | 2 -- hott/hit/circle.hlean | 6 ++-- hott/init/equiv.hlean | 2 +- hott/init/funext.hlean | 2 +- hott/init/path.hlean | 56 ++++++++++++++++++------------------- hott/init/trunc.hlean | 19 +++++++------ hott/init/ua.hlean | 3 ++ hott/types/pi.hlean | 4 +-- hott/types/sigma.hlean | 14 +++++----- hott/types/trunc.hlean | 2 +- 11 files changed, 57 insertions(+), 55 deletions(-) diff --git a/hott/cubical/pathover.hlean b/hott/cubical/pathover.hlean index a561d75c6..810684524 100644 --- a/hott/cubical/pathover.hlean +++ b/hott/cubical/pathover.hlean @@ -8,7 +8,7 @@ Author: Floris van Doorn Theorems about pathovers -/ -import .sigma arity +import types.sigma arity open eq equiv is_equiv equiv.ops diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 6639685de..8c18f3e01 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -8,8 +8,6 @@ Author: Floris van Doorn Theorems about square -/ -import .sigma arity - open eq equiv is_equiv namespace cubical diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index 5b3f8f72c..c7ed9ef23 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -78,7 +78,7 @@ namespace circle { exact Pbase}, { exact (transport P seg1 Pbase)}, { apply idp}, - { apply tr_eq_of_eq_inv_tr, exact (Ploop⁻¹ ⬝ !tr_con)}, + { apply tr_eq_of_eq_inv_tr, exact (Ploop⁻¹ ⬝ !con_tr)}, end --rewrite -tr_con, exact Ploop⁻¹ @@ -88,7 +88,7 @@ namespace circle theorem rec_loop_helper {A : Type} (P : A → Type) {x y : A} {p : x = y} {u : P x} {v : P y} (q : u = p⁻¹ ▹ v) : - eq_inv_tr_of_tr_eq P (tr_eq_of_eq_inv_tr P q) = q := + eq_inv_tr_of_tr_eq (tr_eq_of_eq_inv_tr q) = q := by cases p; exact idp theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : @@ -96,7 +96,7 @@ namespace circle begin rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2], apply concat, apply (ap (λx, x ⬝ _)), apply con_idp, esimp, - rewrite [(rec_loop_helper P),inv_con_inv_left], + rewrite [rec_loop_helper,inv_con_inv_left], apply con_inv_cancel_left end diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 709051d12..e049c4ccb 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -216,7 +216,7 @@ namespace is_equiv --Transporting is an equivalence definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) := - is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p) + is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p) end is_equiv diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 9ee2b4133..f6ca4b9c4 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -36,7 +36,7 @@ definition weak_funext_of_naive_funext : naive_funext → weak_funext := let c := λx, center (P x) in is_contr.mk c (λ f, have eq' : (λx, center (P x)) ∼ f, - from (λx, contr (f x)), + from (λx, center_eq (f x)), have eq : (λx, center (P x)) = f, from nf A P (λx, center (P x)) f eq', eq diff --git a/hott/init/path.hlean b/hott/init/path.hlean index b11a43d83..18eedc72c 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -201,14 +201,14 @@ namespace eq notation f ∼ g := homotopy f g namespace homotopy - protected definition refl (f : Πx, P x) : f ∼ f := + protected definition refl [reducible] (f : Πx, P x) : f ∼ f := λ x, idp - protected definition symm {f g : Πx, P x} (H : f ∼ g) : g ∼ f := - λ x, inverse (H x) + protected definition symm [reducible] {f g : Πx, P x} (H : f ∼ g) : g ∼ f := + λ x, (H x)⁻¹ - protected definition trans {f g h : Πx, P x} (H1 : f ∼ g) (H2 : g ∼ h) : f ∼ h := - λ x, concat (H1 x) (H2 x) + protected definition trans [reducible] {f g h : Πx, P x} (H1 : f ∼ g) (H2 : g ∼ h) : f ∼ h := + λ x, H1 x ⬝ H2 x calc_refl refl calc_symm symm @@ -239,19 +239,19 @@ namespace eq /- More theorems for moving things around in equations -/ - definition tr_eq_of_eq_inv_tr (P : A → Type) {x y : A} {p : x = y} {u : P x} {v : P y} : + definition tr_eq_of_eq_inv_tr {P : A → Type} {x y : A} {p : x = y} {u : P x} {v : P y} : u = p⁻¹ ▹ v → p ▹ u = v := eq.rec_on p (take v, id) v - definition inv_tr_eq_of_eq_tr (P : A → Type) {x y : A} {p : y = x} {u : P x} {v : P y} : + definition inv_tr_eq_of_eq_tr {P : A → Type} {x y : A} {p : y = x} {u : P x} {v : P y} : u = p ▹ v → p⁻¹ ▹ u = v := eq.rec_on p (take u, id) u - definition eq_inv_tr_of_tr_eq (P : A → Type) {x y : A} {p : x = y} {u : P x} {v : P y} : + definition eq_inv_tr_of_tr_eq {P : A → Type} {x y : A} {p : x = y} {u : P x} {v : P y} : p ▹ u = v → u = p⁻¹ ▹ v := eq.rec_on p (take v, id) v - definition eq_tr_of_inv_tr_eq (P : A → Type) {x y : A} {p : y = x} {u : P x} {v : P y} : + definition eq_tr_of_inv_tr_eq {P : A → Type} {x y : A} {p : y = x} {u : P x} {v : P y} : p⁻¹ ▹ u = v → u = p ▹ v := eq.rec_on p (take u, id) u @@ -403,41 +403,41 @@ namespace eq /- Transport and the groupoid structure of paths -/ - definition tr_idp (P : A → Type) {x : A} (u : P x) : idp ▹ u = u := idp + definition idp_tr {P : A → Type} {x : A} (u : P x) : idp ▹ u = u := idp - definition tr_con (P : A → Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) : + definition con_tr {P : A → Type} {x y z : A} (p : x = y) (q : y = z) (u : P x) : p ⬝ q ▹ u = q ▹ p ▹ u := eq.rec_on q (eq.rec_on p idp) - definition tr_inv_tr (P : A → Type) {x y : A} (p : x = y) (z : P y) : + definition tr_inv_tr {P : A → Type} {x y : A} (p : x = y) (z : P y) : p ▹ p⁻¹ ▹ z = z := - (tr_con P p⁻¹ p z)⁻¹ ⬝ ap (λr, transport P r z) (con.left_inv p) + (con_tr p⁻¹ p z)⁻¹ ⬝ ap (λr, transport P r z) (con.left_inv p) - definition inv_tr_tr (P : A → Type) {x y : A} (p : x = y) (z : P x) : + definition inv_tr_tr {P : A → Type} {x y : A} (p : x = y) (z : P x) : p⁻¹ ▹ p ▹ z = z := - (tr_con P p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p) + (con_tr p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p) - definition tr_con_lemma (P : A → Type) + definition con_tr_lemma {P : A → Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) : - ap (λe, e ▹ u) (con.assoc' p q r) ⬝ (tr_con P (p ⬝ q) r u) ⬝ - ap (transport P r) (tr_con P p q u) - = (tr_con P p (q ⬝ r) u) ⬝ (tr_con P q r (p ▹ u)) + ap (λe, e ▹ u) (con.assoc' p q r) ⬝ (con_tr (p ⬝ q) r u) ⬝ + ap (transport P r) (con_tr p q u) + = (con_tr p (q ⬝ r) u) ⬝ (con_tr q r (p ▹ u)) :> ((p ⬝ (q ⬝ r)) ▹ u = r ▹ q ▹ p ▹ u) := eq.rec_on r (eq.rec_on q (eq.rec_on p idp)) -- Here is another coherence lemma for transport. - definition tr_inv_tr_lemma (P : A → Type) {x y : A} (p : x = y) (z : P x) : - tr_inv_tr P p (transport P p z) = ap (transport P p) (inv_tr_tr P p z) := + definition tr_inv_tr_lemma {P : A → Type} {x y : A} (p : x = y) (z : P x) : + tr_inv_tr p (transport P p z) = ap (transport P p) (inv_tr_tr p z) := eq.rec_on p idp /- some properties for apd -/ definition apd_idp (x : A) (f : Πx, P x) : apd f idp = idp :> (f x = f x) := idp definition apd_con (f : Πx, P x) {x y z : A} (p : x = y) (q : y = z) - : apd f (p ⬝ q) = tr_con P p q (f x) ⬝ ap (transport P q) (apd f p) ⬝ apd f q := + : apd f (p ⬝ q) = con_tr p q (f x) ⬝ ap (transport P q) (apd f p) ⬝ apd f q := by cases p;cases q;apply idp definition apd_inv (f : Πx, P x) {x y : A} (p : x = y) - : apd f p⁻¹ = (eq_inv_tr_of_tr_eq P (apd f p))⁻¹ := + : apd f p⁻¹ = (eq_inv_tr_of_tr_eq (apd f p))⁻¹ := by cases p;apply idp @@ -462,7 +462,7 @@ namespace eq transport2 Q r z = ap10 (ap (transport Q) r) z := eq.rec_on r idp - definition tr2_con (P : A → Type) {x y : A} {p1 p2 p3 : x = y} + definition tr2_con {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 := eq.rec_on r1 (eq.rec_on r2 idp) @@ -525,10 +525,10 @@ namespace eq eq.rec_on p idp -- A special case of [transport_compose] which seems to come up a lot. - definition tr_eq_cast_ap (P : A → Type) {x y} (p : x = y) (u : P x) : p ▹ u = cast (ap P p) u := + definition tr_eq_cast_ap {P : A → Type} {x y} (p : x = y) (u : P x) : p ▹ u = cast (ap P p) u := eq.rec_on p idp - definition tr_eq_cast_ap_fn (P : A → Type) {x y} (p : x = y) : transport P p = cast (ap P p) := + definition tr_eq_cast_ap_fn {P : A → Type} {x y} (p : x = y) : transport P p = cast (ap P p) := eq.rec_on p idp /- The behavior of [ap] and [apd] -/ @@ -649,11 +649,11 @@ namespace eq eq.rec_on r !idp_con⁻¹ -- And now for a lemma whose statement is much longer than its proof. - definition apd02_con (P : A → Type) (f : Π x:A, P x) {x y : A} + definition apd02_con {P : A → Type} (f : Π x:A, P x) {x y : A} {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) : apd02 f (r1 ⬝ r2) = apd02 f r1 ⬝ whisker_left (transport2 P r1 (f x)) (apd02 f r2) ⬝ con.assoc' _ _ _ - ⬝ (whisker_right (tr2_con P r1 r2 (f x))⁻¹ (apd f p3)) := + ⬝ (whisker_right (tr2_con r1 r2 (f x))⁻¹ (apd f p3)) := eq.rec_on r2 (eq.rec_on r1 (eq.rec_on p1 idp)) end eq diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index fbc7b59ea..450030aac 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -64,7 +64,8 @@ namespace is_trunc -/ structure contr_internal (A : Type) := - (center : A) (contr : Π(a : A), center = a) + (center : A) + (center_eq : Π(a : A), center = a) definition is_trunc_internal (n : trunc_index) : Type → Type := trunc_index.rec_on n @@ -95,17 +96,17 @@ namespace is_trunc /- contractibility -/ - definition is_contr.mk (center : A) (contr : Π(a : A), center = a) : is_contr A := - is_trunc.mk (contr_internal.mk center contr) + definition is_contr.mk (center : A) (center_eq : Π(a : A), center = a) : is_contr A := + is_trunc.mk (contr_internal.mk center center_eq) definition center (A : Type) [H : is_contr A] : A := @contr_internal.center A !is_trunc.to_internal - definition contr [H : is_contr A] (a : A) : !center = a := - @contr_internal.contr A !is_trunc.to_internal a + definition center_eq [H : is_contr A] (a : A) : !center = a := + @contr_internal.center_eq A !is_trunc.to_internal a definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y := - (contr x)⁻¹ ⬝ (contr y) + (center_eq x)⁻¹ ⬝ (center_eq y) definition hprop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q := have K : ∀ (r : x = y), eq_of_is_contr x y = r, from (λ r, eq.rec_on r !con.left_inv), @@ -215,7 +216,7 @@ namespace is_trunc --"is_trunc_is_equiv_closed" definition is_contr_is_equiv_closed (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) := - is_contr.mk (f (center A)) (λp, eq_of_eq_inv !contr) + is_contr.mk (f (center A)) (λp, eq_of_eq_inv !center_eq) theorem is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B := @is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _ @@ -223,7 +224,7 @@ namespace is_trunc definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B := equiv.mk (λa, center B) - (is_equiv.adjointify (λa, center B) (λb, center A) contr contr) + (is_equiv.adjointify (λa, center B) (λb, center A) center_eq center_eq) definition is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f] [HA : is_trunc n A] : is_trunc n B := @@ -258,7 +259,7 @@ namespace is_trunc equiv.MK (λ (x : A), ⋆) (λ (u : unit), center A) (λ (u : unit), unit.rec_on u idp) - (λ (x : A), contr x) + (λ (x : A), center_eq x) -- TODO: port "Truncated morphisms" diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index b04636a5c..e5fe8bd96 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -33,6 +33,9 @@ attribute univalence [instance] definition ua [reducible] {A B : Type} : A ≃ B → A = B := equiv_of_eq⁻¹ +definition eq_equiv_equiv (A B : Type) : (A = B) ≃ (A ≃ B) := +equiv.mk equiv_of_eq _ + definition equiv_of_eq_ua [reducible] {A B : Type} (f : A ≃ B) : equiv_of_eq (ua f) = f := right_inv equiv_of_eq f diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 54739915f..d1d645fed 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -1,5 +1,5 @@ /- -Copyright (c) 2014 Floris van Doorn. All rights reserved. +Copyright (c) 2014-15 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: types.pi @@ -163,7 +163,7 @@ namespace pi fapply is_contr.mk, intro a, apply center, intro f, apply eq_of_homotopy, - intro x, apply (contr (f x))}, + intro x, apply (center_eq (f x))}, {intros [n, IH, B, H], fapply is_trunc_succ_intro, intros [f, g], fapply is_trunc_equiv_closed, diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 793a0aab0..653b4bf5c 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -1,5 +1,5 @@ /- -Copyright (c) 2014 Floris van Doorn. All rights reserved. +Copyright (c) 2014-15 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: types.sigma @@ -101,13 +101,13 @@ namespace sigma definition dpair_eq_dpair_con (p1 : a = a' ) (q1 : p1 ▹ b = b' ) (p2 : a' = a'') (q2 : p2 ▹ b' = b'') : - dpair_eq_dpair (p1 ⬝ p2) (tr_con B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2) + dpair_eq_dpair (p1 ⬝ p2) (con_tr p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2) = dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 := by cases p1; cases p2; cases q1; cases q2; apply idp definition sigma_eq_con (p1 : u.1 = v.1) (q1 : p1 ▹ u.2 = v.2) (p2 : v.1 = w.1) (q2 : p2 ▹ v.2 = w.2) : - sigma_eq (p1 ⬝ p2) (tr_con B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2) + sigma_eq (p1 ⬝ p2) (con_tr p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2) = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 := by cases u; cases v; cases w; apply dpair_eq_dpair_con @@ -200,7 +200,7 @@ namespace sigma -- "rewrite right_inv (g (f⁻¹ a'))" apply concat, apply (ap (λx, (transport B' (right_inv f a') x))), apply (right_inv (g (f⁻¹ a'))), show right_inv f a' ▹ ((right_inv f a')⁻¹ ▹ b') = b', - from tr_inv_tr _ (right_inv f a') b' + from tr_inv_tr (right_inv f a') b' end begin intro u, @@ -253,7 +253,7 @@ namespace sigma adjointify pr1 (λa, ⟨a, !center⟩) (λa, idp) - (λu, sigma_eq idp !contr) + (λu, sigma_eq idp !center_eq) definition sigma_equiv_of_is_contr_pr2 [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A := equiv.mk pr1 _ @@ -263,10 +263,10 @@ namespace sigma definition sigma_equiv_of_is_contr_pr1 (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A) := equiv.mk _ (adjointify - (λu, (contr u.1)⁻¹ ▹ u.2) + (λu, (center_eq u.1)⁻¹ ▹ u.2) (λb, ⟨!center, b⟩) (λb, ap (λx, x ▹ b) !hprop_eq_of_is_contr) - (λu, sigma_eq !contr !tr_inv_tr)) + (λu, sigma_eq !center_eq !tr_inv_tr)) /- Associativity -/ diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index ebe4c3b7c..c2494a11c 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -19,7 +19,7 @@ namespace is_trunc fapply equiv.mk, {intro S, apply is_contr.mk, exact S.2}, {fapply is_equiv.adjointify, - {intro H, apply sigma.mk, exact (@contr A H)}, + {intro H, apply sigma.mk, exact (@center_eq A H)}, {intro H, apply (is_trunc.rec_on H), intro Hint, apply (contr_internal.rec_on Hint), intros [H1, H2], apply idp},