From 3d0d0947d6a24d36cdb93993699b22e09891b8ce Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 7 Sep 2018 16:30:58 +0200 Subject: [PATCH] various cleanup changes in library some of the changes are backported from the hott3 library pi_pathover and pi_pathover' are interchanged (same for variants and for sigma) various definitions received explicit arguments: pinverse and eq_equiv_homotopy and ***.sigma_char eq_of_fn_eq_fn is renamed to inj in definitions about higher loop spaces and homotopy groups, the natural number arguments are now consistently before the type arguments --- hott/algebra/category/category.hlean | 2 +- .../category/constructions/functor.hlean | 64 +++++++++---------- .../algebra/category/functor/attributes.hlean | 8 +-- .../category/functor/equivalence.hlean | 2 +- hott/algebra/group_theory.hlean | 2 +- hott/algebra/homotopy_group.hlean | 62 +++++++++--------- hott/cubical/square.hlean | 2 +- hott/cubical/squareover.hlean | 2 +- hott/eq2.hlean | 12 ++-- hott/hit/coeq.hlean | 2 +- hott/hit/colimit.hlean | 4 +- hott/hit/groupoid_quotient.hlean | 2 +- hott/hit/prop_trunc.hlean | 2 +- hott/hit/pushout.hlean | 2 +- hott/hit/quotient.hlean | 4 +- hott/hit/set_quotient.hlean | 2 +- hott/hit/trunc.hlean | 4 +- hott/hit/two_quotient.hlean | 2 +- hott/homotopy/EM.hlean | 2 +- hott/homotopy/LES_of_homotopy_groups.hlean | 24 +++---- hott/homotopy/circle.hlean | 14 ++-- hott/homotopy/connectedness.hlean | 8 +-- hott/homotopy/cylinder.hlean | 2 +- hott/homotopy/freudenthal.hlean | 56 ++++++++-------- hott/homotopy/homotopy_group.hlean | 14 ++-- hott/homotopy/interval.hlean | 2 +- hott/homotopy/join.hlean | 2 +- hott/homotopy/smash.hlean | 4 +- hott/homotopy/sphere.hlean | 2 +- hott/homotopy/sphere2.hlean | 4 +- hott/homotopy/susp.hlean | 4 +- hott/init/equiv.hlean | 39 ++++++----- hott/init/funext.hlean | 2 +- hott/init/trunc.hlean | 2 - hott/init/ua.hlean | 2 +- hott/types/equiv.hlean | 16 ++--- hott/types/fiber.hlean | 6 +- hott/types/lift.hlean | 6 +- hott/types/pi.hlean | 12 ++-- hott/types/pointed.hlean | 54 +++++++--------- hott/types/pointed2.hlean | 18 ++---- hott/types/sigma.hlean | 5 +- hott/types/trunc.hlean | 10 +-- hott/types/unit.hlean | 2 +- tests/lean/extra/755.hlean | 2 +- 45 files changed, 239 insertions(+), 255 deletions(-) diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index 9b18f7e16..43b13daa6 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -120,7 +120,7 @@ namespace category (q : Πa b c g f, cast p (@comp ob C a b c g f) = @comp ob D a b c (cast p g) (cast p f)) : C = D := begin - apply eq_of_fn_eq_fn !category.sigma_char, + apply inj !category.sigma_char, fapply sigma_eq, { induction C, induction D, esimp, exact precategory_eq @p q}, { unfold is_univalent, apply is_prop.elimo}, diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index a115924fa..505ac6b37 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -383,7 +383,7 @@ namespace functor { intro G H I η θ, reflexivity}, end - definition faithful_precomposition_functor [instance] + definition faithful_precomposition_functor [instance] {C D E} {H : C ⇒ D} [Hs : essentially_surjective H] : faithful (precomposition_functor E H) := begin intro F G γ δ Hγδ, apply nat_trans_eq, intro b, @@ -414,7 +414,7 @@ namespace functor begin induction Hs b with Hb, induction Hb with a0 h, fconstructor, exact G h ∘ γ a0 ∘ F h⁻¹ⁱ, intro a f, - induction Hf (to_hom (f ⬝i h⁻¹ⁱ)) with k Ek, + induction Hf (to_hom (f ⬝i h⁻¹ⁱ)) with k Ek, have is_iso (H k), by rewrite Ek; apply _, refine _ ⬝ !assoc⁻¹, refine _ ⬝ ap (λ x, x ∘ F f) !assoc⁻¹, refine _ ⬝ !assoc, refine _ ⬝ ap (λ x, (G f⁻¹ⁱ ∘ G h) ∘ x) !assoc, @@ -425,24 +425,24 @@ namespace functor --TODO speed this up private definition fully_faithful_precomposition_naturality {b b' : carrier D} - (f : hom b b') : to_fun_hom G f ∘ (fully_faithful_precomposition_functor_pair γ b).1 + (f : hom b b') : to_fun_hom G f ∘ (fully_faithful_precomposition_functor_pair γ b).1 = (fully_faithful_precomposition_functor_pair γ b').1 ∘ to_fun_hom F f := begin esimp[fully_faithful_precomposition_functor_pair], induction Hs b with Hb, induction Hb with a h, induction Hs b' with Hb', induction Hb' with a' h', - induction Hf (to_hom h'⁻¹ⁱ ∘ f ∘ to_hom h) with k Ek, + induction Hf (to_hom h'⁻¹ⁱ ∘ f ∘ to_hom h) with k Ek, apply concat, apply assoc, apply concat, apply ap (λ x, x ∘ _), - apply concat, apply !respect_comp⁻¹, - apply concat, apply ap (λ x, to_fun_hom G x), apply inverse, + apply concat, apply !respect_comp⁻¹, + apply concat, apply ap (λ x, to_fun_hom G x), apply inverse, apply comp_eq_of_eq_inverse_comp, apply Ek, apply respect_comp, - apply concat, apply !assoc⁻¹, - apply concat, apply ap (λ x, _ ∘ x), apply concat, apply assoc, - apply concat, apply ap (λ x, x ∘ _), apply naturality γ, apply !assoc⁻¹, - apply concat, apply ap (λ x, _ ∘ _ ∘ x), apply concat, esimp, apply !respect_comp⁻¹, - apply concat, apply ap (λ x, to_fun_hom F x), - apply comp_inverse_eq_of_eq_comp, apply Ek ⬝ !assoc, apply respect_comp, + apply concat, apply !assoc⁻¹, + apply concat, apply ap (λ x, _ ∘ x), apply concat, apply assoc, + apply concat, apply ap (λ x, x ∘ _), apply naturality γ, apply !assoc⁻¹, + apply concat, apply ap (λ x, _ ∘ _ ∘ x), apply concat, esimp, apply !respect_comp⁻¹, + apply concat, apply ap (λ x, to_fun_hom F x), + apply comp_inverse_eq_of_eq_comp, apply Ek ⬝ !assoc, apply respect_comp, apply concat, apply assoc, apply concat, apply assoc, apply ap (λ x, x ∘ _) !assoc⁻¹ end @@ -454,13 +454,13 @@ namespace functor { apply faithful_precomposition_functor }, { intro F G γ, esimp at *, fapply image.mk, fconstructor, - { intro b, apply (fully_faithful_precomposition_functor_pair γ b).1 }, + { intro b, apply (fully_faithful_precomposition_functor_pair γ b).1 }, { intro b b' f, apply fully_faithful_precomposition_naturality }, { fapply nat_trans_eq, intro a, esimp, apply inverse, induction (fully_faithful_precomposition_functor_pair γ (to_fun_ob H a)) with g Hg, esimp, apply concat, apply Hg a (iso.refl (H a)), esimp, - apply concat, apply ap (λ x, x ∘ _), apply respect_id, apply concat, apply id_left, + apply concat, apply ap (λ x, x ∘ _), apply respect_id, apply concat, apply id_left, apply concat, apply ap (λ x, _ ∘ x), apply respect_id, apply id_right } } end @@ -480,7 +480,7 @@ namespace functor structure essentially_surj_precomp_X (b : carrier B) : Type := (c : carrier C) (k : Π (a : carrier A) (h : H a ≅ b), F a ≅ c) - (k_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h + (k_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h → to_hom (k a' h') ∘ to_fun_hom F f = to_hom (k a h)) local abbreviation X := essentially_surj_precomp_X local abbreviation X.mk [constructor] := @essentially_surj_precomp_X.mk @@ -493,9 +493,9 @@ namespace functor {k : Π (a : carrier A) (h : H a ≅ b), F a ≅ c} {k' : Π (a : carrier A) (h : H a ≅ b), F a ≅ c'} (q : Π (a : carrier A) (h : H a ≅ b), to_hom (k a h ⬝i iso_of_eq p) = to_hom (k' a h)) - {k_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h + {k_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h → to_hom (k a' h') ∘ to_fun_hom F f = to_hom (k a h)} - {k'_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h + {k'_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h → to_hom (k' a' h') ∘ to_fun_hom F f = to_hom (k' a h)} include c c' p k k' q @@ -503,7 +503,7 @@ namespace functor begin cases p, assert q' : k = k', - { apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro h, + { apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro h, apply iso_eq, apply !id_left⁻¹ ⬝ q a h }, cases q', apply ap (essentially_surj_precomp_X.mk c' k'), @@ -541,10 +541,10 @@ namespace functor { intro a h, apply to_fun_iso F, apply reflect_iso H, exact h ⬝i Ha0⁻¹ⁱ }, { intros a a' h h' f HH, - apply concat, apply !respect_comp⁻¹, apply ap (to_fun_hom F), + apply concat, apply !respect_comp⁻¹, apply ap (to_fun_hom F), esimp, rewrite [-HH], - apply concat, apply ap (λ x, _ ∘ x), apply inverse, apply left_inv (to_fun_hom H), - apply concat, apply !hom_inv_respect_comp⁻¹, apply ap (hom_inv H), + apply concat, apply ap (λ x, _ ∘ x), apply inverse, apply left_inv (to_fun_hom H), + apply concat, apply !hom_inv_respect_comp⁻¹, apply ap (hom_inv H), apply !assoc⁻¹ } end local abbreviation G0 [reducible] := λ (b), X.c (X_inh b) @@ -626,37 +626,37 @@ namespace functor apply concat, apply ap (λ x, _ ∘ x), apply right_inv (to_fun_hom H), apply comp_inverse_cancel_left }, fapply Y.mk, - { refine to_hom (k b' a0' h0') ∘ _ ∘ to_hom (k b a0 h0)⁻¹ⁱ, + { refine to_hom (k b' a0' h0') ∘ _ ∘ to_hom (k b a0 h0)⁻¹ⁱ, apply to_fun_hom F, apply l0Hl0.1 }, { intros a a' h h' l Hl, esimp, apply inverse, assert mHm : Σ m, to_hom h0 ∘ to_fun_hom H m = to_hom h, - { fconstructor, apply hom_inv, apply He.1, exact to_hom h0⁻¹ⁱ ∘ to_hom h, + { fconstructor, apply hom_inv, apply He.1, exact to_hom h0⁻¹ⁱ ∘ to_hom h, apply concat, apply ap (λ x, _ ∘ x), apply right_inv (to_fun_hom H), apply comp_inverse_cancel_left }, assert m'Hm' : Σ m', to_hom h0' ∘ to_fun_hom H m' = to_hom h', - { fconstructor, apply hom_inv, apply He.1, exact to_hom h0'⁻¹ⁱ ∘ to_hom h', + { fconstructor, apply hom_inv, apply He.1, exact to_hom h0'⁻¹ⁱ ∘ to_hom h', apply concat, apply ap (λ x, _ ∘ x), apply right_inv (to_fun_hom H), apply comp_inverse_cancel_left }, assert m'l0lm : l0Hl0.1 ∘ mHm.1 = m'Hm'.1 ∘ l, { apply faithful_of_fully_faithful, apply He.1, apply concat, apply respect_comp, apply comp.cancel_left (to_hom h0'), apply inverse, - apply concat, apply ap (λ x, _ ∘ x), apply respect_comp, + apply concat, apply ap (λ x, _ ∘ x), apply respect_comp, apply concat, apply assoc, apply concat, apply ap (λ x, x ∘ _), apply m'Hm'.2, - apply concat, apply Hl, + apply concat, apply Hl, apply concat, apply ap (λ x, _ ∘ x), apply mHm.2⁻¹, apply concat, apply assoc, apply concat, apply ap (λ x, x ∘ _), apply l0Hl0.2⁻¹, apply !assoc⁻¹ }, apply concat, apply !assoc⁻¹, - apply concat, apply ap (λ x, _ ∘ x), apply !assoc⁻¹, - apply concat, apply ap (λ x, _ ∘ _ ∘ x), apply inverse_comp_eq_of_eq_comp, + apply concat, apply ap (λ x, _ ∘ x), apply !assoc⁻¹, + apply concat, apply ap (λ x, _ ∘ _ ∘ x), apply inverse_comp_eq_of_eq_comp, apply inverse, apply k_coh b h h0, apply mHm.2, - apply concat, apply ap (λ x, _ ∘ x), apply concat, apply !respect_comp⁻¹, + apply concat, apply ap (λ x, _ ∘ x), apply concat, apply !respect_comp⁻¹, apply concat, apply ap (to_fun_hom F), apply m'l0lm, apply respect_comp, apply concat, apply assoc, apply ap (λ x, x ∘ _), apply k_coh, apply m'Hm'.2 } end - + private definition G_hom [constructor] := λ {b b'} (f : hom b b'), Y.g (Y_inh f) private definition G_hom_coh := λ {b b'} (f : hom b b'), @essentially_surj_precomp_Y.Hg b b' f (Y_inh f) @@ -712,7 +712,7 @@ namespace functor fconstructor, { exact F a0 }, { intro a h, apply to_fun_iso F, apply reflect_iso, apply He.1, exact h }, - { intro a a' h h' f l, esimp, + { intro a a' h h' f l, esimp, apply concat, apply !respect_comp⁻¹, apply ap (to_fun_hom F), apply inverse, apply concat, apply ap (hom_inv H) l⁻¹, apply concat, apply hom_inv_respect_comp, apply ap (λ x, _ ∘ x), apply left_inv } @@ -739,7 +739,7 @@ namespace functor apply concat, apply assoc, apply concat, apply ap (λ x, x ∘ _), apply X_phi_hom_of_eq, esimp[XF], refine !respect_comp⁻¹ ⬝ ap (to_fun_hom F) _ ⬝ !respect_comp, - apply eq_of_fn_eq_fn' (to_fun_hom H), + apply inj' (to_fun_hom H), refine !respect_comp ⬝ _ ⬝ !respect_comp⁻¹, apply concat, apply ap (λ x, x ∘ _) !(right_inv (to_fun_hom H)), apply concat, rotate 1, apply ap (λ x, _ ∘ x) !(right_inv (to_fun_hom H))⁻¹, diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean index b42cb9f08..3d5ebd6a8 100644 --- a/hott/algebra/category/functor/attributes.hlean +++ b/hott/algebra/category/functor/attributes.hlean @@ -43,14 +43,14 @@ namespace category definition hom_inv_respect_id (F : C ⇒ D) [H : fully_faithful F] (c : C) : hom_inv F (ID (F c)) = id := begin - apply eq_of_fn_eq_fn' (to_fun_hom F), + apply inj' (to_fun_hom F), exact !(right_inv (to_fun_hom F)) ⬝ !respect_id⁻¹, end definition hom_inv_respect_comp (F : C ⇒ D) [H : fully_faithful F] {a b c : C} (g : F b ⟶ F c) (f : F a ⟶ F b) : hom_inv F (g ∘ f) = hom_inv F g ∘ hom_inv F f := begin - apply eq_of_fn_eq_fn' (to_fun_hom F), + apply inj' (to_fun_hom F), refine !(right_inv (to_fun_hom F)) ⬝ _ ⬝ !respect_comp⁻¹, rewrite [right_inv (to_fun_hom F), right_inv (to_fun_hom F)], end @@ -60,9 +60,9 @@ namespace category begin fconstructor, { exact (to_fun_hom F)⁻¹ᶠ (F f)⁻¹}, - { apply eq_of_fn_eq_fn' (to_fun_hom F), + { apply inj' (to_fun_hom F), rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,left_inverse]}, - { apply eq_of_fn_eq_fn' (to_fun_hom F), + { apply inj' (to_fun_hom F), rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,right_inverse]}, end diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean index fb96487f4..664920361 100644 --- a/hott/algebra/category/functor/equivalence.hlean +++ b/hott/algebra/category/functor/equivalence.hlean @@ -161,7 +161,7 @@ namespace category { exact inverse_of_fully_faithful_of_split_essentially_surjective}, { fapply natural_iso.mk', { intro c, esimp, apply reflect_iso F, exact (H₂ (F c)).2}, - intro c c' f, esimp, apply eq_of_fn_eq_fn' (to_fun_hom F), + intro c c' f, esimp, apply inj' (to_fun_hom F), rewrite [+respect_comp, +right_inv (to_fun_hom F), comp_inverse_cancel_left]}, { fapply natural_iso.mk', { intro c, esimp, exact (H₂ c).2}, diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index 8f162fa1d..5e862f9c0 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -182,7 +182,7 @@ namespace group definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ := homomorphism.mk φ⁻¹ abstract begin - intro g₁ g₂, apply eq_of_fn_eq_fn' φ, + intro g₁ g₂, apply inj' φ, rewrite [respect_mul φ, +right_inv φ] end end diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 80cebd131..0eb2cee0a 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -10,8 +10,6 @@ import .trunc_group types.trunc .group_theory types.nat.hott open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv nat --- TODO: consistently make n an argument before A --- TODO: rename homotopy_group_functor_compose to homotopy_group_functor_pcompose namespace eq definition inf_pgroup_loop [constructor] [instance] (A : Type*) : inf_pgroup (Ω A) := @@ -103,7 +101,7 @@ namespace eq π[k] (ptrunc k A) ≃* π[k] A := homotopy_group_ptrunc_of_le (le.refl k) A - theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 := + theorem trivial_homotopy_of_is_set (n : ℕ) (A : Type*) [H : is_set A] : πg[n+1] A ≃g G0 := begin apply trivial_group_of_is_contr, apply is_trunc_trunc_of_is_trunc, @@ -111,30 +109,30 @@ namespace eq apply is_trunc_succ_succ_of_is_set end - definition homotopy_group_succ_out (A : Type*) (n : ℕ) : π[n + 1] A = π₁ (Ω[n] A) := idp + definition homotopy_group_succ_out (n : ℕ) (A : Type*) : π[n + 1] A = π₁ (Ω[n] A) := idp - definition homotopy_group_succ_in (A : Type*) (n : ℕ) : π[n + 1] A ≃* π[n] (Ω A) := - ptrunc_pequiv_ptrunc 0 (loopn_succ_in A n) + definition homotopy_group_succ_in (n : ℕ) (A : Type*) : π[n + 1] A ≃* π[n] (Ω A) := + ptrunc_pequiv_ptrunc 0 (loopn_succ_in n A) - definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n + 1] A = π₁ (Ω[n] A) := idp + definition ghomotopy_group_succ_out (n : ℕ) (A : Type*) : πg[n + 1] A = π₁ (Ω[n] A) := idp - definition homotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[n + 2] A) : - homotopy_group_succ_in A (succ n) (g * h) = - homotopy_group_succ_in A (succ n) g * homotopy_group_succ_in A (succ n) h := + definition homotopy_group_succ_in_con {n : ℕ} {A : Type*} (g h : πg[n + 2] A) : + homotopy_group_succ_in (succ n) A (g * h) = + homotopy_group_succ_in (succ n) A g * homotopy_group_succ_in (succ n) A h := begin induction g with p, induction h with q, esimp, apply ap tr, apply loopn_succ_in_con end - definition ghomotopy_group_succ_in [constructor] (A : Type*) (n : ℕ) : + definition ghomotopy_group_succ_in [constructor] (n : ℕ) (A : Type*) : πg[n + 2] A ≃g πg[n + 1] (Ω A) := begin fapply isomorphism_of_equiv, - { exact homotopy_group_succ_in A (succ n)}, - { exact homotopy_group_succ_in_con}, + { exact homotopy_group_succ_in (succ n) A }, + { exact homotopy_group_succ_in_con }, end - definition is_contr_homotopy_group_of_is_contr (A : Type*) (n : ℕ) [is_contr A] : is_contr (π[n] A) := + definition is_contr_homotopy_group_of_is_contr (n : ℕ) (A : Type*) [is_contr A] : is_contr (π[n] A) := begin apply is_trunc_trunc_of_is_trunc, apply is_contr_loop_of_is_trunc, @@ -154,35 +152,35 @@ namespace eq definition homotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) := ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid - definition homotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C) + definition homotopy_group_functor_pcompose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C) (f : A →* B) : π→[n] (g ∘* f) ~* π→[n] g ∘* π→[n] f := ptrunc_functor_phomotopy 0 !apn_pcompose ⬝* !ptrunc_functor_pcompose definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) - [is_equiv f] : is_equiv (π→[n] f) := - @(is_equiv_trunc_functor 0 _) !is_equiv_apn + (H : is_equiv f) : is_equiv (π→[n] f) := + @(is_equiv_trunc_functor 0 _) (is_equiv_apn n f H) definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) : - homotopy_group_succ_in B n ∘* π→[n + 1] f ~* - π→[n] (Ω→ f) ∘* homotopy_group_succ_in A n := + homotopy_group_succ_in n B ∘* π→[n + 1] f ~* + π→[n] (Ω→ f) ∘* homotopy_group_succ_in n A := begin refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose, exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f) end definition homotopy_group_succ_in_natural_unpointed (n : ℕ) {A B : Type*} (f : A →* B) : - hsquare (homotopy_group_succ_in A n) (homotopy_group_succ_in B n) (π→[n+1] f) (π→[n] (Ω→ f)) := + hsquare (homotopy_group_succ_in n A) (homotopy_group_succ_in n B) (π→[n+1] f) (π→[n] (Ω→ f)) := (homotopy_group_succ_in_natural n f)⁻¹* definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) := - have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n), - from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in B n) + have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in n A), + from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in n B) (homotopy_group_succ_in_natural n f), - is_equiv.cancel_right (homotopy_group_succ_in A n) _ + is_equiv.cancel_right (homotopy_group_succ_in n A) _ definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X := - ptrunc_functor 0 pinverse + ptrunc_functor 0 (pinverse X) definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) := by apply @is_equiv_trunc_functor; apply is_equiv_eq_inverse @@ -218,14 +216,14 @@ namespace eq definition homotopy_group_homomorphism_pcompose (n : ℕ) [H : is_succ n] {A B C : Type*} (g : B →* C) (f : A →* B) : π→g[n] (g ∘* f) ~ π→g[n] g ∘ π→g[n] f := begin - induction H with n, exact to_homotopy (homotopy_group_functor_compose (succ n) g f) + induction H with n, exact to_homotopy (homotopy_group_functor_pcompose (succ n) g f) end definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B) : πg[n+1] A ≃g πg[n+1] B := begin apply isomorphism.mk (homotopy_group_homomorphism (succ n) f), - esimp, apply is_equiv_trunc_functor, apply is_equiv_apn, + exact is_equiv_homotopy_group_functor _ _ _, end definition homotopy_group_add (A : Type*) (n m : ℕ) : @@ -238,11 +236,11 @@ namespace eq exact !loopn_succ_in⁻¹ᵉ*} end - theorem trivial_homotopy_add_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ) + theorem trivial_homotopy_add_of_is_set_loopn {n : ℕ} (m : ℕ) {A : Type*} (H : is_set (Ω[n] A)) : πg[m+n+1] A ≃g G0 := !homotopy_group_add ⬝g !trivial_homotopy_of_is_set - theorem trivial_homotopy_le_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m) + theorem trivial_homotopy_le_of_is_set_loopn {n : ℕ} (m : ℕ) (H1 : n ≤ m) {A : Type*} (H2 : is_set (Ω[n] A)) : πg[m+1] A ≃g G0 := obtain (k : ℕ) (p : n + k = m), from le.elim H1, isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g @@ -300,8 +298,8 @@ namespace eq definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) := - !homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝* - !homotopy_group_functor_compose + !homotopy_group_functor_pcompose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝* + !homotopy_group_functor_pcompose definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n] (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) := @@ -313,7 +311,7 @@ namespace eq /- some homomorphisms -/ - -- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) : + -- definition is_homomorphism_cast_loopn_succ_eq_in (n : ℕ) {A : Type*} : -- is_homomorphism (loopn_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) := -- begin -- intro g h, induction g with g, induction h with h, @@ -321,7 +319,7 @@ namespace eq -- loopn_succ_eq_in_concat, - + tr_compose], -- end - definition is_mul_hom_inverse (A : Type*) (n : ℕ) + definition is_mul_hom_inverse (n : ℕ) (A : Type*) : is_mul_hom (λp, p⁻¹ : (πag[n+2] A) → (πag[n+2] A)) := begin intro g h, exact ap inv (mul.comm g h) ⬝ mul_inv h g, diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index e800b87a3..d8a028250 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -668,7 +668,7 @@ namespace eq induction r₁₀, induction r₀₁, induction r₁₂, induction r₂₁, induction p₁₂, induction p₁₀, induction p₂₁, esimp at *, induction s₁₁, esimp at *, esimp [square_of_eq], - apply eq_of_fn_eq_fn !square_equiv_eq, esimp, + apply inj !square_equiv_eq, esimp, exact (eq_bot_of_square u)⁻¹ end diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index 8168330a8..d2196084c 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -242,7 +242,7 @@ namespace eq induction p₁₀, -- if needed we can remove this induction and use con_tr_idp in types/eq2 rewrite [▸* at H,idp_con at H,+ap_id at H], let H' := eq_of_vdeg_square H, - exact eq_of_fn_eq_fn !pathover_equiv_tr_eq H' + exact inj !pathover_equiv_tr_eq H' end -- definition vdeg_tr_squareover {q₁₂ : p₀₁ ▸ b₀₀ =[p₁₂] p₂₁ ▸ b₂₀} (r : q₁₀ =[_] q₁₂) diff --git a/hott/eq2.hlean b/hott/eq2.hlean index 9ff14ca58..f75ae9b58 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -248,7 +248,7 @@ namespace eq (H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p := begin assert qr : Σ(q : a₀ = a₁), ap f q = p, - { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, + { exact ⟨inj f p, ap_inj' f p⟩ }, cases qr with q r, apply transport P r, induction q, exact H end @@ -256,7 +256,7 @@ namespace eq (H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p := begin assert qr : Σ(q : a₀ = a₁), ap f q = p, - { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, + { exact ⟨inj f p, ap_inj' f p⟩ }, cases qr with q r, apply transport P r, induction q, exact H end @@ -273,11 +273,11 @@ namespace eq ⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p := begin assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p, - { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p), - whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ }, + { exact ⟨inj g (right_inv g (f a₀) ⬝ p), + whisker_left _ (ap_inj' g _) ⬝ !inv_con_cancel_left⟩ }, assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p', - { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'), - whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ }, + { exact ⟨inj g (right_inv g (f a₀) ⬝ p'), + whisker_left _ (ap_inj' g _) ⬝ !inv_con_cancel_left⟩ }, induction qr with q r, induction q'r' with q' r', induction q, induction q', induction r, induction r', diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 8fcb7f9f4..4fee13f54 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -58,7 +58,7 @@ parameters {A B : Type.{u}} (f g : A → B) theorem elim_cp {P : Type} (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x)) (x : A) : ap (elim P_i Pcp) (cp x) = Pcp x := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (cp x)), + apply inj_inv !(pathover_constant (cp x)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cp], end diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 333c17068..bedebd957 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -67,7 +67,7 @@ section (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) {j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)), + apply inj_inv !(pathover_constant (cglue j x)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cglue], end @@ -157,7 +157,7 @@ section (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) {n : ℕ} (a : A n) : ap (elim Pincl Pglue) (glue a) = Pglue a := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (glue a)), + apply inj_inv !(pathover_constant (glue a)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_glue], end diff --git a/hott/hit/groupoid_quotient.hlean b/hott/hit/groupoid_quotient.hlean index dea68cfdc..86c188546 100644 --- a/hott/hit/groupoid_quotient.hlean +++ b/hott/hit/groupoid_quotient.hlean @@ -219,7 +219,7 @@ section definition encode_con (p : elt a = elt b) (q : elt b = elt c) : encode (elt c) (p ⬝ q) = encode (elt c) q ∘ encode (elt b) p := begin - apply eq_of_fn_eq_fn (elt_eq_elt_equiv a c)⁻¹ᵉ, + apply inj (elt_eq_elt_equiv a c)⁻¹ᵉ, refine !right_inv ⬝ _ ⬝ !decode_comp⁻¹, apply concat2, do 2 exact (to_left_inv !elt_eq_elt_equiv _)⁻¹ end diff --git a/hott/hit/prop_trunc.hlean b/hott/hit/prop_trunc.hlean index 9cae8937e..3d3ffd8e9 100644 --- a/hott/hit/prop_trunc.hlean +++ b/hott/hit/prop_trunc.hlean @@ -78,7 +78,7 @@ namespace one_step_tr (Pe : Π(a a' : A), Pt a = Pt a') (a a' : A) : ap (elim Pt Pe) (tr_eq a a') = Pe a a' := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (tr_eq a a')), + apply inj_inv !(pathover_constant (tr_eq a a')), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_tr_eq], end diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index ea8787614..a21df3f4d 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -66,7 +66,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (x : TL) : ap (elim Pinl Pinr Pglue) (glue x) = Pglue x := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (glue x)), + apply inj_inv !(pathover_constant (glue x)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue], end diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 1b9de387e..a124aeae9 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -34,7 +34,7 @@ namespace quotient (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a') : ap (quotient.elim Pc Pp) (eq_of_rel R H) = Pp H := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)), + apply inj_inv !(pathover_constant (eq_of_rel R H)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel], end @@ -148,7 +148,7 @@ namespace quotient induction v with q p, induction q, { exact Qpt p}, - { apply pi_pathover_left', esimp, intro c, + { apply pi_pathover_left, esimp, intro c, refine _ ⬝op apdt Qpt (elim_type_eq_of_rel C f H c)⁻¹ᵖ, refine _ ⬝op (tr_compose Q Ppt _ _)⁻¹ , rewrite ap_inv, diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean index b8a68e7c6..6fb70ccea 100644 --- a/hott/hit/set_quotient.hlean +++ b/hott/hit/set_quotient.hlean @@ -59,7 +59,7 @@ section (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a') : ap (elim Pc Pp) (eq_of_rel H) = Pp H := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)), + apply inj_inv !(pathover_constant (eq_of_rel H)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], end diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 8d02dc9fb..74a673f69 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -71,7 +71,7 @@ namespace trunc exact fn_tr_eq_tr_fn p (λy, tr) x ⬝ !tr_compose end - definition is_equiv_trunc_functor [constructor] (f : X → Y) [H : is_equiv f] + definition is_equiv_trunc_functor [constructor] (f : X → Y) (H : is_equiv f) : is_equiv (trunc_functor n f) := adjointify _ (trunc_functor n f⁻¹) @@ -83,7 +83,7 @@ namespace trunc section definition trunc_equiv_trunc [constructor] (f : X ≃ Y) : trunc n X ≃ trunc n Y := - equiv.mk _ (is_equiv_trunc_functor n f) + equiv.mk _ (is_equiv_trunc_functor n f _) end section diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 0aacd9e55..298025ba2 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -92,7 +92,7 @@ namespace simple_two_quotient (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') ⦃a a' : A⦄ (s : R a a') : ap (pre_elim Pj Pa Pe) (e s) = Pe s := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (e s)), + apply inj_inv !(pathover_constant (e s)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pre_elim,rec_e], end diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index a94413757..6466f3f4a 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -257,7 +257,7 @@ namespace EM { rewrite [EMadd1_succ G (succ n)], refine (ptrunc_pequiv (succ n + 1) _)⁻¹ᵉ* ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*, have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1, - refine freudenthal_pequiv _ this } + refine freudenthal_pequiv this _ } end definition loopn_EMadd1_pequiv_EM1 (G : AbGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 39688d4b8..9efa2a01c 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -181,7 +181,7 @@ namespace chain_complex (fiber_sequence_carrier_pequiv n ∘* fiber_sequence_fun (n + 3)) ∘* (fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* ~* - Ω→ (fiber_sequence_fun n) ∘* pinverse := + Ω→ (fiber_sequence_fun n) ∘* !pinverse := begin fapply phomotopy.mk, { exact chain_complex.fiber_sequence_fun_eq_helper f n}, @@ -203,7 +203,7 @@ namespace chain_complex theorem fiber_sequence_fun_phomotopy (n : ℕ) : fiber_sequence_carrier_pequiv n ∘* fiber_sequence_fun (n + 3) ~* - (Ω→ (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) := + (Ω→ (fiber_sequence_fun n) ∘* !pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) := begin apply phomotopy_of_pinv_right_phomotopy, apply fiber_sequence_fun_phomotopy_helper @@ -271,7 +271,7 @@ namespace chain_complex by reflexivity definition pid_or_pinverse_add4_rev (n : ℕ) : - pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1)) := + pid_or_pinverse (n + 4) ~* !pinverse ∘* Ω→(pid_or_pinverse (n + 1)) := !ap1_pcompose_pinverse theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ), @@ -312,7 +312,7 @@ namespace chain_complex | 0 := !pid | 1 := !pid | 2 := !pid - | (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse + | (k+3) := Ω→(pid_or_pinverse_right k) ∘* !pinverse definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n | 0 := pequiv.rfl @@ -320,14 +320,14 @@ namespace chain_complex | 2 := pequiv.rfl | 3 := pequiv.rfl | 4 := pequiv.rfl - | (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* pinverse + | (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* !pinverse definition pid_or_pinverse_right_add3 (n : ℕ) - : pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* pinverse := + : pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* !pinverse := by reflexivity definition pid_or_pinverse_left_add5 (n : ℕ) - : pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* pinverse := + : pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* !pinverse := by reflexivity theorem pid_or_pinverse_commute_right : Π(n : ℕ), @@ -420,7 +420,7 @@ namespace chain_complex definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n | (n, fin.mk 0 H) := proof Ω→[n] f qed | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed - | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loopn_succ_in Y n qed + | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loopn_succ_in n Y qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2) @@ -580,7 +580,7 @@ namespace chain_complex | (n, fin.mk 0 H) := proof π→[n] f qed | (n, fin.mk 1 H) := proof π→[n] (ppoint f) qed | (n, fin.mk 2 H) := - proof π→[n] boundary_map ∘* homotopy_group_succ_in Y n qed + proof π→[n] boundary_map ∘* homotopy_group_succ_in n Y qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible] @@ -638,7 +638,7 @@ namespace chain_complex cc_to_fn LES_of_homotopy_groups (n, 1) = π→[n] (ppoint f) := by reflexivity definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) = - π→[n] boundary_map ∘* homotopy_group_succ_in Y n := + π→[n] boundary_map ∘* homotopy_group_succ_in n Y := by reflexivity open group @@ -673,7 +673,7 @@ namespace chain_complex begin apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)), exact abstract begin rewrite [LES_of_homotopy_groups_fun_2], - refine homomorphism.struct ((π→g[k+1] boundary_map) ∘g ghomotopy_group_succ_in Y k), + refine homomorphism.struct ((π→g[k+1] boundary_map) ∘g ghomotopy_group_succ_in k Y), end end end | (k, fin.mk (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end @@ -749,7 +749,7 @@ namespace chain_complex : Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n | (n, fin.mk 0 H) := proof Ω→[n] f qed | (n, fin.mk 1 H) := proof Ω→[n] g qed - | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loopn_succ_in Y n qed + | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loopn_succ_in n Y qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition fibration_sequence_pequiv : Π(x : +3ℕ), diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index eda87b4eb..ac2a94604 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -59,14 +59,14 @@ namespace circle theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant seg1), + apply inj_inv !(pathover_constant seg1), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim2,rec2_seg1], end theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant seg2), + apply inj_inv !(pathover_constant seg2), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim2,rec2_seg2], end @@ -122,14 +122,14 @@ namespace circle theorem elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : ap (circle.elim Pbase Ploop) loop = Ploop := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant loop), + apply inj_inv !(pathover_constant loop), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,rec_loop], end theorem elim_seg1 {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : ap (circle.elim Pbase Ploop) seg1 = (tr_constant seg1 Pbase)⁻¹ := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant seg1), + apply inj_inv !(pathover_constant seg1), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec], rewrite [↑circle.rec2_on,rec2_seg1], apply inverse, apply pathover_of_eq_tr_constant_inv @@ -138,7 +138,7 @@ namespace circle theorem elim_seg2 {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : ap (circle.elim Pbase Ploop) seg2 = Ploop ⬝ (tr_constant seg1 Pbase)⁻¹ := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant seg2), + apply inj_inv !(pathover_constant seg2), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec], rewrite [↑circle.rec2_on,rec2_seg2], assert l : Π(A B : Type)(a a₂ a₂' : A)(b b' : B)(p : a = a₂)(p' : a₂' = a₂) @@ -295,7 +295,7 @@ namespace circle trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p := - eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm]) + inj base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm]) definition fundamental_group_of_circle : π₁(S¹*) ≃g gℤ := begin @@ -308,7 +308,7 @@ namespace circle open nat definition homotopy_group_of_circle (n : ℕ) : πg[n+2] S¹* ≃g G0 := begin - refine @trivial_homotopy_add_of_is_set_loopn S¹* 1 n _, + refine @trivial_homotopy_add_of_is_set_loopn 1 n S¹* _, exact is_trunc_equiv_closed_rev _ base_eq_base_equiv _ end diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index 1c0456a88..6fd597ca7 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -97,11 +97,11 @@ namespace is_conn rewrite [-(ap (λv a, v (f a)) (apd10_eq_of_homotopy_fn r))], rewrite [-(apd10_ap_precompose_dependent f (eq_of_homotopy r))], apply equiv.symm, - apply eq_equiv_fn_eq (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a))) + apply eq_equiv_fn_eq_of_is_equiv (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a))) end, apply equiv.trans (sigma.sigma_equiv_sigma_right e'), clear e', apply equiv.trans (equiv.symm (sigma.sigma_equiv_sigma_left - eq_equiv_homotopy)), + !eq_equiv_homotopy)), apply equiv.symm, apply equiv.trans !fiber_eq_equiv, apply sigma.sigma_equiv_sigma_right, intro r, apply eq_equiv_eq_symm @@ -321,7 +321,7 @@ namespace is_conn [H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) := begin apply is_conn_fun_of_is_equiv, - apply is_equiv_trunc_functor_of_le f H + exact is_equiv_trunc_functor_of_le f H _ end -- Exercise 7.18 @@ -427,7 +427,7 @@ namespace is_conn begin apply is_conn_fun_of_is_equiv, have H3 : is_equiv (trunc_functor k f), from !is_equiv_trunc_functor_of_is_conn_fun, - have H4 : is_equiv (trunc_functor n f), from is_equiv_trunc_functor_of_le _ H, + have H4 : is_equiv (trunc_functor n f), from is_equiv_trunc_functor_of_le _ H _, apply is_equiv_of_equiv_of_homotopy (equiv.mk (trunc_functor n f) _ ⬝e !trunc_equiv), intro x, induction x, reflexivity end diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean index ac8778209..322018b53 100644 --- a/hott/homotopy/cylinder.hlean +++ b/hott/homotopy/cylinder.hlean @@ -67,7 +67,7 @@ section (Pseg : Π(a : A), Pbase (f a) = Ptop a) (a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (seg a)), + apply inj_inv !(pathover_constant (seg a)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_seg], end diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index 5505fd669..5c2124ff8 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -167,29 +167,29 @@ namespace freudenthal section end end freudenthal open algebra group -definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) +definition freudenthal_pequiv {n k : ℕ} (H : k ≤ 2 * n) (A : Type*) [is_conn n A] : ptrunc k A ≃* ptrunc k (Ω (susp A)) := have H' : k ≤[ℕ₋₂] n + n, by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H, ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n) -definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) +definition freudenthal_equiv {n k : ℕ} (H : k ≤ 2 * n) (A : Type*) [is_conn n A] : trunc k A ≃ trunc k (Ω (susp A)) := -freudenthal_pequiv A H +freudenthal_pequiv H A -definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) +definition freudenthal_homotopy_group_pequiv {n k : ℕ} (H : k ≤ 2 * n) (A : Type*) [is_conn n A] : π[k + 1] (susp A) ≃* π[k] A := calc - π[k + 1] (susp A) ≃* π[k] (Ω (susp A)) : homotopy_group_succ_in (susp A) k + π[k + 1] (susp A) ≃* π[k] (Ω (susp A)) : homotopy_group_succ_in k (susp A) ... ≃* Ω[k] (ptrunc k (Ω (susp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (susp A)) - ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) + ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv H A) ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* -definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A] - (H : k + 1 ≤ 2 * n) : πg[k+2] (susp A) ≃g πg[k + 1] A := +definition freudenthal_homotopy_group_isomorphism {n k : ℕ} (H : k + 1 ≤ 2 * n) + (A : Type*) [is_conn n A] : πg[k+2] (susp A) ≃g πg[k + 1] A := begin fapply isomorphism_of_equiv, - { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A H)}, + { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv H A)}, { intro g h, refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con, apply ap !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, @@ -198,17 +198,17 @@ begin apply homotopy_group_succ_in_con} end - definition to_pmap_freudenthal_pequiv {A : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) - : freudenthal_pequiv A H ~* ptrunc_functor k (loop_susp_unit A) := + definition to_pmap_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) (A : Type*) [is_conn n A] + : freudenthal_pequiv H A ~* ptrunc_functor k (loop_susp_unit A) := begin fapply phomotopy.mk, { intro x, induction x with a, reflexivity }, { refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose } end - definition ptrunc_elim_freudenthal_pequiv {A B : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) + definition ptrunc_elim_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) {A B : Type*} [is_conn n A] (f : A →* Ω B) [is_trunc (k.+1) (B)] : - ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv A H ~* ptrunc.elim k f := + ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv H A ~* ptrunc.elim k f := begin refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, refine !ptrunc_elim_ptrunc_functor ⬝* _, @@ -220,12 +220,12 @@ namespace susp definition iterate_susp_stability_pequiv_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A] (H : k ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, - freudenthal_homotopy_group_pequiv (iterate_susp n A) H + freudenthal_homotopy_group_pequiv H (iterate_susp n A) - definition iterate_susp_stability_isomorphism_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A] - (H : k + 1 ≤ 2 * n) : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := + definition iterate_susp_stability_isomorphism_of_is_conn_0 {k n : ℕ} (H : k + 1 ≤ 2 * n) + (A : Type*) [is_conn 0 A] : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, - freudenthal_homotopy_group_isomorphism (iterate_susp n A) H + freudenthal_homotopy_group_isomorphism H (iterate_susp n A) definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : k ≤ 2 * pred n := begin @@ -233,7 +233,7 @@ namespace susp apply pred_le_pred, apply pred_le_pred, exact H end - definition stability_helper2 (A : Type*) {k n : ℕ} (H : k + 2 ≤ 2 * n) : + definition stability_helper2 {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) : is_conn (pred n) (iterate_susp n A) := have Π(n : ℕ), n = -1 + (n + 1), begin intro n, induction n with n IH, reflexivity, exact ap succ IH end, @@ -243,17 +243,17 @@ namespace susp { esimp, rewrite [this n], exact is_conn_iterate_susp -1 _ A } end - definition iterate_susp_stability_pequiv (A : Type*) {k n : ℕ} - (H : k + 2 ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := - have is_conn (pred n) (iterate_susp n A), from stability_helper2 A H, - freudenthal_homotopy_group_pequiv (iterate_susp n A) (stability_helper1 H) + definition iterate_susp_stability_pequiv {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) : + π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := + have is_conn (pred n) (iterate_susp n A), from stability_helper2 H A, + freudenthal_homotopy_group_pequiv (stability_helper1 H) (iterate_susp n A) - definition iterate_susp_stability_isomorphism (A : Type*) {k n : ℕ} - (H : k + 3 ≤ 2 * n) : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := - have is_conn (pred n) (iterate_susp n A), from @stability_helper2 A (k+1) n H, - freudenthal_homotopy_group_isomorphism (iterate_susp n A) (stability_helper1 H) + definition iterate_susp_stability_isomorphism {k n : ℕ} (H : k + 3 ≤ 2 * n) (A : Type*) : + πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := + have is_conn (pred n) (iterate_susp n A), from @stability_helper2 (k+1) n H A, + freudenthal_homotopy_group_isomorphism (stability_helper1 H) (iterate_susp n A) - definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n) + definition iterated_freudenthal_pequiv {n k m : ℕ} (H : k ≤ 2 * n) (A : Type*) [HA : is_conn n A] : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_susp m A)) := begin revert A n k HA H, induction m with m IH: intro A n k HA H, @@ -263,7 +263,7 @@ namespace susp succ k ≤ succ (2 * n) : succ_le_succ H ... ≤ 2 * succ n : self_le_succ, exact calc - ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv A H + ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv H A ... ≃* Ω (ptrunc (succ k) (susp A)) : loop_ptrunc_pequiv ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_susp m (susp A)))) : loop_pequiv_loop (IH (susp A) (succ n) (succ k) _ H2) diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 87cb5491b..51dad31c6 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -79,8 +79,8 @@ namespace is_trunc begin have π→[k] pdown.{v u} ∘* π→[k] (plift_functor f) ∘* π→[k] pup.{u v} ~* π→[k] f, begin - refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _, - refine !homotopy_group_functor_compose⁻¹* ⬝* _, + refine pwhisker_left _ !homotopy_group_functor_pcompose⁻¹* ⬝* _, + refine !homotopy_group_functor_pcompose⁻¹* ⬝* _, apply homotopy_group_functor_phomotopy, apply plift_functor_phomotopy end, have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this, @@ -133,10 +133,10 @@ namespace is_trunc pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))), begin apply is_equiv_compose, exact this a p, - apply is_equiv_trunc_functor + exact is_equiv_trunc_functor _ _ _ end, apply is_equiv.homotopy_closed, exact this, - refine !homotopy_group_functor_compose⁻¹* ⬝* _, + refine !homotopy_group_functor_pcompose⁻¹* ⬝* _, apply homotopy_group_functor_phomotopy, fapply phomotopy.mk, { esimp, intro q, refine !idp_con⁻¹}, @@ -157,12 +157,12 @@ namespace is_trunc apply is_equiv_compose (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)), apply is_equiv_compose (π→[k + 1] f), - all_goals apply is_equiv_homotopy_group_functor, + all_goals exact is_equiv_homotopy_group_functor _ _ _, end, refine @(is_equiv.homotopy_closed _) _ this _, apply to_homotopy, - refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _, - refine !homotopy_group_functor_compose⁻¹* ⬝* _, + refine pwhisker_left _ !homotopy_group_functor_pcompose⁻¹* ⬝* _, + refine !homotopy_group_functor_pcompose⁻¹* ⬝* _, apply homotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map end diff --git a/hott/homotopy/interval.hlean b/hott/homotopy/interval.hlean index d8df97ae0..78a6ea0fa 100644 --- a/hott/homotopy/interval.hlean +++ b/hott/homotopy/interval.hlean @@ -44,7 +44,7 @@ namespace interval theorem elim_seg {P : Type} (P0 P1 : P) (Ps : P0 = P1) : ap (interval.elim P0 P1 Ps) seg = Ps := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant seg), + apply inj_inv !(pathover_constant seg), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑interval.elim,rec_seg], end diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index 3d5386748..bdc7b3cbc 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -45,7 +45,7 @@ namespace join (Pglue : Π(x : A)(y : B), Pinl x = Pinr y) (x : A) (y : B) : ap (join.elim Pinl Pinr Pglue) (glue x y) = Pglue x y := begin - apply equiv.eq_of_fn_eq_fn_inv !(pathover_constant (glue x y)), + apply equiv.inj_inv !(pathover_constant (glue x y)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑join.elim], apply join.rec_glue end diff --git a/hott/homotopy/smash.hlean b/hott/homotopy/smash.hlean index c9b3206ca..aa6ca9857 100644 --- a/hott/homotopy/smash.hlean +++ b/hott/homotopy/smash.hlean @@ -109,7 +109,7 @@ namespace smash (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) : ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluel A B a)), + apply inj_inv !(pathover_constant (@gluel A B a)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluel], end @@ -117,7 +117,7 @@ namespace smash (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) : ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluer A B b)), + apply inj_inv !(pathover_constant (@gluer A B b)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluer], end diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 129880d34..4c4f4ad2f 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -38,7 +38,7 @@ namespace sphere begin induction n with n s, { exact tt }, - { exact (loopn_succ_in (S (succ n)) n)⁻¹ᵉ* (apn n (equator n) s) } + { exact (loopn_succ_in n (S (succ n)))⁻¹ᵉ* (apn n (equator n) s) } end definition sphere_equiv_bool [constructor] : S 0 ≃ bool := by reflexivity diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean index 6f6401972..3386d6bea 100644 --- a/hott/homotopy/sphere2.hlean +++ b/hott/homotopy/sphere2.hlean @@ -56,11 +56,11 @@ namespace sphere definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : π[k + 1] (S (n+1)) ≃* π[k] (S n) := - iterate_susp_stability_pequiv pbool H + iterate_susp_stability_pequiv H pbool definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S (n+1)) ≃g πg[k+1] (S n) := - iterate_susp_stability_isomorphism pbool H + iterate_susp_stability_isomorphism H pbool open int circle hopf definition πnSn (n : ℕ) [H : is_succ n] : πg[n] (S (n)) ≃g gℤ := diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 2e551bf13..24df3f986 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -69,7 +69,7 @@ namespace susp theorem elim_merid {P : Type} {PN PS : P} (Pm : A → PN = PS) (a : A) : ap (susp.elim PN PS Pm) (merid a) = Pm a := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)), + apply inj_inv !(pathover_constant (merid a)), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑susp.elim,rec_merid], end @@ -512,7 +512,7 @@ namespace susp begin revert X Y, induction n with n IH: intro X Y, { reflexivity }, - { refine !susp_adjoint_loop ⬝e* !IH ⬝e* _, apply pequiv_ppcompose_left, + { refine !susp_adjoint_loop ⬝e* !IH ⬝e* _, apply ppmap_pequiv_ppmap_right, symmetry, apply loopn_succ_in } end diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index b28bb959b..d8b24ee74 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -174,10 +174,10 @@ namespace is_equiv have Hfinv : is_equiv f⁻¹, from is_equiv_inv f, @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (f ∘ g)) (λa, left_inv f (g a)) - definition eq_of_fn_eq_fn' [unfold 4] {x y : A} (q : f x = f y) : x = y := + definition inj' [unfold 4] {x y : A} (q : f x = f y) : x = y := (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y - definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := + definition ap_inj' {x y : A} (q : f x = f y) : ap f (inj' f q) = q := !ap_con ⬝ whisker_right _ !ap_con ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) ◾ (inverse (ap_compose f f⁻¹ _)) @@ -186,15 +186,15 @@ namespace is_equiv ⬝ whisker_right _ !con.left_inv ⬝ !idp_con - definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q := + definition inj'_ap {x y : A} (q : x = y) : inj' f (ap f q) = q := by induction q; apply con.left_inv definition is_equiv_ap [instance] [constructor] (x y : A) : is_equiv (ap f : x = y → f x = f y) := adjointify (ap f) - (eq_of_fn_eq_fn' f) - (ap_eq_of_fn_eq_fn' f) - (eq_of_fn_eq_fn'_ap f) + (inj' f) + (ap_inj' f) + (inj'_ap f) end @@ -269,16 +269,16 @@ namespace is_equiv include H definition inv_commute' (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A} (c : C (g' a)) : f⁻¹ (h' c) = h (f⁻¹ c) := - eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) + inj' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) definition fun_commute_of_inv_commute' (p : Π⦃a : A⦄ (c : C (g' a)), f⁻¹ (h' c) = h (f⁻¹ c)) {a : A} (b : B (g' a)) : f (h b) = h' (f b) := - eq_of_fn_eq_fn' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹) + inj' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹) definition ap_inv_commute' (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A} (c : C (g' a)) : ap f (inv_commute' @f @h @h' p c) = right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹ := - !ap_eq_of_fn_eq_fn' + !ap_inj' -- inv_commute'_fn is in types.equiv end @@ -286,7 +286,7 @@ namespace is_equiv -- This is inv_commute' for A ≡ unit definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C) (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) := - eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) + inj' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) end is_equiv open is_equiv @@ -350,12 +350,11 @@ namespace equiv : A ≃ B := equiv.mk f (inv_homotopy_closed Heq) - --rename: eq_equiv_fn_eq_fn_of_is_equiv - definition eq_equiv_fn_eq [constructor] (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) := + definition eq_equiv_fn_eq_of_is_equiv [constructor] (f : A → B) [H : is_equiv f] (a b : A) : + (a = b) ≃ (f a = f b) := equiv.mk (ap f) !is_equiv_ap - --rename: eq_equiv_fn_eq_fn - definition eq_equiv_fn_eq_of_equiv [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) := + definition eq_equiv_fn_eq [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) := equiv.mk (ap f) !is_equiv_ap definition equiv_ap [constructor] (P : A → Type) {a b : A} (p : a = b) : P a ≃ P b := @@ -368,17 +367,17 @@ namespace equiv : equiv_of_eq (refl A) = equiv.refl A := idp - definition eq_of_fn_eq_fn [unfold 3] (f : A ≃ B) {x y : A} (q : f x = f y) : x = y := + definition inj [unfold 3] (f : A ≃ B) {x y : A} (q : f x = f y) : x = y := (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y - definition eq_of_fn_eq_fn_inv [unfold 3] (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y := + definition inj_inv [unfold 3] (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y := (right_inv f x)⁻¹ ⬝ ap f q ⬝ right_inv f y - definition ap_eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := - ap_eq_of_fn_eq_fn' f q + definition ap_inj (f : A ≃ B) {x y : A} (q : f x = f y) : ap f (inj' f q) = q := + ap_inj' f q - definition eq_of_fn_eq_fn_ap (f : A ≃ B) {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q := - eq_of_fn_eq_fn'_ap f q + definition inj_ap (f : A ≃ B) {x y : A} (q : x = y) : inj' f (ap f q) = q := + inj'_ap f q definition to_inv_homotopy_inv {f g : A ≃ B} (p : f ~ g) : f⁻¹ᵉ ~ g⁻¹ᵉ := inv_homotopy_inv p diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 472876277..dc69450dd 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -239,7 +239,7 @@ end funext open funext namespace eq - definition eq_equiv_homotopy : (f = g) ≃ (f ~ g) := + definition eq_equiv_homotopy (f g : Πx, P x) : (f = g) ≃ (f ~ g) := equiv.mk apd10 _ definition eq_of_homotopy [reducible] : f ~ g → f = g := diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 3410d41b1..37de448b3 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -355,8 +355,6 @@ namespace is_trunc theorem is_set.elimo (q q' : c =[p] c₂) [H : is_set (C a)] : q = q' := !is_prop.elim - -- TODO: port "Truncated morphisms" - /- truncated universe -/ end is_trunc diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index d2dce74cd..f7deacc50 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -71,7 +71,7 @@ namespace equiv rec_on_ua' f (λq, eq.rec_on q H) definition ua_refl (A : Type) : ua erfl = idpath A := - eq_of_fn_eq_fn !eq_equiv_equiv (right_inv !eq_equiv_equiv erfl) + inj !eq_equiv_equiv (right_inv !eq_equiv_equiv erfl) definition ua_symm {A B : Type} (f : A ≃ B) : ua f⁻¹ᵉ = (ua f)⁻¹ := begin diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 32b5035a2..5f2ca913c 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -106,7 +106,7 @@ namespace is_equiv inv_commute' @f @h @h' p (f b) = (ap f⁻¹ (p b))⁻¹ ⬝ left_inv f (h b) ⬝ (ap h (left_inv f b))⁻¹ := begin - rewrite [↑[inv_commute',eq_of_fn_eq_fn'],+ap_con,-adj_inv f,+con.assoc,inv_con_cancel_left, + rewrite [↑[inv_commute',inj'],+ap_con,-adj_inv f,+con.assoc,inv_con_cancel_left, adj f,+ap_inv,-+ap_compose, eq_bot_of_square (natural_square_tr (λb, (left_inv f (h b))⁻¹ ⬝ ap f⁻¹ (p b)) (left_inv f b))⁻¹ʰ, con_inv,inv_inv,+con.assoc], @@ -254,8 +254,8 @@ namespace equiv definition equiv_eq_char (f f' : A ≃ B) : (f = f') ≃ (to_fun f = to_fun f') := calc - (f = f') ≃ (to_fun !equiv.sigma_char f = to_fun !equiv.sigma_char f') - : eq_equiv_fn_eq (to_fun !equiv.sigma_char) + (f = f') ≃ (!equiv.sigma_char f = !equiv.sigma_char f') + : eq_equiv_fn_eq !equiv.sigma_char ... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype ... ≃ (to_fun f = to_fun f') : equiv.rfl @@ -315,15 +315,15 @@ namespace equiv [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) := by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv - definition eq_of_fn_eq_fn'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A) - : eq_of_fn_eq_fn' f (idpath (f x)) = idpath x := + definition inj'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A) + : inj' f (idpath (f x)) = idpath x := !con.left_inv - definition eq_of_fn_eq_fn'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A} + definition inj'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A} (p : f x = f y) (q : f y = f z) - : eq_of_fn_eq_fn' f (p ⬝ q) = eq_of_fn_eq_fn' f p ⬝ eq_of_fn_eq_fn' f q := + : inj' f (p ⬝ q) = inj' f p ⬝ inj' f q := begin - unfold eq_of_fn_eq_fn', + unfold inj', refine _ ⬝ !con.assoc, apply whisker_right, refine _ ⬝ !con.assoc⁻¹ ⬝ !con.assoc⁻¹, apply whisker_left, refine !ap_con ⬝ _, apply whisker_left, diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 32735d08f..fa863fa73 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -31,7 +31,7 @@ namespace fiber : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) := begin apply equiv.trans, - apply eq_equiv_fn_eq_of_equiv, apply fiber.sigma_char, + apply eq_equiv_fn_eq, apply fiber.sigma_char, apply equiv.trans, apply sigma_eq_equiv, apply sigma_equiv_sigma_right, @@ -180,7 +180,7 @@ namespace fiber begin fapply pequiv_of_equiv, esimp, refine fiber.equiv_precompose f g (Point B), - esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp, + esimp, apply (inj (fiber.sigma_char _ _)), fapply sigma_eq: esimp, { apply respect_pt g }, { apply eq_pathover_Fl' } end @@ -210,7 +210,7 @@ namespace fiber x = y ≃ fiber (ap1_gen f (point_eq x) (point_eq y)) (idpath b) := calc x = y ≃ fiber.sigma_char f b x = fiber.sigma_char f b y : - eq_equiv_fn_eq_of_equiv (fiber.sigma_char f b) x y + eq_equiv_fn_eq (fiber.sigma_char f b) x y ... ≃ Σ(p : point x = point y), point_eq x =[p] point_eq y : sigma_eq_equiv ... ≃ Σ(p : point x = point y), (point_eq x)⁻¹ ⬝ ap f p ⬝ point_eq y = idp : sigma_equiv_sigma_right (λp, diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean index a6b603d81..cec437dbc 100644 --- a/hott/types/lift.hlean +++ b/hott/types/lift.hlean @@ -142,10 +142,10 @@ namespace lift fiber (lift_functor f) (up b) ≃ fiber f b := begin fapply equiv.MK: intro v; cases v with a p, - { cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p) }, + { cases a with a, exact fiber.mk a (inj' up p) }, { exact fiber.mk (up a) (ap up p) }, - { apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap }, - { cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn' } + { apply ap (fiber.mk a), apply inj'_ap }, + { cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_inj' } end definition lift_functor2 {A B C : Type} (f : A → B → C) (x : lift A) (y : lift B) : lift C := diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index cae70f3d6..96692f1dd 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -58,7 +58,7 @@ namespace pi /- Pathovers -/ - definition pi_pathover {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'} + definition pi_pathover' {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'} (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[apd011 C p q] g b') : f =[p] g := begin cases p, apply pathover_idp_of_eq, @@ -66,7 +66,7 @@ namespace pi apply eq_of_pathover_idp, apply r end - definition pi_pathover_left {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'} + definition pi_pathover_left' {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'} (r : Π(b : B a), f b =[apd011 C p !pathover_tr] g (p ▸ b)) : f =[p] g := begin cases p, apply pathover_idp_of_eq, @@ -74,7 +74,7 @@ namespace pi apply eq_of_pathover_idp, apply r end - definition pi_pathover_right {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'} + definition pi_pathover_right' {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'} (r : Π(b' : B a'), f (p⁻¹ ▸ b') =[apd011 C p !tr_pathover] g b') : f =[p] g := begin cases p, apply pathover_idp_of_eq, @@ -93,7 +93,7 @@ namespace pi -- a version where C is uncurried, but where the conclusion of r is still a proper pathover -- instead of a heterogenous equality - definition pi_pathover' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩} + definition pi_pathover {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩} {p : a = a'} (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[dpair_eq_dpair p q] g b') : f =[p] g := begin @@ -102,7 +102,7 @@ namespace pi apply (@eq_of_pathover_idp _ C), exact (r b b (pathover.idpatho b)), end - definition pi_pathover_left' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩} + definition pi_pathover_left {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩} {p : a = a'} (r : Π(b : B a), f b =[dpair_eq_dpair p !pathover_tr] g (p ▸ b)) : f =[p] g := begin @@ -111,7 +111,7 @@ namespace pi apply eq_of_pathover_idp, esimp at r, exact !pathover_ap (r b) end - definition pi_pathover_right' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩} + definition pi_pathover_right {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩} {p : a = a'} (r : Π(b' : B a'), f (p⁻¹ ▸ b') =[dpair_eq_dpair p !tr_pathover] g b') : f =[p] g := begin diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 14902f57f..f0b1bab35 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -162,7 +162,7 @@ namespace pointed { induction x, reflexivity } end - definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt := + definition pmap.sigma_char [constructor] (A B : Type*) : (A →* B) ≃ Σ(f : A → B), f pt = pt := !ppi.sigma_char definition pmap.eta_expand [constructor] {A B : Type*} (f : A →* B) : A →* B := @@ -204,7 +204,7 @@ namespace pointed definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B := pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) - definition pinverse [constructor] {X : Type*} : Ω X →* Ω X := + definition pinverse [constructor] (X : Type*) : Ω X →* Ω X := pmap.mk eq.inverse idp /- @@ -301,24 +301,16 @@ namespace pointed intro p, exact !idp_con⁻¹ end - definition is_equiv_apn (n : ℕ) (f : A →* B) [H : is_equiv f] - : is_equiv (apn n f) := - begin - induction n with n IH, - { exact H}, - { exact is_equiv_ap1 (apn n f)} - end - definition pinverse_con [constructor] {X : Type*} (p q : Ω X) - : pinverse (p ⬝ q) = pinverse q ⬝ pinverse p := + : pinverse X (p ⬝ q) = pinverse X q ⬝ pinverse X p := !con_inv definition pinverse_inv [constructor] {X : Type*} (p : Ω X) - : pinverse p⁻¹ = (pinverse p)⁻¹ := + : pinverse X p⁻¹ = (pinverse X p)⁻¹ := idp definition ap1_pcompose_pinverse [constructor] {X Y : Type*} (f : X →* Y) : - Ω→ f ∘* pinverse ~* pinverse ∘* Ω→ f := + Ω→ f ∘* pinverse X ~* pinverse Y ∘* Ω→ f := phomotopy.mk (ap1_gen_inv f (respect_pt f) (respect_pt f)) abstract begin induction Y with Y y₀, induction f with f f₀, esimp at * ⊢, induction f₀, reflexivity @@ -437,7 +429,7 @@ namespace pointed : sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _))) ... ≃ Σ(p : k ~ l), respect_pt k = p pt ⬝ respect_pt l - : sigma_equiv_sigma_left' eq_equiv_homotopy + : sigma_equiv_sigma_left' !eq_equiv_homotopy ... ≃ Σ(p : k ~ l), p pt ⬝ respect_pt l = respect_pt k : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) ... ≃ (k ~* l) : phomotopy.sigma_char k l @@ -640,7 +632,7 @@ namespace pointed { reflexivity} end - definition ap1_pinverse [constructor] {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) := + definition ap1_pinverse [constructor] {A : Type*} : ap1 (pinverse A) ~* pinverse (Ω A) := begin fapply phomotopy.mk, { intro p, refine !idp_con ⬝ _, exact !inv_eq_inv2⁻¹ }, @@ -715,7 +707,7 @@ namespace pointed definition pcast_idp [constructor] {A : Type*} : pcast (idpath A) ~* pid A := by reflexivity - definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) := + definition pinverse_pinverse (A : Type*) : pinverse A ∘* pinverse A ~* pid (Ω A) := begin fapply phomotopy.mk, { apply inv_inv}, @@ -1051,7 +1043,6 @@ namespace pointed /- pointed equivalences between particular pointed types -/ - -- TODO: remove is_equiv_apn, which is proven again here definition loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B := pequiv.MK (apn n f) (apn n f⁻¹ᵉ*) abstract begin @@ -1073,9 +1064,15 @@ namespace pointed apply ap1_pid} end end + definition is_equiv_apn [constructor] (n : ℕ) (f : A →* B) (H : is_equiv f) : is_equiv (apn n f) := + to_is_equiv (loopn_pequiv_loopn n (pequiv_of_pmap f H)) + definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B := loopn_pequiv_loopn 1 f + notation `Ω≃`:(max+5) := loop_pequiv_loop + notation `Ω≃[`:95 n:0 `]`:0 := loopn_pequiv_loopn n + definition loop_pequiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a') : pointed.MK (a = a) idp ≃* pointed.MK (a' = a') idp := pequiv_of_equiv (loop_equiv_eq_closed p) (con.left_inv p) @@ -1121,7 +1118,7 @@ namespace pointed end end definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A := - pequiv_of_pmap pinverse !is_equiv_eq_inverse + pequiv_of_pmap (pinverse A) !is_equiv_eq_inverse definition pequiv_of_eq_pt [constructor] {A : Type} {a a' : A} (p : a = a') : pointed.MK A a ≃* pointed.MK A a' := @@ -1142,36 +1139,33 @@ namespace pointed end /- properties of iterated loop space -/ - variable (A) - definition loopn_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) := + definition loopn_succ_in (n : ℕ) (A : Type*) : Ω[succ n] A ≃* Ω[n] (Ω A) := begin induction n with n IH, { reflexivity}, { exact loop_pequiv_loop IH} end - definition loopn_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) := + definition loopn_add (n m : ℕ) (A : Type*) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) := begin induction n with n IH, { reflexivity}, { exact loop_pequiv_loop IH} end - definition loopn_succ_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A) := + definition loopn_succ_out (n : ℕ) (A : Type*) : Ω[succ n] A ≃* Ω(Ω[n] A) := by reflexivity - variable {A} - definition loopn_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) : - loopn_succ_in A (succ n) (p ⬝ q) = - loopn_succ_in A (succ n) p ⬝ loopn_succ_in A (succ n) q := + loopn_succ_in (succ n) A (p ⬝ q) = + loopn_succ_in (succ n) A p ⬝ loopn_succ_in (succ n) A q := !loop_pequiv_loop_con definition loopn_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A := begin intros, fapply pType_eq, { esimp, transitivity _, - apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹), + apply eq_equiv_fn_eq (equiv_eq_closed_right _ p⁻¹), esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv}, { esimp, apply con.left_inv} end @@ -1185,7 +1179,7 @@ namespace pointed ... = Ω[n+2] A : by rewrite [algebra.add.comm] definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) : - loopn_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n := + loopn_succ_in n B ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in n A := begin induction n with n IH, { reflexivity}, @@ -1193,11 +1187,11 @@ namespace pointed end definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) : - loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n := + loopn_succ_in n B ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in n A := !apn_succ_phomotopy_in definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) : - Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= + Ω→[n + 1] f ∘* (loopn_succ_in n A)⁻¹ᵉ* ~* (loopn_succ_in n B)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= begin apply pinv_right_phomotopy_of_phomotopy, refine _ ⬝* !passoc⁻¹*, diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index 7a8e03c4d..d65f45caf 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -48,10 +48,6 @@ namespace pointed -- intro p, -- end - /- Short term TODO: generalize to dependent maps (use ppi_eq_equiv?) - Long term TODO: use homotopies between pointed homotopies, not equalities - -/ - definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) : (h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k), whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h := @@ -72,7 +68,7 @@ namespace pointed : by exact sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ (!whisker_right_ap⁻¹ᵖ))) ... ≃ Σ(p : to_homotopy h ~ to_homotopy k), whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h - : sigma_equiv_sigma_left' eq_equiv_homotopy + : sigma_equiv_sigma_left' !eq_equiv_homotopy definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) (q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k := @@ -448,7 +444,7 @@ namespace pointed : f ~* g := begin apply phomotopy.mk (λa, eq_of_phomotopy (p a)), - apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv], + apply inj (pmap_eq_equiv _ _), esimp [pmap_eq_equiv], refine !phomotopy_of_eq_con ⬝ _, refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, end @@ -460,8 +456,8 @@ namespace pointed definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C := pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f)) - /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof), rename to ppmap_pequiv_ppmap_right -/ - definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := + /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof) -/ + definition ppmap_pequiv_ppmap_right [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := pequiv.MK' (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*) begin intro f, apply eq_of_phomotopy, apply pinv_pcompose_cancel_left end begin intro f, apply eq_of_phomotopy, apply pcompose_pinv_cancel_left end @@ -477,7 +473,7 @@ namespace pointed -- exact sorry -- end end - definition pequiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := + definition ppmap_pequiv_ppmap_left [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := begin fapply pequiv.MK', { exact ppcompose_right f }, @@ -830,7 +826,7 @@ namespace pointed fapply is_trunc_equiv_closed, { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, fapply is_contr_fiber_of_is_equiv, - exact pequiv.to_is_equiv (pequiv_ppcompose_left f) + exact pequiv.to_is_equiv (ppmap_pequiv_ppmap_right f) end definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) := @@ -838,7 +834,7 @@ namespace pointed fapply is_trunc_equiv_closed, { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, fapply is_contr_fiber_of_is_equiv, - exact pequiv.to_is_equiv (pequiv_ppcompose_right f) + exact pequiv.to_is_equiv (ppmap_pequiv_ppmap_left f) end definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g := diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 2aba40ae8..82d48f166 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -198,15 +198,14 @@ namespace sigma : bc =[p] ⟨p ▸ bc.1, p ▸D bc.2⟩ := by induction p; induction bc; apply idpo - -- TODO: interchange sigma_pathover and sigma_pathover' - definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) + definition sigma_pathover' (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) (r : u.1 =[p] v.1) (s : u.2 =[apd011 C p r] v.2) : u =[p] v := begin induction u, induction v, esimp at *, induction r, esimp [apd011] at s, induction s using idp_rec_on, apply idpo end - definition sigma_pathover' (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) + definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) (r : u.1 =[p] v.1) (s : pathover (λx, C x.1 x.2) u.2 (sigma_eq p r) v.2) : u =[p] v := begin induction u, induction v, esimp at *, induction r, diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 9a51c1e9b..a07ba82c9 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -325,7 +325,7 @@ namespace is_trunc (A = B) ≃ (carrier A = carrier B) := calc (A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B) - : eq_equiv_fn_eq_of_equiv + : eq_equiv_fn_eq ... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1) : equiv.symm (!equiv_subtype) ... ≃ (carrier A = carrier B) : equiv.refl @@ -352,7 +352,7 @@ namespace is_trunc definition tua_refl {n : ℕ₋₂} (A : n-Type) : tua (@erfl A) = idp := begin refine ap (trunctype_eq_equiv n A A)⁻¹ᶠ (ua_refl A) ⬝ _, - refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_idp , + refine ap (inj _) _ ⬝ !inj'_idp , apply ap (dpair_eq_dpair idp), apply is_prop.elim end @@ -360,7 +360,7 @@ namespace is_trunc : tua (f ⬝e g) = tua f ⬝ tua g := begin refine ap (trunctype_eq_equiv n A C)⁻¹ᶠ (ua_trans f g) ⬝ _, - refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_con, + refine ap (inj _) _ ⬝ !inj'_con, refine _ ⬝ !dpair_eq_dpair_con, apply ap (dpair_eq_dpair _), esimp, apply is_prop.elim end @@ -723,7 +723,7 @@ namespace trunc end definition is_equiv_trunc_functor_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k) - [is_equiv (trunc_functor k f)] : is_equiv (trunc_functor n f) := + (H' : is_equiv (trunc_functor k f)) : is_equiv (trunc_functor n f) := is_equiv_of_equiv_of_homotopy (trunc_equiv_trunc_of_le H (equiv.mk (trunc_functor k f) _)) (trunc_functor_homotopy_of_le f H) @@ -1116,7 +1116,7 @@ namespace function apply is_equiv_of_imp_is_equiv, intro p, note q := ap (@tr 0 _) p, - note r := @(eq_of_fn_eq_fn' (trunc_functor 0 f)) _ (tr a) (tr a') q, + note r := @(inj' (trunc_functor 0 f)) _ (tr a) (tr a') q, induction (tr_eq_tr_equiv _ _ _ r) with s, induction s, apply is_equiv.homotopy_closed (ap1 (pmap_of_map f a)), diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean index 1ab63bc8e..a0b602556 100644 --- a/hott/types/unit.hlean +++ b/hott/types/unit.hlean @@ -42,7 +42,7 @@ namespace unit definition unit_arrow_eq_compose {X Y : Type} (g : X → Y) (f : unit → X) : unit_arrow_eq (g ∘ f) = ap (λf, g ∘ f) (unit_arrow_eq f) := begin - apply eq_of_fn_eq_fn' apd10, + apply inj' apd10, refine right_inv apd10 _ ⬝ _, refine _ ⬝ ap apd10 (!compose_eq_of_homotopy)⁻¹, refine _ ⬝ (right_inv apd10 _)⁻¹, diff --git a/tests/lean/extra/755.hlean b/tests/lean/extra/755.hlean index 959cb9b98..95b3d75f7 100644 --- a/tests/lean/extra/755.hlean +++ b/tests/lean/extra/755.hlean @@ -38,7 +38,7 @@ section (Pe : Π(a a' : A), Pt a = Pt a') (a a' : A) : ap (elim Pt Pe) (tr_eq a a') = Pe a a' := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (tr_eq a a')), + apply inj_inv !(pathover_constant (tr_eq a a')), rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_tr_eq], end