From 7a780b1b6048e116f2629e2ddfd67d02a4ecfa6f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 29 Jul 2015 14:17:16 +0200 Subject: [PATCH] feat(hott): various minor changes in the HoTT library --- .../category/constructions/functor.hlean | 1 - .../algebra/category/constructions/hset.hlean | 8 +- hott/algebra/category/iso.hlean | 15 ++-- hott/algebra/e_closure.hlean | 12 ++- hott/arity.hlean | 2 +- hott/hit/circle.hlean | 2 +- hott/hit/colimit.hlean | 2 +- hott/hit/susp.hlean | 12 +-- hott/hit/two_quotient.hlean | 28 +++--- hott/init/equiv.hlean | 90 ++++++++++--------- hott/init/funext.hlean | 17 ++-- hott/init/path.hlean | 2 +- hott/init/pathover.hlean | 7 +- hott/types/cubical/cube.hlean | 37 ++++++-- hott/types/cubical/cubeover.hlean | 12 +-- hott/types/cubical/square.hlean | 36 +++++--- hott/types/eq.hlean | 6 +- hott/types/equiv.hlean | 44 +++++---- hott/types/hprop_trunc.hlean | 4 +- hott/types/pi.hlean | 54 +++++------ hott/types/pointed.hlean | 10 ++- hott/types/sigma.hlean | 3 +- hott/types/trunc.hlean | 30 ++++--- tests/lean/hott/433.hlean | 3 +- tests/lean/hott/unfold_test.hlean | 2 +- 25 files changed, 246 insertions(+), 193 deletions(-) diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index b6407dc16..510d9cbd6 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -123,7 +123,6 @@ namespace category {intro c c' f, esimp [eq_of_iso_ob, inv_of_eq, hom_of_eq, eq_of_iso], rewrite [*right_inv iso_of_eq], - esimp [function.id], symmetry, apply @naturality_iso _ _ _ _ _ (iso.struct _) } end diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean index 819dde294..56b094f2e 100644 --- a/hott/algebra/category/constructions/hset.hlean +++ b/hott/algebra/category/constructions/hset.hlean @@ -35,8 +35,8 @@ namespace category definition equiv_of_iso {A B : Precategory_hset} (f : A ≅ B) : A ≃ B := begin apply equiv.MK (to_hom f) (iso.to_inv f), - exact ap10 (right_inverse (to_hom f)), - exact ap10 (left_inverse (to_hom f)) + exact ap10 (to_right_inverse f), + exact ap10 (to_left_inverse f) end definition is_equiv_iso_of_equiv (A B : Precategory_hset) : is_equiv (@iso_of_equiv A B) := @@ -64,8 +64,8 @@ namespace category equiv.MK (λf, iso_of_equiv f) (λf, proof equiv.MK (to_hom f) (iso.to_inv f) - (ap10 (right_inverse (to_hom f))) - (ap10 (left_inverse (to_hom f))) qed) + (ap10 (to_right_inverse f)) + (ap10 (to_left_inverse f)) qed) (λf, proof iso_eq idp qed) (λf, proof equiv_eq idp qed) diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index c14026a8f..4536f24c4 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -137,24 +137,27 @@ namespace iso include C infix `≅`:50 := iso - attribute iso.struct [instance] [priority 400] + attribute struct [instance] [priority 400] attribute to_hom [coercion] protected definition MK [constructor] (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) := - @mk _ _ _ _ f (is_iso.mk H1 H2) + @(mk f) (is_iso.mk H1 H2) - definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := - (to_hom f)⁻¹ + definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹ + definition to_left_inverse [unfold 5] (f : a ≅ b) : (to_hom f)⁻¹ ∘ (to_hom f) = id := + left_inverse (to_hom f) + definition to_right_inverse [unfold 5] (f : a ≅ b) : (to_hom f) ∘ (to_hom f)⁻¹ = id := + right_inverse (to_hom f) protected definition refl [constructor] (a : ob) : a ≅ a := mk (ID a) - protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := + protected definition symm [constructor] ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (to_hom H)⁻¹ - protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := + protected definition trans [constructor] ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (to_hom H2 ∘ to_hom H1) definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f') diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index f798596bf..4218d46c5 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -33,7 +33,7 @@ section variables ⦃a a' : A⦄ {s : R a a'} {r : T a a} parameter {R} - protected definition e_closure.elim {B : Type} {f : A → B} + protected definition e_closure.elim [unfold 6] {B : Type} {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' := begin induction t, @@ -43,7 +43,7 @@ section exact v_0 ⬝ v_1 end - definition ap_e_closure_elim_h {B C : Type} {f : A → B} {g : B → C} + definition ap_e_closure_elim_h [unfold 12] {B C : Type} {f : A → B} {g : B → C} (e : Π⦃a a' : A⦄, R a a' → f a = f a') {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') @@ -84,16 +84,14 @@ section (ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) t) := begin induction t, - { unfold [ap_e_closure_elim_h, e_closure.elim], + { esimp, apply square_of_eq, exact !con.right_inv ⬝ !con.left_inv⁻¹}, { apply ids}, - { unfold [e_closure.elim, ap_e_closure_elim_h], - rewrite [ap_con (ap h)], + { rewrite [▸*,ap_con (ap h)], refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _, rewrite [con_inv,inv_inv,-inv2_inv], exact !ap_inv2 ⬝v square_inv2 v_0}, - { unfold [e_closure.elim, ap_e_closure_elim_h], - rewrite [ap_con (ap h)], + { rewrite [▸*,ap_con (ap h)], refine (transpose !ap_compose_con)⁻¹ᵛ ⬝h _, rewrite [con_inv,inv_inv,con2_inv], refine !ap_con2 ⬝v square_con2 v_0 v_1}, diff --git a/hott/arity.hlean b/hott/arity.hlean index f4be844c9..cd1d4d2b3 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -187,7 +187,7 @@ namespace funext adjointify _ eq_of_homotopy2 begin - intro H, esimp [apd100, eq_of_homotopy2, function.compose], + intro H, esimp [apd100, eq_of_homotopy2], apply eq_of_homotopy, intro a, apply concat, apply (ap (λx, apd10 (x a))), apply (right_inv apd10), apply (right_inv apd10) diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index d7a17712c..f54b4c33a 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -152,7 +152,7 @@ attribute circle.rec2 circle.elim2 [unfold 6] [recursor 6] attribute circle.elim2_type [unfold 5] attribute circle.rec2_on circle.elim2_on [unfold 2] attribute circle.elim2_type [unfold 1] -attribute circle.elim circle.rec [unfold 4] [recursor 4] +attribute circle.rec circle.elim [unfold 4] [recursor 4] attribute circle.elim_type [unfold 3] attribute circle.rec_on circle.elim_on [unfold 2] attribute circle.elim_type_on [unfold 1] diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 220c40585..9b5003674 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -93,7 +93,7 @@ namespace seq_colim section /- we define it directly in terms of quotients. An alternative definition could be - definition seq_colim := colimit.colimit A function.id succ f + definition seq_colim := colimit.colimit A id succ f -/ parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n)) variables {n : ℕ} (a : A n) diff --git a/hott/hit/susp.hlean b/hott/hit/susp.hlean index 3526fc001..c06c9abcd 100644 --- a/hott/hit/susp.hlean +++ b/hott/hit/susp.hlean @@ -105,7 +105,7 @@ namespace susp { intro a, induction a, { reflexivity}, { reflexivity}, - { apply pathover_eq, apply hdeg_square, + { apply eq_pathover, apply hdeg_square, rewrite [▸*,ap_compose' _ (Susp_functor f),↑Susp_functor,+elim_merid]}}, { reflexivity} end @@ -136,7 +136,7 @@ namespace susp refine _ ⬝ !con.assoc', rewrite inverse2_right_inv, refine _ ⬝ !con.assoc', - rewrite [ap_con_right_inv,↑Susp_functor,idp_con_idp,-ap_compose]}, + rewrite [ap_con_right_inv], unfold Susp_functor, xrewrite [idp_con_idp,-ap_compose], }, end definition loop_susp_counit [constructor] (X : Pointed) : Susp (Ω X) →* X := @@ -154,9 +154,9 @@ namespace susp { intro x', induction x' with p, { reflexivity}, { reflexivity}, - { esimp, apply pathover_eq, apply hdeg_square, - xrewrite [ap_compose f,ap_compose (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*, - +elim_merid,▸*,idp_con]}}, + { esimp, apply eq_pathover, apply hdeg_square, + xrewrite [ap_compose f,ap_compose (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*], + xrewrite [+elim_merid,▸*,idp_con]}}, { reflexivity} end @@ -181,7 +181,7 @@ namespace susp { intro x', induction x', { reflexivity}, { exact merid pt}, - { apply pathover_eq, + { apply eq_pathover, xrewrite [▸*, ap_id, ap_compose (susp.elim north north (λa, a)), +elim_merid,▸*], apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹}}, { reflexivity} diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index bd20aa8ed..11e84995c 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import hit.circle types.eq2 algebra.e_closure +import hit.circle types.eq2 algebra.e_closure types.cubical.cube open quotient eq circle sum sigma equiv function relation @@ -21,17 +21,17 @@ namespace simple_two_quotient local abbreviation B := A ⊎ Σ(a : A) (r : T a a), Q r - inductive pre_simple_two_quotient_rel : B → B → Type := - | pre_Rmk {} : Π⦃a a'⦄ (r : R a a'), pre_simple_two_quotient_rel (inl a) (inl a') + inductive pre_two_quotient_rel : B → B → Type := + | pre_Rmk {} : Π⦃a a'⦄ (r : R a a'), pre_two_quotient_rel (inl a) (inl a') --BUG: if {} not provided, the alias for pre_Rmk is wrong - definition pre_simple_two_quotient := quotient pre_simple_two_quotient_rel + definition pre_two_quotient := quotient pre_two_quotient_rel - open pre_simple_two_quotient_rel - local abbreviation C := quotient pre_simple_two_quotient_rel - protected definition j [constructor] (a : A) : C := class_of pre_simple_two_quotient_rel (inl a) + open pre_two_quotient_rel + local abbreviation C := quotient pre_two_quotient_rel + protected definition j [constructor] (a : A) : C := class_of pre_two_quotient_rel (inl a) protected definition pre_aux [constructor] (q : Q r) : C := - class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩) + class_of pre_two_quotient_rel (inr ⟨a, r, q⟩) protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s) protected definition et (t : T a a') : j a = j a' := e_closure.elim e t protected definition f [unfold 7] (q : Q r) : S¹ → C := @@ -102,7 +102,7 @@ namespace simple_two_quotient definition incl2 (q : Q r) : inclt r = idp := inclt_eq_incltw r ⬝ incl2w q - local attribute simple_two_quotient f i incl0 aux incl1 incl2' inclt [reducible] + local attribute simple_two_quotient f i D incl0 aux incl1 incl2' inclt [reducible] local attribute i aux incl0 [constructor] protected definition elim {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') @@ -116,7 +116,7 @@ namespace simple_two_quotient { exact P1}}, { exact abstract begin induction H, induction x, { exact idpath (P0 a)}, - { unfold f, apply pathover_eq, apply hdeg_square, + { unfold f, apply eq_pathover, apply hdeg_square, exact abstract ap_compose (pre_elim P0 _ P1) (f q) loop ⬝ ap _ !elim_loop ⬝ !elim_et ⬝ @@ -167,7 +167,7 @@ namespace simple_two_quotient krewrite [-eq_of_homotopy3_inv,-eq_of_homotopy3_con] end - definition elim_incl2'_incl0 {P : Type} {P0 : A → P} + definition elim_incl2' {P : Type} {P0 : A → P} {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp) ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) := @@ -198,7 +198,7 @@ namespace simple_two_quotient apply eq_vconcat, { apply ap (λx, _ ⬝ eq_con_inv_of_con_eq ((_ ⬝ x ⬝ _)⁻¹ ⬝ _) ⬝ _), transitivity _, apply ap eq_of_square, - apply to_right_inv !pathover_eq_equiv_square (hdeg_square (elim_1 P A R Q P0 P1 a r q P2)), + apply to_right_inv !eq_pathover_equiv_square (hdeg_square (elim_1 P A R Q P0 P1 a r q P2)), transitivity _, apply eq_of_square_hdeg_square, unfold elim_1, reflexivity}, rewrite [+con_inv,whisker_left_inv,+inv_inv,-whisker_right_inv, @@ -212,10 +212,10 @@ namespace simple_two_quotient right_inv_eq_idp ( (λ(x : ap (elim P0 P1 P2) (incl2' q base) = idpath (elim P0 P1 P2 (class_of simple_two_quotient_rel (f q base)))), x) - (elim_incl2'_incl0 P2 q)), + (elim_incl2' P2 q)), ↑[whisker_left]], xrewrite [con2_con_con2], - rewrite [idp_con,↑elim_incl2'_incl0,con.left_inv,whisker_right_inv,↑whisker_right], + rewrite [idp_con,↑elim_incl2',con.left_inv,whisker_right_inv,↑whisker_right], xrewrite [con.assoc _ _ (_ ◾ _)], rewrite [con.left_inv,▸*,-+con.assoc,con.assoc _⁻¹,↑[elim,function.compose],con.left_inv, ▸*,↑j,con.left_inv,idp_con], diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 4cb2162f6..9a9a39f9c 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -17,8 +17,8 @@ open eq function lift structure is_equiv [class] {A B : Type} (f : A → B) := mk' :: (inv : B → A) - (right_inv : (f ∘ inv) ~ id) - (left_inv : (inv ∘ f) ~ id) + (right_inv : Πb, f (inv b) = b) + (left_inv : Πa, inv (f a) = a) (adj : Πx, right_inv (f x) = ap f (left_inv x)) attribute is_equiv.inv [quasireducible] @@ -66,44 +66,43 @@ namespace is_equiv section parameters {A B : Type} (f : A → B) (g : B → A) - (ret : f ∘ g ~ id) (sec : g ∘ f ~ id) + (ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a) - private definition adjointify_sect' : g ∘ f ~ id := - (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x) + private definition adjointify_left_inv' (a : A) : g (f a) = a := + ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a - private definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) := - (λ (a : A), - let fgretrfa := ap f (ap g (ret (f a))) in - let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in - let fgfa := f (g (f a)) in - let retrfa := ret (f a) in - have eq1 : ap f (sec a) = _, - from calc ap f (sec a) - = idp ⬝ ap f (sec a) : by rewrite idp_con - ... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a) : by rewrite con.right_inv - ... = ((ret fgfa)⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : by rewrite con_ap_eq_con - ... = ((ret fgfa)⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose - ... = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc, - have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)), - from !con_idp ⬝ eq1, - have eq3 : idp = _, - from calc idp - = (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : eq_inv_con_of_con_eq eq2 - ... = ((ap f (sec a))⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc' - ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite ap_inv - ... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con.assoc' - ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con - ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose - ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : by rewrite con.assoc' - ... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : by rewrite ap_con - ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc' - ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a) : by rewrite -ap_con, - have eq4 : ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a), - from eq_of_idp_eq_inv_con eq3, - eq4) + private definition adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) := + let fgretrfa := ap f (ap g (ret (f a))) in + let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in + let fgfa := f (g (f a)) in + let retrfa := ret (f a) in + have eq1 : ap f (sec a) = _, + from calc ap f (sec a) + = idp ⬝ ap f (sec a) : by rewrite idp_con + ... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a) : by rewrite con.right_inv + ... = ((ret fgfa)⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : by rewrite con_ap_eq_con + ... = ((ret fgfa)⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose + ... = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc, + have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)), + from !con_idp ⬝ eq1, + have eq3 : idp = _, + from calc idp + = (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : eq_inv_con_of_con_eq eq2 + ... = ((ap f (sec a))⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc' + ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite ap_inv + ... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con.assoc' + ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con + ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose + ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : by rewrite con.assoc' + ... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : by rewrite ap_con + ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc' + ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a) : by rewrite -ap_con, + have eq4 : ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a), + from eq_of_idp_eq_inv_con eq3, + eq4 definition adjointify [constructor] : is_equiv f := - is_equiv.mk f g ret adjointify_sect' adjointify_adj' + is_equiv.mk f g ret adjointify_left_inv' adjointify_adj' end -- Any function pointwise equal to an equivalence is an equivalence as well. @@ -174,11 +173,12 @@ namespace is_equiv definition equiv_rect_comp (P : B → Type) (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x := - calc equiv_rect f P df (f x) - = transport P (right_inv f (f x)) (df (f⁻¹ (f x))) : by esimp - ... = transport P (eq.ap f (left_inv f x)) (df (f⁻¹ (f x))) : by rewrite adj - ... = transport (P ∘ f) (left_inv f x) (df (f⁻¹ (f x))) : by rewrite -transport_compose - ... = df x : by rewrite (apd df (left_inv f x)) + calc + equiv_rect f P df (f x) + = right_inv f (f x) ▸ df (f⁻¹ (f x)) : by esimp + ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj + ... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -transport_compose + ... = df x : by rewrite (apd df (left_inv f x)) end @@ -229,12 +229,14 @@ namespace equiv variables {A B C : Type} protected definition MK [reducible] [constructor] (f : A → B) (g : B → A) - (right_inv : f ∘ g ~ id) (left_inv : g ∘ f ~ id) : A ≃ B := + (right_inv : Πb, f (g b) = b) (left_inv : Πa, g (f a) = a) : A ≃ B := equiv.mk f (adjointify f g right_inv left_inv) definition to_inv [reducible] [unfold 3] (f : A ≃ B) : B → A := f⁻¹ - definition to_right_inv [reducible] [unfold 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f - definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f + definition to_right_inv [reducible] [unfold 3] (f : A ≃ B) (b : B) : f (f⁻¹ b) = b := + right_inv f b + definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) (a : A) : f⁻¹ (f a) = a := + left_inv f a protected definition refl [refl] [constructor] : A ≃ A := equiv.mk id !is_equiv_id diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index e54a6f047..84644ebf7 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -169,15 +169,14 @@ section (λ b c p, eq.rec_on p idp)))) private definition isequiv_tgt_compose {A B : Type} - : @is_equiv (A → diagonal B) - (A → B) - (compose (pr₂ ∘ pr1)) := - @ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1) - (is_equiv.adjointify (pr2 ∘ pr1) - (λ x, sigma.mk (x , x) idp) (λx, idp) - (λ x, sigma.rec_on x - (λ xy, prod.rec_on xy - (λ b c p, eq.rec_on p idp)))) + : is_equiv (compose (pr₂ ∘ pr1) : (A → diagonal B) → (A → B)) := + begin + refine @ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1) _, + fapply adjointify, + { intro b, exact ⟨(b, b), idp⟩}, + { intro b, reflexivity}, + { intro a, induction a with q p, induction q, esimp at *, induction p, reflexivity} + end set_option class.conservative false theorem nondep_funext_from_ua {A : Type} {B : Type} diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 81f31f54d..7e114bd2e 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -190,7 +190,7 @@ namespace eq eq.rec_on p u -- This idiom makes the operation right associative. - notation p `▸` x := transport _ p x + infixr `▸` := transport _ definition cast [reducible] [unfold 3] {A B : Type} (p : A = B) (a : A) : B := p ▸ a diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index d3ead5838..38fd8bf1a 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -11,7 +11,7 @@ import .path .equiv open equiv is_equiv equiv.ops -variables {A A' : Type} {B : A → Type} {C : Πa, B a → Type} +variables {A A' : Type} {B B' : A → Type} {C : Πa, B a → Type} {a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄} {c : C a b} {c₂ : C a₂ b₂} @@ -240,4 +240,9 @@ namespace eq definition change_path (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ := by induction q;exact r + definition change_path_equiv (f : Π{a}, B a ≃ B' a) (r : b =[p] b₂) : f b =[p] f b₂ := + by induction r;constructor + + definition change_path_equiv' (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ := + (left_inv f b)⁻¹ ⬝po change_path_equiv (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂ end eq diff --git a/hott/types/cubical/cube.hlean b/hott/types/cubical/cube.hlean index c243a776c..8951aca56 100644 --- a/hott/types/cubical/cube.hlean +++ b/hott/types/cubical/cube.hlean @@ -20,29 +20,50 @@ namespace eq {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} (s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀) (s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂) - (s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁) - (s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁) (s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁) - (s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁), Type := + (s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁) + (s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁) + (s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁), Type := idc : cube ids ids ids ids ids ids - variables {A : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A} + variables {A B : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ a a' : A} {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂} {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂} {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂} {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} - {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} - {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} + {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} + {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} + {b₁ b₂ b₃ b₄ : B} definition idc [reducible] [constructor] := @cube.idc definition idcube [reducible] [constructor] (a : A) := @cube.idc A a definition rfl1 : cube s₁₁₀ s₁₁₀ vrfl vrfl vrfl vrfl := by induction s₁₁₀; exact idc - definition rfl2 : cube hrfl hrfl s₁₀₁ s₁₀₁ hrfl hrfl := by induction s₁₀₁; exact idc - definition rfl3 : cube vrfl vrfl hrfl hrfl s₁₁₀ s₁₁₀ := by induction s₁₁₀; exact idc + definition rfl2 : cube vrfl vrfl s₁₁₀ s₁₁₀ hrfl hrfl := by induction s₁₁₀; exact idc + definition rfl3 : cube hrfl hrfl hrfl hrfl s₁₀₁ s₁₀₁ := by induction s₁₀₁; exact idc + + definition eq_of_cube (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) : + transpose s₁₀₁⁻¹ᵛ ⬝h s₁₁₀ ⬝h transpose s₁₂₁ = + whisker_square (eq_bottom_of_square s₀₁₁) (eq_bottom_of_square s₂₁₁) idp idp s₁₁₂ := + by induction c; reflexivity + + --set_option pp.implicit true + definition eq_of_vdeg_cube {s s' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} + (c : cube s s' vrfl vrfl vrfl vrfl) : s = s' := + begin + induction s, exact eq_of_cube c + end + + definition square_pathover [unfold 7] + {f₁ : A → b₁ = b₂} {f₂ : A → b₃ = b₄} {f₃ : A → b₁ = b₃} {f₄ : A → b₂ = b₄} + {p : a = a'} + {q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)} {r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')} + (s : cube q r (vdeg_square (ap f₁ p)) (vdeg_square (ap f₂ p)) + (vdeg_square (ap f₃ p)) (vdeg_square (ap f₄ p))) : q =[p] r := + by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_cube s end eq diff --git a/hott/types/cubical/cubeover.hlean b/hott/types/cubical/cubeover.hlean index 9f721f624..56193a61c 100644 --- a/hott/types/cubical/cubeover.hlean +++ b/hott/types/cubical/cubeover.hlean @@ -21,11 +21,11 @@ namespace eq {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} - {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} - {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} - (c : cube s₁₁₀ s₁₁₂ s₁₀₁ s₁₂₁ s₀₁₁ s₂₁₁) + {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} + {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} + (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) {b₀₂₀ : B a₀₂₀} {b₂₀₀ : B a₂₀₀} {b₂₂₀ : B a₂₂₀} {b₀₀₂ : B a₀₀₂} {b₀₂₂ : B a₀₂₂} {b₂₀₂ : B a₂₀₂} {b₂₂₂ : B a₂₂₂} {q₁₀₀ : pathover B b₀₀₀ p₁₀₀ b₂₀₀} {q₀₁₀ : pathover B b₀₀₀ p₀₁₀ b₀₂₀} @@ -36,10 +36,10 @@ namespace eq {q₂₁₂ : pathover B b₂₀₂ p₂₁₂ b₂₂₂} {q₂₂₁ : pathover B b₂₂₀ p₂₂₁ b₂₂₂} (t₁₁₀ : squareover B s₁₁₀ q₀₁₀ q₂₁₀ q₁₀₀ q₁₂₀) (t₁₁₂ : squareover B s₁₁₂ q₀₁₂ q₂₁₂ q₁₀₂ q₁₂₂) - (t₁₀₁ : squareover B s₁₀₁ q₁₀₀ q₁₀₂ q₀₀₁ q₂₀₁) - (t₁₂₁ : squareover B s₁₂₁ q₁₂₀ q₁₂₂ q₀₂₁ q₂₂₁) (t₀₁₁ : squareover B s₀₁₁ q₀₁₀ q₀₁₂ q₀₀₁ q₀₂₁) - (t₂₁₁ : squareover B s₂₁₁ q₂₁₀ q₂₁₂ q₂₀₁ q₂₂₁), Type := + (t₂₁₁ : squareover B s₂₁₁ q₂₁₀ q₂₁₂ q₂₀₁ q₂₂₁) + (t₁₀₁ : squareover B s₁₀₁ q₁₀₀ q₁₀₂ q₀₀₁ q₂₀₁) + (t₁₂₁ : squareover B s₁₂₁ q₁₂₀ q₁₂₂ q₀₂₁ q₂₂₁), Type := idcubeo : cubeover B idc idso idso idso idso idso idso diff --git a/hott/types/cubical/square.hlean b/hott/types/cubical/square.hlean index cb279f8fc..8c18d0f4c 100644 --- a/hott/types/cubical/square.hlean +++ b/hott/types/cubical/square.hlean @@ -11,9 +11,9 @@ open eq equiv is_equiv namespace eq variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} - /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ - {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} - /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ + /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ + {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} + /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ @@ -134,6 +134,10 @@ namespace eq definition square_of_eq_top (r : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹) : square p₁₀ p₁₂ p₀₁ p₂₁ := by induction p₂₁; induction p₁₂; esimp at r;induction r;induction p₁₀;exact ids + definition eq_bottom_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : p₁₂ = p₀₁⁻¹ ⬝ p₁₀ ⬝ p₂₁ := + by induction s₁₁; apply idp + definition square_equiv_eq [constructor] (t : a₀₀ = a₀₂) (b : a₂₀ = a₂₂) (l : a₀₀ = a₂₀) (r : a₀₂ = a₂₂) : square t b l r ≃ t ⬝ r = l ⬝ b := begin @@ -157,7 +161,8 @@ namespace eq definition eq_of_vdeg_square [reducible] {p q : a = a'} (s : square p q idp idp) : p = q := to_fun !vdeg_square_equiv' s - definition top_deg_square (l : a₁ = a₂) (b : a₂ = a₃) (r : a₄ = a₃) : square (l ⬝ b ⬝ r⁻¹) b l r := + definition top_deg_square (l : a₁ = a₂) (b : a₂ = a₃) (r : a₄ = a₃) + : square (l ⬝ b ⬝ r⁻¹) b l r := by induction r;induction b;induction l;constructor /- @@ -186,7 +191,7 @@ namespace eq -- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp - definition pathover_eq [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} + definition eq_pathover [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) : q =[p] r := by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s @@ -197,17 +202,17 @@ namespace eq /- interaction of equivalences with operations on squares -/ - definition pathover_eq_equiv_square [constructor] {f g : A → B} + definition eq_pathover_equiv_square [constructor] {f g : A → B} (p : a = a') (q : f a = g a) (r : f a' = g a') : q =[p] r ≃ square q r (ap f p) (ap g p) := equiv.MK square_of_pathover - pathover_eq + eq_pathover begin - intro s, induction p, esimp [square_of_pathover,pathover_eq], + intro s, induction p, esimp [square_of_pathover,eq_pathover], exact ap vdeg_square (to_right_inv !pathover_idp (eq_of_vdeg_square s)) ⬝ to_left_inv !vdeg_square_equiv s end begin - intro s, induction p, esimp [square_of_pathover,pathover_eq], + intro s, induction p, esimp [square_of_pathover,eq_pathover], exact ap pathover_idp_of_eq (to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s)) ⬝ to_left_inv !pathover_idp s end @@ -267,17 +272,17 @@ namespace eq -- the following definition is very slow, maybe it's interesting to see why? - -- definition pathover_eq_equiv_square' {f g : A → B}(p : a = a') (q : f a = g a) (r : f a' = g a') + -- definition eq_pathover_equiv_square' {f g : A → B}(p : a = a') (q : f a = g a) (r : f a' = g a') -- : square q r (ap f p) (ap g p) ≃ q =[p] r := - -- equiv.MK pathover_eq + -- equiv.MK eq_pathover -- square_of_pathover -- (λs, begin - -- induction p, rewrite [↑[square_of_pathover,pathover_eq], + -- induction p, rewrite [↑[square_of_pathover,eq_pathover], -- to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s), -- to_left_inv !pathover_idp s] -- end) -- (λs, begin - -- induction p, rewrite [↑[square_of_pathover,pathover_eq],▸*, + -- induction p, rewrite [↑[square_of_pathover,eq_pathover],▸*, -- to_right_inv !(@pathover_idp A) (eq_of_vdeg_square s), -- to_left_inv !vdeg_square_equiv s] -- end) @@ -345,6 +350,11 @@ namespace eq --we can also do the other recursors (tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed + definition whisker_square [unfold 14 15 16 17] (r₁₀ : p₁₀ = p₁₀') (r₁₂ : p₁₂ = p₁₂') + (r₀₁ : p₀₁ = p₀₁') (r₂₁ : p₂₁ = p₂₁') (s : square p₁₀ p₁₂ p₀₁ p₂₁) + : square p₁₀' p₁₂' p₀₁' p₂₁' := + by induction r₁₀; induction r₁₂; induction r₀₁; induction r₂₁; exact s + /- squares commute with some operations on 2-paths -/ definition square_inv2 {p₁ p₂ p₃ p₄ : a = a'} diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index f53196dc7..c3cb79d91 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -220,7 +220,7 @@ namespace eq /- Path operations are equivalences -/ - definition is_equiv_eq_inverse (a₁ a₂ : A) : is_equiv (@inverse A a₁ a₂) := + definition is_equiv_eq_inverse (a₁ a₂ : A) : is_equiv (inverse : a₁ = a₂ → a₂ = a₁) := is_equiv.mk inverse inverse inv_inv inv_inv (λp, eq.rec_on p idp) local attribute is_equiv_eq_inverse [instance] @@ -253,7 +253,7 @@ namespace eq equiv.trans (equiv_eq_closed_left a₃ p) (equiv_eq_closed_right a₂ q) definition is_equiv_whisker_left (p : a₁ = a₂) (q r : a₂ = a₃) - : is_equiv (@whisker_left A a₁ a₂ a₃ p q r) := + : is_equiv (whisker_left p : q = r → p ⬝ q = p ⬝ r) := begin fapply adjointify, {intro s, apply (!cancel_left s)}, @@ -273,7 +273,7 @@ namespace eq equiv.mk _ !is_equiv_whisker_left definition is_equiv_whisker_right {p q : a₁ = a₂} (r : a₂ = a₃) - : is_equiv (λs, @whisker_right A a₁ a₂ a₃ p q s r) := + : is_equiv (λs, whisker_right s r : p = q → p ⬝ r = q ⬝ r) := begin fapply adjointify, {intro s, apply (!cancel_right s)}, diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 18484931f..fbf1e87c3 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -9,7 +9,7 @@ Theorems about the types equiv and is_equiv import .fiber .arrow arity .hprop_trunc -open eq is_trunc sigma sigma.ops pi fiber function equiv +open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops namespace is_equiv variables {A B : Type} (f : A → B) [H : is_equiv f] @@ -18,14 +18,16 @@ namespace is_equiv definition is_contr_fiber_of_is_equiv [instance] (b : B) : is_contr (fiber f b) := is_contr.mk (fiber.mk (f⁻¹ b) (right_inv f b)) - (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc - right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc - ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose - ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv - ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con))) + (λz, fiber.rec_on z (λa p, + fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc + right_inv f b + = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc + ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose + ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv + ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con))) definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ~ id) := begin @@ -54,12 +56,12 @@ namespace is_equiv equiv.MK (λH, ⟨inv f, right_inv f, left_inv f, adj f⟩) (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2) (λp, begin - cases p with p1 p2, - cases p2 with p21 p22, - cases p22 with p221 p222, - apply idp + induction p with p1 p2, + induction p2 with p21 p22, + induction p22 with p221 p222, + reflexivity end) - (λH, is_equiv.rec_on H (λH1 H2 H3 H4, idp)) + (λH, by induction H; reflexivity) protected definition sigma_char' : (is_equiv f) ≃ (Σ(u : Σ(g : B → A), f ∘ g ~ id), Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) := @@ -116,7 +118,8 @@ namespace equiv definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' := by (cases f; cases f'; apply (equiv_mk_eq p)) - protected definition equiv.sigma_char (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f := + protected definition equiv.sigma_char [constructor] + (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f := begin fapply equiv.MK, {intro F, exact ⟨to_fun F, to_is_equiv F⟩}, @@ -143,4 +146,15 @@ namespace equiv {intro p, cases p, cases f with f H, apply ap (ap (equiv.mk f)), apply is_hset.elim} end + definition equiv_pathover {A : Type} {a a' : A} (p : a = a') + {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') + (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g := + begin + fapply change_path_equiv', + { intro a, apply equiv.sigma_char}, + { fapply sigma_pathover, + esimp, apply arrow_pathover, exact r, + apply is_hprop.elimo} + end + end equiv diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean index 44060c3d3..4c5c4ec15 100644 --- a/hott/types/hprop_trunc.hlean +++ b/hott/types/hprop_trunc.hlean @@ -31,8 +31,8 @@ namespace is_trunc { intro H x y, apply is_trunc_eq}, { intro H, cases H, apply idp}, { intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b, - esimp [is_trunc_eq], esimp[compose,is_trunc_succ_intro], - generalize (P a b), intro H, cases H, apply idp}, + change is_trunc.mk (to_internal n (a = b)) = P a b, + induction (P a b), apply idp}, end definition is_hprop_is_trunc [instance] (n : trunc_index) : diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 2026cd0dd..f5b96d7ee 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -18,11 +18,15 @@ namespace pi /- Paths -/ - /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g]. + /- + Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values + in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g]. - This equivalence, however, is just the combination of [apd10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path: -/ + This equivalence, however, is just the combination of [apd10] and function extensionality + [funext], and as such, [eq_of_homotopy] - /- Now we show how these things compute. -/ + Now we show how these things compute. + -/ definition apd10_eq_of_homotopy (h : f ~ g) : apd10 (eq_of_homotopy h) ~ h := apd10 (right_inv apd10 h) @@ -33,17 +37,19 @@ namespace pi definition eq_of_homotopy_idp (f : Πa, B a) : eq_of_homotopy (λx : A, refl (f x)) = refl f := !eq_of_homotopy_eta - /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/ + /- + The identification of the path space of a dependent function space, + up to equivalence, is of course just funext. + -/ definition eq_equiv_homotopy (f g : Πx, B x) : (f = g) ≃ (f ~ g) := - equiv.mk _ !is_equiv_apd + equiv.mk apd10 _ - definition is_equiv_eq_of_homotopy [instance] (f g : Πx, B x) - : is_equiv (@eq_of_homotopy _ _ f g) := - is_equiv_inv apd10 + definition is_equiv_eq_of_homotopy (f g : Πx, B x) : is_equiv (@eq_of_homotopy _ _ f g) := + _ definition homotopy_equiv_eq (f g : Πx, B x) : (f ~ g) ≃ (f = g) := - equiv.mk _ !is_equiv_eq_of_homotopy + equiv.mk eq_of_homotopy _ /- Transport -/ @@ -56,7 +62,7 @@ namespace pi /- A special case of [transport_pi] where the type [B] does not depend on [A], and so it is just a fixed type [B]. -/ definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A') - : (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) := + : (transport _ p f) b = p ▸ (f b) := eq.rec_on p idp /- Pathovers -/ @@ -147,10 +153,11 @@ namespace pi /- The functoriality of [forall] is slightly subtle: it is contravariant in the domain type and covariant in the codomain, but the codomain is dependent on the domain. -/ - definition pi_functor : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a'))) + definition pi_functor [unfold-full] : (Π(a:A), B a) → (Π(a':A'), B' a') := λg a', f1 a' (g (f0 a')) definition ap_pi_functor {g g' : Π(a:A), B a} (h : g ~ g') - : ap (pi_functor f0 f1) (eq_of_homotopy h) = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) := + : ap (pi_functor f0 f1) (eq_of_homotopy h) + = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) := begin apply (equiv_rect (@apd10 A B g g')), intro p, clear h, cases p, @@ -161,32 +168,25 @@ namespace pi /- Equivalences -/ - definition is_equiv_pi_functor [instance] - [H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] - : is_equiv (pi_functor f0 f1) := + definition is_equiv_pi_functor [instance] [H0 : is_equiv f0] + [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : is_equiv (pi_functor f0 f1) := begin apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹ (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))), - intro h, apply eq_of_homotopy, - unfold pi_functor, unfold function.compose, unfold function.id, begin - intro a', - apply (tr_rev _ (adj f0 a')), - apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (left_inv f0 a') _)), - apply (tr_rev (λx, x = h a') (fn_tr_eq_tr_fn _ f1 _)), unfold function.compose, - apply (tr_rev (λx, left_inv f0 a' ▸ x = h a') (right_inv (f1 _) _)), unfold function.id, + intro h, apply eq_of_homotopy, intro a', esimp, + rewrite [adj f0 a',-transport_compose,fn_tr_eq_tr_fn _ f1,right_inv (f1 _)], apply apd end, begin - intro h, - apply eq_of_homotopy, intro a, - apply (tr_rev (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)), unfold function.id, + intro h, apply eq_of_homotopy, intro a, esimp, + rewrite [left_inv (f1 _)], apply apd end end - definition pi_equiv_pi_of_is_equiv [H : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] - : (Πa, B a) ≃ (Πa', B' a') := + definition pi_equiv_pi_of_is_equiv [H : is_equiv f0] + [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : (Πa, B a) ≃ (Πa', B' a') := equiv.mk (pi_functor f0 f1) _ definition pi_equiv_pi (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a')) diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index c3e13f645..e255e8e91 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -67,13 +67,15 @@ namespace pointed -- | Iterated_loop_space A 0 := A -- | Iterated_loop_space A (n+1) := Iterated_loop_space (Loop_space A) n - definition Iterated_loop_space [reducible] (n : ℕ) (A : Pointed) : Pointed := + definition Iterated_loop_space [unfold 1] [reducible] (n : ℕ) (A : Pointed) : Pointed := nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A prefix `Ω`:(max+5) := Loop_space notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space n A - definition iterated_loop_space (A : Type) [H : pointed A] (n : ℕ) : Type := + definition refln [constructor] {A : Pointed} {n : ℕ} : Ω[n] A := pt + + definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type := Ω[n] (pointed.mk' A) open equiv.ops @@ -202,11 +204,11 @@ namespace pointed { esimp, exact !con.left_inv⁻¹}}, end - definition apn [constructor] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := + definition apn [unfold 3] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := begin revert A B f, induction n with n IH, { intros A B f, exact f}, - { intros A B f, esimp [Iterated_loop_space], apply IH (Ω A), + { intros A B f, esimp, apply IH (Ω A), { esimp, fconstructor, intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt, esimp, apply con.left_inv}} diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 4ae941aa3..e871109bd 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -9,10 +9,9 @@ Theorems about sigma-types (dependent sums) import types.prod -open eq sigma sigma.ops equiv is_equiv +open eq sigma sigma.ops equiv is_equiv function namespace sigma - local infixr ∘ := function.compose --remove variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a} diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 62f191dec..66a7b421a 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -31,8 +31,8 @@ namespace is_trunc fapply equiv.MK, { intro A, exact (⟨carrier A, struct A⟩)}, { intro S, exact (trunctype.mk S.1 S.2)}, - { intro S, apply (sigma.rec_on S), intro S1 S2, apply idp}, - { intro A, apply (trunctype.rec_on A), intro A1 A2, apply idp}, + { intro S, induction S with S1 S2, reflexivity}, + { intro A, induction A with A1 A2, reflexivity}, end definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) : @@ -47,7 +47,7 @@ namespace is_trunc definition is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B] (Hn : -1 ≤ n) : is_trunc n A := begin - cases n with n, + induction n with n, {exact !empty.elim Hn}, {apply is_trunc_succ_intro, intro a a', fapply @is_trunc_is_equiv_closed_rev _ _ n (ap f)} @@ -57,18 +57,18 @@ namespace is_trunc (n : trunc_index) [HA : is_trunc n A] : is_trunc n B := begin revert A B f Hf HA, - eapply (trunc_index.rec_on n), - { clear n, intro A B f Hf HA, cases Hf with g ε, fapply is_contr.mk, + induction n with n IH, + { intro A B f Hf HA, induction Hf with g ε, fapply is_contr.mk, { exact f (center A)}, { intro b, apply concat, { apply (ap f), exact (center_eq (g b))}, { apply ε}}}, - { clear n, intro n IH A B f Hf HA, cases Hf with g ε, + { intro A B f Hf HA, induction Hf with g ε, apply is_trunc_succ_intro, intro b b', fapply (IH (g b = g b')), { intro q, exact ((ε b)⁻¹ ⬝ ap f q ⬝ ε b')}, { apply (is_retraction.mk (ap g)), - { intro p, cases p, {rewrite [↑ap, con.left_inv]}}}, + { intro p, induction p, {rewrite [↑ap, con.left_inv]}}}, { apply is_trunc_eq}} end @@ -82,7 +82,7 @@ namespace is_trunc {apply equiv.symm, apply trunctype_eq_equiv}, fapply is_trunc_equiv_closed, {apply equiv.symm, apply eq_equiv_equiv}, - cases n, + induction n, {apply @is_contr_of_inhabited_hprop, {apply is_trunc_is_embedding_closed, {apply is_embedding_to_fun} , @@ -143,7 +143,7 @@ namespace is_trunc begin apply is_trunc_succ_intro, intros a a', apply is_trunc_of_imp_is_trunc_of_leq Hn, intro p, - cases p, apply Hp + induction p, apply Hp end definition is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) : @@ -176,7 +176,7 @@ namespace is_trunc definition is_trunc_iff_is_contr_loop (n : ℕ) (A : Type) : is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) := begin - cases n with n, + induction n with n, { esimp [sub_two,Iterated_loop_space], apply iff.intro, intro H a, exact is_contr_of_inhabited_hprop a, intro H, apply is_hprop_of_imp_is_contr, exact H}, @@ -193,7 +193,7 @@ namespace trunc protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' := begin - intro p, cases p, apply (trunc.rec_on aa), + intro p, induction p, apply (trunc.rec_on aa), intro a, esimp [trunc.code,trunc.rec_on], exact (tr idp) end @@ -212,8 +212,10 @@ namespace trunc { apply trunc.decode}, { eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa), intro a a' x, esimp [trunc.code, trunc.rec_on] at x, - apply (trunc.rec_on x), intro p, cases p, exact idp}, - { intro p, cases p, apply (trunc.rec_on aa), intro a, exact idp}, + refine (@trunc.rec_on n _ _ x _ _), + intro x, apply is_trunc_eq, + intro p, induction p, reflexivity}, + { intro p, induction p, apply (trunc.rec_on aa), intro a, exact idp}, end definition tr_eq_tr_equiv (n : trunc_index) (a a' : A) @@ -226,7 +228,7 @@ namespace trunc revert A m H, eapply (trunc_index.rec_on n), { clear n, intro A m H, apply is_contr_equiv_closed, { apply equiv_trunc, apply (@is_trunc_of_leq _ -2), exact unit.star} }, - { clear n, intro n IH A m H, cases m with m, + { clear n, intro n IH A m H, induction m with m, { apply (@is_trunc_of_leq _ -2), exact unit.star}, { apply is_trunc_succ_intro, intro aa aa', apply (@trunc.rec_on _ _ _ aa (λy, !is_trunc_succ_of_is_hprop)), diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean index b4fdf00d3..eaa162e8a 100644 --- a/tests/lean/hott/433.hlean +++ b/tests/lean/hott/433.hlean @@ -112,10 +112,9 @@ namespace pi rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _), rewrite (right_inv (f1 _) _), apply apd, - intro h, beta, + intro h, apply eq_of_homotopy, intro a, esimp, apply (transport_V (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)), - esimp [function.id], apply apd end diff --git a/tests/lean/hott/unfold_test.hlean b/tests/lean/hott/unfold_test.hlean index 952e8a380..b5e398fcf 100644 --- a/tests/lean/hott/unfold_test.hlean +++ b/tests/lean/hott/unfold_test.hlean @@ -26,7 +26,7 @@ section apply sorry, apply sorry, { - rewrite [↑e_closure.elim, ↑ap_e_closure_elim_h, ap_con (ap h)], + rewrite [▸*, ap_con (ap h)], refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _, rewrite [con_inv,inv_inv,-inv2_inv], exact !ap_inv2 ⬝v square_inv2 v_0