From ed7de51d0232fcd73b70a197e6905743e16d2554 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 2 Jun 2017 12:15:31 -0400 Subject: [PATCH] move basic lemmas from the spectral repository to the main repository --- TODO.txt | 6 + algebra/direct_sum.hlean | 4 +- algebra/exact_couple.hlean | 22 +- algebra/exactness.hlean | 124 +++ algebra/is_short_exact.hlean | 57 -- algebra/left_module.hlean | 4 +- algebra/module_chain_complex.hlean | 4 +- algebra/module_exact_couple.hlean | 13 +- algebra/quotient_group.hlean | 4 +- algebra/ses.hlean | 12 +- algebra/short_five.hlean | 4 +- homotopy/cohomology.hlean | 2 +- homotopy/pushout.hlean | 3 +- homotopy/smash.hlean | 2 +- homotopy/smash_adjoint.hlean | 4 +- homotopy/spectrum.hlean | 8 +- homotopy/susp.hlean | 2 +- move_to_lib.hlean | 1327 +--------------------------- pointed.hlean | 943 +------------------- 19 files changed, 190 insertions(+), 2355 deletions(-) create mode 100644 algebra/exactness.hlean delete mode 100644 algebra/is_short_exact.hlean diff --git a/TODO.txt b/TODO.txt index 3a36435..79ce9f0 100644 --- a/TODO.txt +++ b/TODO.txt @@ -2,3 +2,9 @@ - define pmap in terms of ppi - move move_to_lib and pointed to library + +talk with Favonia about: +- dependent pointed maps +- higher cube filling strategies +- HIT equivalences +- algebra diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 5363b8a..e5eaf82 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -71,8 +71,8 @@ namespace group (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 := begin induction r with r, induction r, - rewrite [to_respect_add, to_respect_neg], apply add_neg_eq_of_eq_add, - rewrite [zero_add, to_respect_add, ▸*, ↑foldl, +one_mul, to_respect_add'] + rewrite [to_respect_add, to_respect_neg, to_respect_add, ▸*, ↑foldl, +one_mul, + to_respect_add'], apply mul.right_inv end definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' := diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 3dcd5d8..8a4c47c 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -38,9 +38,9 @@ definition homology_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : (homology d H) ≃g (homology_ugly d H) := begin - fapply @iso_of_ab_qg_group (ab_kernel d), + fapply @iso_of_ab_qg_group (ab_kernel d), intro a, - intro p, induction p with f, induction f with b p, + intro p, induction p with f, induction f with b p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact d b, fapply tr, fapply fiber.mk, exact b, reflexivity, induction a with c q, fapply subtype_eq, refine p ⬝ _, reflexivity, intro b p, induction p with f, induction f with c p, induction p, @@ -50,7 +50,7 @@ definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d definition SES_iso_C {A B C C' : AbGroup} (ses : SES A B C) (k : C ≃g C') : SES A B C' := - begin + begin fapply SES.mk, exact SES.f ses, exact k ∘g SES.g ses, @@ -139,14 +139,14 @@ definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) := fapply ab_group_first_iso_thm i, end -definition kj_zero (a : A) : k (j a) = 1 := +definition kj_zero (a : A) : k (j a) = 1 := is_exact.im_in_ker (exact_couple.exact_jk EC) a - -definition j_factor : A →g (ab_kernel d) := + +definition j_factor : A →g (ab_kernel d) := begin fapply ab_hom_lift j, - intro a, - unfold kernel_subgroup, + intro a, + unfold kernel_subgroup, exact calc d (j a) = j (k (j a)) : rfl ... = j 1 : by exact ap j (kj_zero a) @@ -164,7 +164,7 @@ definition subgroup_iso_exact_at_A : ab_kernel i ≃g ab_image k := induction EC, induction exact_ki, exact im_in_ker b, - end + end definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k ∘g subgroup_iso_exact_at_A := begin @@ -183,10 +183,10 @@ definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f ( refine sorry --(ap (j_factor) subgroup_iso_exact_at_A_triangle) ⬝ _, end -definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := +/-definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := begin exact sorry, -- refine (comm_gq_map (comm_kernel (boundary CC)) (image_subgroup_of_bd (boundary CC) (boundary_is_boundary CC))) ∘g _, - end + end-/ end derived_couple diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean new file mode 100644 index 0000000..3b0fd26 --- /dev/null +++ b/algebra/exactness.hlean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2017 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Avigad + +Short exact sequences +-/ +import homotopy.chain_complex eq2 +open pointed is_trunc equiv is_equiv eq algebra group trunc function + +structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + ( im_in_ker : Π(a:A), g (f a) = pt) + ( ker_in_im : Π(b:B), (g b = pt) → fiber f b) + +structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + ( im_in_ker : Π(a:A), g (f a) = pt) + ( ker_in_im : Π(b:B), (g b = pt) → image f b) + +namespace algebra + +definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) := +is_exact f g + +definition is_exact_ag {A B C : AbGroup} (f : A →g B) (g : B →g C) := +is_exact f g + +definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C} + (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g := +is_exact.mk H₁ H₂ + +definition is_exact.im_in_ker2 {A B : Type} {C : Set*} {f : A → B} {g : B → C} (H : is_exact f g) + {b : B} (h : image f b) : g b = pt := +begin + induction h with a p, exact ap g p⁻¹ ⬝ is_exact.im_in_ker H a +end + +-- TO DO: give less univalency proof +definition is_exact_homotopy {A B : Type} {C : Type*} {f f' : A → B} {g g' : B → C} + (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' := +begin + induction p using homotopy.rec_on_idp, + induction q using homotopy.rec_on_idp, + exact H +end + +definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} + (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := +begin + constructor, + { intro a, esimp, induction a with a, + exact ap tr (is_exact_t.im_in_ker H a) }, + { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q, + induction is_exact_t.ker_in_im H b q with a r, + exact image.mk (tr a) (ap tr r) } +end + +definition is_contr_middle_of_is_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C} (H : is_exact f g) + [is_contr A] [is_set B] [is_contr C] : is_contr B := +begin + apply is_contr.mk (f pt), + intro b, + induction is_exact.ker_in_im H b !is_prop.elim, + exact ap f !is_prop.elim ⬝ p +end + +definition is_surjective_of_is_exact_of_is_contr {A B : Type} {C : Type*} {f : A → B} {g : B → C} + (H : is_exact f g) [is_contr C] : is_surjective f := +λb, is_exact.ker_in_im H b !is_prop.elim + +section chain_complex +open succ_str chain_complex +definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N} + (H : is_exact_at A n) : is_exact (cc_to_fn A (S n)) (cc_to_fn A n) := +is_exact.mk (cc_is_chain_complex A n) H +end chain_complex + +structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + (is_emb : is_embedding f) + (im_in_ker : Π(a:A), g (f a) = pt) + (ker_in_im : Π(b:B), (g b = pt) → image f b) + (is_surj : is_surjective g) + +structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + (is_emb : is_embedding f) + (im_in_ker : Π(a:A), g (f a) = pt) + (ker_in_im : Π(b:B), (g b = pt) → fiber f b) + (is_surj : is_split_surjective g) + +lemma is_short_exact_of_is_exact {X A B C Y : Group} + (k : X →g A) (f : A →g B) (g : B →g C) (l : C →g Y) + (hX : is_contr X) (hY : is_contr Y) + (kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g := +begin + constructor, + { apply to_is_embedding_homomorphism, intro a p, + induction is_exact.ker_in_im kf a p with x q, + exact q⁻¹ ⬝ ap k !is_prop.elim ⬝ to_respect_one k }, + { exact is_exact.im_in_ker fg }, + { exact is_exact.ker_in_im fg }, + { intro c, exact is_exact.ker_in_im gl c !is_prop.elim }, +end + +lemma is_short_exact_equiv {A B A' B' : Type} {C C' : Type*} + {f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C) + (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C') + (h₁ : hsquare f f' eA eB) (h₂ : hsquare g g' eB eC) + (H : is_short_exact f' g') : is_short_exact f g := +begin + constructor, + { apply is_embedding_homotopy_closed_rev (homotopy_top_of_hsquare h₁), + apply is_embedding_compose, apply is_embedding_of_is_equiv, + apply is_embedding_compose, apply is_short_exact.is_emb H, apply is_embedding_of_is_equiv }, + { intro a, refine homotopy_top_of_hsquare' (hhconcat h₁ h₂) a ⬝ _, + refine ap eC⁻¹ _ ⬝ respect_pt eC⁻¹ᵉ*, exact is_short_exact.im_in_ker H (eA a) }, + { intro b p, note q := eq_of_inv_eq ((homotopy_top_of_hsquare' h₂ b)⁻¹ ⬝ p) ⬝ respect_pt eC, + induction is_short_exact.ker_in_im H (eB b) q with a' r, + apply image.mk (eA⁻¹ a'), + exact eq_of_fn_eq_fn eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) }, + { apply is_surjective_homotopy_closed_rev (homotopy_top_of_hsquare' h₂), + apply is_surjective_compose, apply is_surjective_of_is_equiv, + apply is_surjective_compose, apply is_short_exact.is_surj H, apply is_surjective_of_is_equiv } +end + +end algebra diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean deleted file mode 100644 index d9f7950..0000000 --- a/algebra/is_short_exact.hlean +++ /dev/null @@ -1,57 +0,0 @@ -/- -Copyright (c) 2017 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad - -Short exact sequences --/ -import .quotient_group -open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group - is_trunc function sphere unit sum prod - -structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := - (is_emb : is_embedding f) - (im_in_ker : Π(a:A), g (f a) = pt) - (ker_in_im : Π(b:B), (g b = pt) → image f b) - (is_surj : is_surjective g) - -structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := - (is_emb : is_embedding f) - (im_in_ker : Π(a:A), g (f a) = pt) - (ker_in_im : Π(b:B), (g b = pt) → fiber f b) - (is_surj : is_split_surjective g) - -lemma is_short_exact_of_is_exact {X A B C Y : Group} - (k : X →g A) (f : A →g B) (g : B →g C) (l : C →g Y) - (hX : is_contr X) (hY : is_contr Y) - (kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g := -begin - constructor, - { apply to_is_embedding_homomorphism, intro a p, - induction is_exact.ker_in_im kf a p with x q, - exact q⁻¹ ⬝ ap k !is_prop.elim ⬝ to_respect_one k }, - { exact is_exact.im_in_ker fg }, - { exact is_exact.ker_in_im fg }, - { intro c, exact is_exact.ker_in_im gl c !is_prop.elim }, -end - -lemma is_short_exact_equiv {A B A' B' : Type} {C C' : Type*} - {f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C) - (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C') - (h₁ : hsquare f f' eA eB) (h₂ : hsquare g g' eB eC) - (H : is_short_exact f' g') : is_short_exact f g := -begin - constructor, - { apply is_embedding_homotopy_closed_rev (homotopy_top_of_hsquare h₁), - apply is_embedding_compose, apply is_embedding_of_is_equiv, - apply is_embedding_compose, apply is_short_exact.is_emb H, apply is_embedding_of_is_equiv }, - { intro a, refine homotopy_top_of_hsquare' (hhconcat h₁ h₂) a ⬝ _, - refine ap eC⁻¹ _ ⬝ respect_pt eC⁻¹ᵉ*, exact is_short_exact.im_in_ker H (eA a) }, - { intro b p, note q := eq_of_inv_eq ((homotopy_top_of_hsquare' h₂ b)⁻¹ ⬝ p) ⬝ respect_pt eC, - induction is_short_exact.ker_in_im H (eB b) q with a' r, - apply image.mk (eA⁻¹ a'), - exact eq_of_fn_eq_fn eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) }, - { apply is_surjective_homotopy_closed_rev (homotopy_top_of_hsquare' h₂), - apply is_surjective_compose, apply is_surjective_of_is_equiv, - apply is_surjective_compose, apply is_short_exact.is_surj H, apply is_surjective_of_is_equiv } -end diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean index a8db111..0de50d3 100644 --- a/algebra/left_module.hlean +++ b/algebra/left_module.hlean @@ -7,7 +7,7 @@ Modules prod vector spaces over a ring. (We use "left_module," which is more precise, because "module" is a keyword.) -/ -import algebra.field ..move_to_lib .is_short_exact algebra.group_power +import algebra.field ..move_to_lib .exactness algebra.group_power open is_trunc pointed function sigma eq algebra prod is_equiv equiv group structure has_scalar [class] (F V : Type) := @@ -273,7 +273,7 @@ section definition homomorphism_eq (φ₁ φ₂ : M₁ →lm M₂) (p : φ₁ ~ φ₂) : φ₁ = φ₂ := begin induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p, - exact ap (homomorphism.mk φ₂) !is_prop.elim + exact ap (homomorphism.mk φ₁) !is_prop.elim end end diff --git a/algebra/module_chain_complex.hlean b/algebra/module_chain_complex.hlean index fa06d8e..6c5f03e 100644 --- a/algebra/module_chain_complex.hlean +++ b/algebra/module_chain_complex.hlean @@ -1,7 +1,7 @@ /- Author: Jeremy Avigad -/ -import homotopy.chain_complex .left_module .is_short_exact ..move_to_lib +import homotopy.chain_complex .left_module .exactness ..move_to_lib open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc open algebra function open chain_complex @@ -53,5 +53,5 @@ namespace left_module variables {A₀ B₀ C₀ : LeftModule R} variables (f₀ : A₀ →lm B₀) (g₀ : B₀ →lm C₀) - definition is_short_exact := @_root_.is_short_exact _ _ C₀ f₀ g₀ + definition is_short_exact := @algebra.is_short_exact _ _ C₀ f₀ g₀ end left_module diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean index bbf0c30..bde504c 100644 --- a/algebra/module_exact_couple.hlean +++ b/algebra/module_exact_couple.hlean @@ -136,6 +136,7 @@ namespace left_module definition deg_k' : deg k' ~ deg k := by reflexivity open group + set_option pp.coercions true lemma i'j' : is_exact_gmod i' j' := begin intro x, refine equiv_rect (deg i) _ _, @@ -165,7 +166,7 @@ namespace left_module { exact is_exact.ker_in_im (exact_couple.ij X _ _) _ s }, refine image.mk ⟨m - k x n, t⟩ _, apply subtype_eq, refine !i'_eq ⬝ !to_respect_sub ⬝ _, - refine ap (sub _) _ ⬝ !sub_zero, + refine ap (@sub (D (deg i (deg k x))) _ _) _ ⬝ @sub_zero _ _ _, apply is_exact.im_in_ker (exact_couple.ki X _ _) } end @@ -314,7 +315,7 @@ namespace left_module definition deg_j_inv (r : ℕ) : (deg (j (page r)))⁻¹ ~ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ := have H : deg (j (page r)) ~ iterate_equiv (deg (i X))⁻¹ᵉ r ⬝e deg (j X), from deg_j r, - λx, to_inv_homotopy_to_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x) + λx, to_inv_homotopy_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x) definition deg_d (r : ℕ) : deg (d (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r ∘ deg (k X) := @@ -322,7 +323,7 @@ namespace left_module definition deg_d_inv (r : ℕ) : (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ := - compose2 (to_inv_homotopy_to_inv (deg_k r)) (deg_j_inv r) + compose2 (to_inv_homotopy_inv (deg_k r)) (deg_j_inv r) definition B3 (x : I) : ℕ := max (B (deg (j X) (deg (k X) x))) (B2 ((deg (k X))⁻¹ ((deg (j X))⁻¹ x))) @@ -468,15 +469,15 @@ namespace pointed definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) : homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B := begin - cases n with n, { apply homomorphism_of_is_contr_right }, - cases n with n, { apply homomorphism_of_is_contr_right }, + cases n with n, { apply trivial_homomorphism }, + cases n with n, { apply trivial_homomorphism }, exact π→g[n+2] f end definition homotopy_group_conn_functor : Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B | (of_nat n) A B f := homotopy_group_conn_nat_functor n f - | (-[1+ n]) A B f := homomorphism_of_is_contr_right _ _ + | (-[1+ n]) A B f := trivial_homomorphism _ _ notation `π→c[`:95 n:0 `]`:0 := homotopy_group_conn_functor n diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index b4deee0..ad81334 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -551,7 +551,7 @@ definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} ( definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) : is_surjective (ab_group_kernel_quotient_to_image f) := begin - fapply @is_surjective_factor A _ (image f) _ _ _ (group_fun (ab_qg_map (kernel_subgroup f))), + fapply is_surjective_factor (group_fun (ab_qg_map (kernel_subgroup f))), exact image_lift f, apply quotient_group_compute, exact is_surjective_image_lift f @@ -560,7 +560,7 @@ exact is_surjective_image_lift f definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) : is_embedding (ab_group_kernel_quotient_to_image f) := begin - fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f), + fapply is_embedding_factor (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f), exact ab_group_kernel_quotient_to_image_codomain_triangle f, exact is_embedding_kernel_quotient_extension f end diff --git a/algebra/ses.hlean b/algebra/ses.hlean index 10fdc13..e03603d 100644 --- a/algebra/ses.hlean +++ b/algebra/ses.hlean @@ -8,7 +8,7 @@ Basic facts about short exact sequences. At the moment, it only covers short exact sequences of abelian groups, but this should be extended to short exact sequences in any abelian category. -/ -import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup +import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup .exactness open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc equiv is_equiv @@ -111,7 +111,7 @@ parameters {A B C : AbGroup} (ses : SES A B C) definition SES_iso_stable {A' B' C' : AbGroup} (f' : A' →g B') (g' : B' →g C') (α : A' ≃g A) (β : B' ≃g B) (γ : C' ≃g C) (Hαβ : f ∘g α ~ β ∘g f') (Hβγ : g ∘g β ~ γ ∘g g') : SES A' B' C' := begin - fapply SES.mk, + fapply SES.mk, exact f', exact g', fapply is_embedding_of_is_injective, @@ -120,10 +120,10 @@ definition SES_iso_stable {A' B' C' : AbGroup} (f' : A' →g B') (g' : B' →g C f (α x) = β (f' x) : Hαβ x ... = β (f' y) : ap β p ... = f (α y) : (Hαβ y)⁻¹, - have path' : α x = α y, by exact @is_injective_of_is_embedding _ _ f (SES.Hf ses) _ _ path, + have path' : α x = α y, by exact @is_injective_of_is_embedding _ _ f (SES.Hf ses) _ _ path, exact @is_injective_of_is_embedding _ _ α (is_embedding_of_is_equiv α) _ _ path', exact sorry, - exact sorry, + exact sorry, end definition SES_of_triangle_left {A' : AbGroup} (α : A' ≃g A) (f' : A' →g B) (H : Π a' : A', f (α a') = f' a') : SES A' B C := @@ -132,7 +132,7 @@ begin exact f', exact g, fapply is_embedding_of_is_injective, - intro x y p, + intro x y p, fapply eq_of_fn_eq_fn (equiv_of_isomorphism α), fapply @is_injective_of_is_embedding _ _ f (SES.Hf ses) (α x) (α y), rewrite [H x], rewrite [H y], exact p, @@ -143,7 +143,7 @@ begin fapply is_exact.im_in_ker (SES.ex ses), intro b p, have t : trunctype.carrier (subgroup_to_rel (image_subgroup f) b), from is_exact.ker_in_im (SES.ex ses) b p, - induction t, fapply tr, induction a with a q, fapply fiber.mk, exact α⁻¹ᵍ a, rewrite [(H (α⁻¹ᵍ a))⁻¹], + induction t, fapply tr, induction a with a q, fapply fiber.mk, exact α⁻¹ᵍ a, rewrite [(H (α⁻¹ᵍ a))⁻¹], krewrite [right_inv (equiv_of_isomorphism α) a], assumption end diff --git a/algebra/short_five.hlean b/algebra/short_five.hlean index 2a1d177..af701b9 100644 --- a/algebra/short_five.hlean +++ b/algebra/short_five.hlean @@ -20,7 +20,7 @@ section short_five include short_exact₀ short_exact₁ hsquare₁ hsquare₂ - open is_short_exact + open algebra.is_short_exact lemma short_five_mono [embh : is_embedding h] [embl : is_embedding l] : is_embedding k := @@ -56,7 +56,7 @@ section short_five assume ha₀ : h a₀ = a₁, have k (f₀ a₀) = k b₀ - b₁, by rewrite [hsquare₁, ▸*, ha₀, f₁a₁], have k (b₀ - f₀ a₀) = b₁, by rewrite [respect_sub, this, sub_sub_self], - image.intro this)))) + image.mk _ this)))) end short_five section short_exact diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 1baa8b8..e28f923 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -87,7 +87,7 @@ definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) : Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) := begin apply loopn_pequiv_loopn 2, - exact loop_pequiv_loop (pequiv_of_eq (ap Y (add_comm_right n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ* + exact loop_pequiv_loop (pequiv_of_eq (ap Y (add.right_comm n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ* end definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) : diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index bf4a9d7..0680f07 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -1,5 +1,5 @@ -import ..move_to_lib +import algebra.exactness homotopy.cofiber homotopy.wedge open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber @@ -25,7 +25,6 @@ namespace pushout end - /- WIP: proving that satisfying the universal property of the pushout is equivalent to being equivalent to the pushout diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 67a1ad9..4b6d875 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -1,6 +1,6 @@ -- Authors: Floris van Doorn -import homotopy.smash ..pointed .pushout homotopy.red_susp +import homotopy.smash types.pointed2 .pushout homotopy.red_susp open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function red_susp unit diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index f1330f2..8d23779 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -2,7 +2,7 @@ -- in collaboration with Egbert, Stefano, Robin, Ulrik /- the adjunction between the smash product and pointed maps -/ -import .smash .susp +import .smash .susp ..pointed open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function unit sigma susp sphere @@ -510,7 +510,7 @@ namespace smash calc ppmap (A ∧ psusp B) X ≃* ppmap (psusp B) (ppmap A X) : smash_adjoint_pmap A (psusp B) X ... ≃* ppmap B (Ω (ppmap A X)) : psusp_adjoint_loop' B (ppmap A X) - ... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_pmap_commute A X) + ... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute A X) ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X) ... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index e10fd82..c61695b 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..colim ..pointed .EM ..pointed_pi +import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group seq_colim succ_str EM EM.ops @@ -234,7 +234,7 @@ namespace spectrum definition sp_cotensor [constructor] {N : succ_str} (A : Type*) (B : gen_spectrum N) : gen_spectrum N := spectrum.MK (λn, ppmap A (B n)) - (λn, (loop_pmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n))) + (λn, (loop_ppmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n))) ---------------------------------------- -- Sections of parametrized spectra @@ -250,7 +250,7 @@ namespace spectrum definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N := spectrum.MK (λn, pfiber (f n)) - (λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_equiv_of_square _ _ (sglue_square f n)) + (λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_pequiv_of_square _ _ (sglue_square f n)) /- the map from the fiber to the domain -/ definition spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : sfiber f →ₛ X := @@ -259,7 +259,7 @@ namespace spectrum intro n, refine _ ⬝* !passoc, refine _ ⬝* pwhisker_right _ !ppoint_loop_pfiber_inv⁻¹*, - rexact (pfiber_equiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹* + rexact (pfiber_pequiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹* end definition scompose_spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index f8c7786..e192d0a 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -1,4 +1,4 @@ -import ..pointed +import homotopy.susp types.pointed2 open susp eq pointed function is_equiv diff --git a/move_to_lib.hlean b/move_to_lib.hlean index bb13e71..59cd841 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1,118 +1,10 @@ -- definitions, theorems and attributes which should be moved to files in the HoTT library -import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient +import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group is_trunc function sphere unit sum prod bool -attribute is_prop.elim_set [unfold 6] - -definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m := -!add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹ - --- move to chain_complex (or another file). rename chain_complex.is_exact -structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := - ( im_in_ker : Π(a:A), g (f a) = pt) - ( ker_in_im : Π(b:B), (g b = pt) → fiber f b) - -structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := - ( im_in_ker : Π(a:A), g (f a) = pt) - ( ker_in_im : Π(b:B), (g b = pt) → image f b) - -definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) := -is_exact f g - -definition is_exact_ag {A B C : AbGroup} (f : A →g B) (g : B →g C) := -is_exact f g - -definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C} - (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g := -is_exact.mk H₁ H₂ - -definition is_exact.im_in_ker2 {A B : Type} {C : Set*} {f : A → B} {g : B → C} (H : is_exact f g) - {b : B} (h : image f b) : g b = pt := -begin - induction h with a p, exact ap g p⁻¹ ⬝ is_exact.im_in_ker H a -end - --- TO DO: give less univalency proof -definition is_exact_homotopy {A B : Type} {C : Type*} {f f' : A → B} {g g' : B → C} - (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' := -begin - induction p using homotopy.rec_on_idp, - induction q using homotopy.rec_on_idp, - exact H -end - -definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} - (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := -begin - constructor, - { intro a, esimp, induction a with a, - exact ap tr (is_exact_t.im_in_ker H a) }, - { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q, - induction is_exact_t.ker_in_im H b q with a r, - exact image.mk (tr a) (ap tr r) } -end - -definition is_contr_middle_of_is_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C} (H : is_exact f g) - [is_contr A] [is_set B] [is_contr C] : is_contr B := -begin - apply is_contr.mk (f pt), - intro b, - induction is_exact.ker_in_im H b !is_prop.elim, - exact ap f !is_prop.elim ⬝ p -end - -definition is_surjective_of_is_exact_of_is_contr {A B : Type} {C : Type*} {f : A → B} {g : B → C} - (H : is_exact f g) [is_contr C] : is_surjective f := -λb, is_exact.ker_in_im H b !is_prop.elim - -section chain_complex -open succ_str chain_complex -definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N} - (H : is_exact_at A n) : is_exact (cc_to_fn A (S n)) (cc_to_fn A n) := -is_exact.mk (cc_is_chain_complex A n) H -end chain_complex - -namespace algebra - definition ab_group_unit [constructor] : ab_group unit := - ⦃ab_group, trivial_group, mul_comm := λx y, idp⦄ - - definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) := - by induction H; exact _ - - definition one_unique {A : Type} [group A] {a : A} (H : Πb, a * b = b) : a = 1 := - !mul_one⁻¹ ⬝ H 1 - - definition pSet_of_AddGroup [constructor] [reducible] [coercion] (G : AddGroup) : Set* := - pSet_of_Group G - attribute algebra._trans_of_pSet_of_AddGroup [unfold 1] - attribute algebra._trans_of_pSet_of_AddGroup_1 algebra._trans_of_pSet_of_AddGroup_2 [constructor] - - definition pType_of_AddGroup [reducible] [constructor] : AddGroup → Type* := - algebra._trans_of_pSet_of_AddGroup_1 - definition Set_of_AddGroup [reducible] [constructor] : AddGroup → Set := - algebra._trans_of_pSet_of_AddGroup_2 - - -- -- - -- definition Group_of_AddAbGroup [coercion] [constructor] (G : AddAbGroup) : Group := - -- AddGroup.mk G _ - -- -- - - definition AddGroup_of_AddAbGroup [coercion] [constructor] (G : AddAbGroup) : AddGroup := - AddGroup.mk G _ - - attribute algebra._trans_of_AddGroup_of_AddAbGroup_1 - algebra._trans_of_AddGroup_of_AddAbGroup - algebra._trans_of_AddGroup_of_AddAbGroup_3 [constructor] - attribute algebra._trans_of_AddGroup_of_AddAbGroup_2 [unfold 1] - - definition add_ab_group_AddAbGroup2 [instance] (G : AddAbGroup) : add_ab_group G := - AddAbGroup.struct G - -end algebra - namespace eq definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type} @@ -190,254 +82,6 @@ namespace eq induction q, exact eq.rec_grading (f ⬝e g) h p' H p end - definition eq.rec_symm {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₁ = a₀ → Type} - (H : P idp) ⦃a₁ : A⦄ (p : a₁ = a₀) : P p := - begin - cases p, exact H - end - - definition is_contr_homotopy_group_of_is_contr (A : Type*) (n : ℕ) [is_contr A] : is_contr (π[n] A) := - begin - apply is_trunc_trunc_of_is_trunc, - apply is_contr_loop_of_is_trunc, - apply is_trunc_of_is_contr - end - - definition cast_fn_cast_square {A : Type} {B C : A → Type} (f : Π⦃a⦄, B a → C a) {a₁ a₂ : A} - (p : a₁ = a₂) (q : a₂ = a₁) (r : p ⬝ q = idp) (b : B a₁) : - cast (ap C q) (f (cast (ap B p) b)) = f b := - have q⁻¹ = p, from inv_eq_of_idp_eq_con r⁻¹, - begin induction this, induction q, reflexivity end - -section -- squares - variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ 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₄₄-/ - - variables {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁} - {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃} - - definition natural_square_eq {A B : Type} {a a' : A} {f g : A → B} (p : f ~ g) (q : a = a') - : natural_square p q = square_of_pathover (apd p q) := - idp - - definition eq_of_square_hrfl_hconcat_eq {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') - : eq_of_square (hrfl ⬝hp q⁻¹) = !idp_con ⬝ q := - by induction q; induction p; reflexivity - - definition aps_vrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') : - aps f (vrefl p) = vrefl (ap f p) := - by induction p; reflexivity - - definition aps_hrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') : - aps f (hrefl p) = hrefl (ap f p) := - by induction p; reflexivity - - -- should the following two equalities be cubes? - definition natural_square_ap_fn {A B C : Type} {a a' : A} {g h : A → B} (f : B → C) (p : g ~ h) - (q : a = a') : natural_square (λa, ap f (p a)) q = - ap_compose f g q ⬝ph (aps f (natural_square p q) ⬝hp (ap_compose f h q)⁻¹) := - begin - induction q, exact !aps_vrfl⁻¹ - end - - definition natural_square_compose {A B C : Type} {a a' : A} {g g' : B → C} - (p : g ~ g') (f : A → B) (q : a = a') : natural_square (λa, p (f a)) q = - ap_compose g f q ⬝ph (natural_square p (ap f q) ⬝hp (ap_compose g' f q)⁻¹) := - by induction q; reflexivity - - definition natural_square_eq2 {A B : Type} {a a' : A} {f f' : A → B} (p : f ~ f') {q q' : a = a'} - (r : q = q') : natural_square p q = ap02 f r ⬝ph (natural_square p q' ⬝hp (ap02 f' r)⁻¹) := - by induction r; reflexivity - - definition natural_square_refl {A B : Type} {a a' : A} (f : A → B) (q : a = a') - : natural_square (homotopy.refl f) q = hrfl := - by induction q; reflexivity - - definition aps_eq_hconcat {p₀₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : - aps f (q ⬝ph s₁₁) = ap02 f q ⬝ph aps f s₁₁ := - by induction q; reflexivity - - definition aps_hconcat_eq {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁' = p₂₁) : - aps f (s₁₁ ⬝hp r⁻¹) = aps f s₁₁ ⬝hp (ap02 f r)⁻¹ := - by induction r; reflexivity - - definition aps_hconcat_eq' {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p₂₁') : - aps f (s₁₁ ⬝hp r) = aps f s₁₁ ⬝hp ap02 f r := - by induction r; reflexivity - - definition aps_square_of_eq (f : A → B) (s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : - aps f (square_of_eq s) = square_of_eq ((ap_con f p₁₀ p₂₁)⁻¹ ⬝ ap02 f s ⬝ ap_con f p₀₁ p₁₂) := - by induction p₁₂; esimp at *; induction s; induction p₂₁; induction p₁₀; reflexivity - - definition aps_eq_hconcat_eq {p₀₁' p₂₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) - (r : p₂₁' = p₂₁) : aps f (q ⬝ph s₁₁ ⬝hp r⁻¹) = ap02 f q ⬝ph aps f s₁₁ ⬝hp (ap02 f r)⁻¹ := - by induction q; induction r; reflexivity - -end - -section -- cubes - - 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₁₂₂} - {b₁ b₂ b₃ b₄ : B} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) - - definition whisker001 {p₀₀₁' : a₀₀₀ = a₀₀₂} (q : p₀₀₁' = p₀₀₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube (q ⬝ph s₀₁₁) s₂₁₁ (q ⬝ph s₁₀₁) s₁₂₁ s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition whisker021 {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁' = p₀₂₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : - cube (s₀₁₁ ⬝hp q⁻¹) s₂₁₁ s₁₀₁ (q ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition whisker021' {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁ = p₀₂₁') - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : - cube (s₀₁₁ ⬝hp q) s₂₁₁ s₁₀₁ (q⁻¹ ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition whisker201 {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁' = p₂₀₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : - cube s₀₁₁ (q ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q⁻¹) s₁₂₁ s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition whisker201' {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁ = p₂₀₁') - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : - cube s₀₁₁ (q⁻¹ ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition whisker221 {p₂₂₁' : a₂₂₀ = a₂₂₂} (q : p₂₂₁ = p₂₂₁') - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ (s₁₂₁ ⬝hp q) s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition move221 {p₂₂₁' : a₂₂₀ = a₂₂₂} {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁'} (q : p₂₂₁ = p₂₂₁') - (c : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : - cube s₀₁₁ s₂₁₁ s₁₀₁ (s₁₂₁ ⬝hp q⁻¹) s₁₁₀ s₁₁₂ := - by induction q; exact c - - definition move201 {p₂₀₁' : a₂₀₀ = a₂₀₂} {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁'} (q : p₂₀₁' = p₂₀₁) - (c : cube s₀₁₁ (q ⬝ph s₂₁₁) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : - cube s₀₁₁ s₂₁₁ (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ := - by induction q; exact c - -end - - definition ap_eq_ap010 {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) : - ap (λa, f a b) p = ap010 f p b := - by reflexivity - - definition ap011_idp {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) : - ap011 f p idp = ap010 f p b := - by reflexivity - - definition ap011_flip {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B} (p : a = a') (q : b = b') : - ap011 f p q = ap011 (λb a, f a b) q p := - by induction q; induction p; reflexivity - - theorem apd_constant' {A A' : Type} {B : A' → Type} {a₁ a₂ : A} {a' : A'} (b : B a') - (p : a₁ = a₂) : apd (λx, b) p = pathover_of_eq p idp := - by induction p; reflexivity - - definition apo011 {A : Type} {B C D : A → Type} {a a' : A} {p : a = a'} {b : B a} {b' : B a'} - {c : C a} {c' : C a'} (f : Π⦃a⦄, B a → C a → D a) (q : b =[p] b') (r : c =[p] c') : - f b c =[p] f b' c' := - begin induction q, induction r using idp_rec_on, exact idpo end - - definition ap011_ap_square_right {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') - {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) : - square (ap011 f p q₁₂) (ap (λx, f x b₃) p) (ap (f a) q₁₃) (ap (f a') q₂₃) := - by induction r; induction q₂₃; induction q₁₂; induction p; exact ids - - definition ap011_ap_square_left {A B C : Type} (f : B → A → C) {a a' : A} (p : a = a') - {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) : - square (ap011 f q₁₂ p) (ap (f b₃) p) (ap (λx, f x a) q₁₃) (ap (λx, f x a') q₂₃) := - by induction r; induction q₂₃; induction q₁₂; induction p; exact ids - - definition ap_ap011 {A B C D : Type} (g : C → D) (f : A → B → C) {a a' : A} {b b' : B} - (p : a = a') (q : b = b') : ap g (ap011 f p q) = ap011 (λa b, g (f a b)) p q := - begin - induction p, exact (ap_compose g (f a) q)⁻¹ - end - - definition con2_assoc {A : Type} {x y z t : A} {p p' : x = y} {q q' : y = z} {r r' : z = t} - (h : p = p') (h' : q = q') (h'' : r = r') : - square ((h ◾ h') ◾ h'') (h ◾ (h' ◾ h'')) (con.assoc p q r) (con.assoc p' q' r') := - by induction h; induction h'; induction h''; exact hrfl - - definition con_left_inv_idp {A : Type} {x : A} {p : x = x} (q : p = idp) - : con.left_inv p = q⁻² ◾ q := - by cases q; reflexivity - - definition eckmann_hilton_con2 {A : Type} {x : A} {p p' q q': idp = idp :> x = x} - (h : p = p') (h' : q = q') : square (h ◾ h') (h' ◾ h) (eckmann_hilton p q) (eckmann_hilton p' q') := - by induction h; induction h'; exact hrfl - - definition ap_con_fn {A B : Type} {a a' : A} {b : B} (g h : A → b = b) (p : a = a') : - ap (λa, g a ⬝ h a) p = ap g p ◾ ap h p := - by induction p; reflexivity - - protected definition homotopy.rfl [reducible] [unfold_full] {A B : Type} {f : A → B} : f ~ f := - homotopy.refl f - - definition compose_id {A B : Type} (f : A → B) : f ∘ id ~ f := - by reflexivity - - definition id_compose {A B : Type} (f : A → B) : id ∘ f ~ f := - by reflexivity - - -- move to eq2 - definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X} - (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) := - by induction p; reflexivity - - definition ap_is_weakly_constant {A B : Type} {f : A → B} - (h : is_weakly_constant f) {a a' : A} (p : a = a') : ap f p = (h a a)⁻¹ ⬝ h a a' := - by induction p; exact !con.left_inv⁻¹ - - definition ap_is_constant_idp {A B : Type} {f : A → B} {b : B} (p : Πa, f a = b) {a : A} (q : a = a) - (r : q = idp) : ap_is_constant p q = ap02 f r ⬝ (con.right_inv (p a))⁻¹ := - by cases r; exact !idp_con⁻¹ - - definition con_right_inv_natural {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') : - con.right_inv p = q ◾ q⁻² ⬝ con.right_inv p' := - by induction q; induction p; reflexivity - - definition whisker_right_ap {A B : Type} {a a' : A}{b₁ b₂ b₃ : B} (q : b₂ = b₃) (f : A → b₁ = b₂) - (p : a = a') : whisker_right q (ap f p) = ap (λa, f a ⬝ q) p := - by induction p; reflexivity - - infix ` ⬝hty `:75 := homotopy.trans - postfix `⁻¹ʰᵗʸ`:(max+1) := homotopy.symm - - definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) := - λa, idp - - -- to algebra.homotopy_group - 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) - end - - definition apn_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : - Ω→[n] f⁻¹ᵉ* ~* (loopn_pequiv_loopn n f)⁻¹ᵉ* := - begin - refine !to_pinv_pequiv_MK2⁻¹* - end - -- definition homotopy_group_homomorphism_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : -- π→g[n+1] f⁻¹ᵉ* ~ (homotopy_group_isomorphism_of_pequiv n f)⁻¹ᵍ := -- begin @@ -449,144 +93,8 @@ end -- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) := -- idp - definition inv_homotopy_inv {A B : Type} {f g : A → B} [is_equiv f] [is_equiv g] - (p : f ~ g) : f⁻¹ ~ g⁻¹ := - λa, inv_eq_of_eq (p (g⁻¹ a) ⬝ right_inv g a)⁻¹ - - definition to_inv_homotopy_inv {A B : Type} {f g : A ≃ B} - (p : f ~ g) : f⁻¹ ~ g⁻¹ := - inv_homotopy_inv p - - definition compose2 {A B C : Type} {g g' : B → C} {f f' : A → B} - (p : g ~ g') (q : f ~ f') : g ∘ f ~ g' ∘ f' := - hwhisker_right f p ⬝hty hwhisker_left g' q - - section hsquare - variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} - {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀} - {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₄₁ : A₄₀ → A₄₂} - {f₁₂ : A₀₂ → A₂₂} {f₃₂ : A₂₂ → A₄₂} - {f₀₃ : A₀₂ → A₀₄} {f₂₃ : A₂₂ → A₂₄} {f₄₃ : A₄₂ → A₄₄} - {f₁₄ : A₀₄ → A₂₄} {f₃₄ : A₂₄ → A₄₄} - - definition hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂) - (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type := - f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ - - definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := - p - - definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := - p - - definition homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := - homotopy_inv_of_homotopy_post _ _ _ p - - definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := - homotopy_inv_of_homotopy_post _ _ _ p - - definition hhconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : - hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ := - hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p - - definition hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : - hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) := - (hhconcat p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ - - definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := - λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b)) - - definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := - (hhinverse p⁻¹ʰᵗʸ)⁻¹ʰᵗʸ - - infix ` ⬝htyh `:73 := hhconcat - infix ` ⬝htyv `:73 := hvconcat - postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse - postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse - - end hsquare - -- move to init.funext - protected definition homotopy.rec_on_idp_left [recursor] {A : Type} {P : A → Type} {g : Πa, P a} - {Q : Πf, (f ~ g) → Type} {f : Π x, P x} - (p : f ~ g) (H : Q g (homotopy.refl g)) : Q f p := - begin - induction p using homotopy.rec_on, induction q, exact H - end - - --eq2 (duplicate of ap_compose_ap02_constant) - definition ap02_ap_constant {A B C : Type} {a a' : A} (f : B → C) (b : B) (p : a = a') : - square (ap_constant p (f b)) (ap02 f (ap_constant p b)) (ap_compose f (λx, b) p) idp := - by induction p; exact ids - - definition ap_constant_compose {A B C : Type} {a a' : A} (c : C) (f : A → B) (p : a = a') : - square (ap_constant p c) (ap_constant (ap f p) c) (ap_compose (λx, c) f p) idp := - by induction p; exact ids - - definition ap02_constant {A B : Type} {a a' : A} (b : B) {p p' : a = a'} - (q : p = p') : square (ap_constant p b) (ap_constant p' b) (ap02 (λx, b) q) idp := - by induction q; exact vrfl - end eq open eq -namespace wedge - open pushout unit - protected definition glue (A B : Type*) : inl pt = inr pt :> wedge A B := - pushout.glue ⋆ - -end wedge - -namespace nat - - definition iterate_succ {A : Type} (f : A → A) (n : ℕ) (x : A) : - f^[succ n] x = f^[n] (f x) := - by induction n with n p; reflexivity; exact ap f p - - lemma iterate_sub {A : Type} (f : A ≃ A) {n m : ℕ} (h : n ≥ m) (a : A) : - iterate f (n - m) a = iterate f n (iterate f⁻¹ m a) := - begin - revert n h, induction m with m p: intro n h, - { reflexivity }, - { cases n with n, exfalso, apply not_succ_le_zero _ h, - rewrite [succ_sub_succ], refine p n (le_of_succ_le_succ h) ⬝ _, - refine ap (f^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ } - end - - definition iterate_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) : - iterate f n ∘ g ~ g ∘ iterate f n := - by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h - - definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A := - equiv.mk (iterate f n) - (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n)) - - definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) : - (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n := - begin - induction n with n p: intro a, - reflexivity, - exact p (f⁻¹ a) ⬝ !iterate_succ⁻¹ - end - - definition iterate_left_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f⁻¹ᵉ^[n] (f^[n] a) = a := - (iterate_inv f n (f^[n] a))⁻¹ ⬝ to_left_inv (iterate_equiv f n) a - - definition iterate_right_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f^[n] (f⁻¹ᵉ^[n] a) = a := - ap (f^[n]) (iterate_inv f n a)⁻¹ ⬝ to_right_inv (iterate_equiv f n) a - -end nat - -namespace pi - - definition is_contr_pi_of_neg {A : Type} (B : A → Type) (H : ¬ A) : is_contr (Πa, B a) := - begin - apply is_contr.mk (λa, empty.elim (H a)), intro f, apply eq_of_homotopy, intro x, contradiction - end -end pi - namespace trunc -- TODO: redefine loopn_ptrunc_pequiv @@ -625,69 +133,8 @@ namespace trunc end trunc -namespace is_equiv - - definition inv_homotopy_inv {A B : Type} {f g : A → B} [is_equiv f] [is_equiv g] (p : f ~ g) - : f⁻¹ ~ g⁻¹ := - λb, (left_inv g (f⁻¹ b))⁻¹ ⬝ ap g⁻¹ ((p (f⁻¹ b))⁻¹ ⬝ right_inv f b) - - definition to_inv_homotopy_to_inv {A B : Type} {f g : A ≃ B} (p : f ~ g) : f⁻¹ᵉ ~ g⁻¹ᵉ := - inv_homotopy_inv p - -end is_equiv - -namespace prod - - definition pprod_functor [constructor] {A B C D : Type*} (f : A →* C) (g : B →* D) : A ×* B →* C ×* D := - pmap.mk (prod_functor f g) (prod_eq (respect_pt f) (respect_pt g)) - - open prod.ops - definition prod_pathover_equiv {A : Type} {B C : A → Type} {a a' : A} (p : a = a') - (x : B a × C a) (x' : B a' × C a') : x =[p] x' ≃ x.1 =[p] x'.1 × x.2 =[p] x'.2 := - begin - fapply equiv.MK, - { intro q, induction q, constructor: constructor }, - { intro v, induction v with q r, exact prod_pathover _ _ _ q r }, - { intro v, induction v with q r, induction x with b c, induction x' with b' c', - esimp at *, induction q, refine idp_rec_on r _, reflexivity }, - { intro q, induction q, induction x with b c, reflexivity } - end - -end prod open prod - namespace sigma - -- set_option pp.notation false - -- set_option pp.binder_types true - - open sigma.ops - definition pathover_pr1 [unfold 9] {A : Type} {B : A → Type} {C : Πa, B a → Type} - {a a' : A} {p : a = a'} {x : Σb, C a b} {x' : Σb', C a' b'} - (q : x =[p] x') : x.1 =[p] x'.1 := - begin induction q, constructor end - - definition is_prop_elimo_self {A : Type} (B : A → Type) {a : A} (b : B a) {H : is_prop (B a)} : - @is_prop.elimo A B a a idp b b H = idpo := - !is_prop.elim - - definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} (C : Πa, B a → Type) - {a a' : A} (p : a = a') (x : Σb, C a b) (x' : Σb', C a' b') - [Πa b, is_prop (C a b)] : x =[p] x' ≃ x.1 =[p] x'.1 := - begin - fapply equiv.MK, - { exact pathover_pr1 }, - { intro q, induction x with b c, induction x' with b' c', esimp at q, induction q, - apply pathover_idp_of_eq, exact sigma_eq idp !is_prop.elimo }, - { intro q, induction x with b c, induction x' with b' c', esimp at q, induction q, - have c = c', from !is_prop.elim, induction this, - rewrite [▸*, is_prop_elimo_self (C a) c] }, - { intro q, induction q, induction x with b c, rewrite [▸*, is_prop_elimo_self (C a) c] } - end - - definition sigma_ua {A B : Type} (C : A ≃ B → Type) : - (Σ(p : A = B), C (equiv_of_eq p)) ≃ Σ(e : A ≃ B), C e := - sigma_equiv_sigma_left' !eq_equiv_equiv - -- definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} {C : Πa, B a → Type} -- {a a' : A} {p : a = a'} {b : B a} {b' : B a'} {c : C a b} {c' : C a' b'} -- [Πa b, is_prop (C a b)] : ⟨b, c⟩ =[p] ⟨b', c'⟩ ≃ b =[p] b' := @@ -704,159 +151,7 @@ namespace sigma end sigma open sigma -namespace pointed - - definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g := - begin - fapply phomotopy.mk, - { exact h }, - { apply is_set.elim } - end - -end pointed open pointed - namespace group - open is_trunc algebra - - definition to_fun_isomorphism_trans {G H K : Group} (φ : G ≃g H) (ψ : H ≃g K) : - φ ⬝g ψ ~ ψ ∘ φ := - by reflexivity - - definition add_homomorphism (G H : AddGroup) : Type := homomorphism G H - infix ` →a `:55 := add_homomorphism - - definition agroup_fun [coercion] [unfold 3] [reducible] {G H : AddGroup} (φ : G →a H) : G → H := - φ - - definition add_homomorphism.struct [instance] {G H : AddGroup} (φ : G →a H) : is_add_hom φ := - homomorphism.addstruct φ - - definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →g H := - homomorphism.mk φ h - - definition add_homomorphism_compose [constructor] [trans] {G₁ G₂ G₃ : AddGroup} - (ψ : G₂ →a G₃) (φ : G₁ →a G₂) : G₁ →a G₃ := - add_homomorphism.mk (ψ ∘ φ) (is_add_hom_compose _ _) - - definition add_homomorphism_id [constructor] [refl] (G : AddGroup) : G →a G := - add_homomorphism.mk (@id G) (is_add_hom_id G) - - abbreviation aid [constructor] := @add_homomorphism_id - infixr ` ∘a `:75 := add_homomorphism_compose - - definition to_respect_add' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g h : H₁) : χ (g + h) = χ g + χ h := - respect_add χ g h - - theorem to_respect_zero' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) : χ 0 = 0 := - respect_zero χ - - theorem to_respect_neg' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g : H₁) : χ (-g) = -(χ g) := - respect_neg χ g - - definition homomorphism_add [constructor] {G H : AddAbGroup} (φ ψ : G →a H) : G →a H := - add_homomorphism.mk (λg, φ g + ψ g) - abstract begin - intro g g', refine ap011 add !to_respect_add' !to_respect_add' ⬝ _, - refine !add.assoc ⬝ ap (add _) (!add.assoc⁻¹ ⬝ ap (λx, x + _) !add.comm ⬝ !add.assoc) ⬝ !add.assoc⁻¹ - end end - - definition homomorphism_mul [constructor] {G H : AbGroup} (φ ψ : G →g H) : G →g H := - homomorphism.mk (λg, φ g * ψ g) (to_respect_add (homomorphism_add φ ψ)) - - definition pmap_of_homomorphism_gid (G : Group) : pmap_of_homomorphism (gid G) ~* pid G := - begin - fapply phomotopy_of_homotopy, reflexivity - end - - definition pmap_of_homomorphism_gcompose {G H K : Group} (ψ : H →g K) (φ : G →g H) - : pmap_of_homomorphism (ψ ∘g φ) ~* pmap_of_homomorphism ψ ∘* pmap_of_homomorphism φ := - begin - fapply phomotopy_of_homotopy, reflexivity - end - - definition pmap_of_homomorphism_phomotopy {G H : Group} {φ ψ : G →g H} (H : φ ~ ψ) - : pmap_of_homomorphism φ ~* pmap_of_homomorphism ψ := - begin - fapply phomotopy_of_homotopy, exact H - end - - definition pequiv_of_isomorphism_trans {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₂) : - pequiv_of_isomorphism (φ ⬝g ψ) ~* pequiv_of_isomorphism ψ ∘* pequiv_of_isomorphism φ := - begin - apply phomotopy_of_homotopy, reflexivity - end - - definition isomorphism_eq {G H : Group} {φ ψ : G ≃g H} (p : φ ~ ψ) : φ = ψ := - begin - induction φ with φ φe, induction ψ with ψ ψe, - exact apd011 isomorphism.mk (homomorphism_eq p) !is_prop.elimo - end - - definition is_set_isomorphism [instance] (G H : Group) : is_set (G ≃g H) := - begin - have H : G ≃g H ≃ Σ(f : G →g H), is_equiv f, - begin - fapply equiv.MK, - { intro φ, induction φ, constructor, assumption }, - { intro v, induction v, constructor, assumption }, - { intro v, induction v, reflexivity }, - { intro φ, induction φ, reflexivity } - end, - apply is_trunc_equiv_closed_rev, exact H - end - - definition is_equiv_mul_right [constructor] {A : Group} (a : A) : is_equiv (λb, b * a) := - adjointify _ (λb : A, b * a⁻¹) (λb, !inv_mul_cancel_right) (λb, !mul_inv_cancel_right) - - definition right_action [constructor] {A : Group} (a : A) : A ≃ A := - equiv.mk _ (is_equiv_mul_right a) - - definition is_equiv_add_right [constructor] {A : AddGroup} (a : A) : is_equiv (λb, b + a) := - adjointify _ (λb : A, b - a) (λb, !neg_add_cancel_right) (λb, !add_neg_cancel_right) - - definition add_right_action [constructor] {A : AddGroup} (a : A) : A ≃ A := - equiv.mk _ (is_equiv_add_right a) - - section - variables {A B : Type} (f : A ≃ B) [ab_group A] - definition group_equiv_mul_comm (b b' : B) : group_equiv_mul f b b' = group_equiv_mul f b' b := - by rewrite [↑group_equiv_mul, mul.comm] - - definition ab_group_equiv_closed : ab_group B := - ⦃ab_group, group_equiv_closed f, - mul_comm := group_equiv_mul_comm f⦄ - end - - definition ab_group_of_is_contr (A : Type) [is_contr A] : ab_group A := - have ab_group unit, from ab_group_unit, - ab_group_equiv_closed (equiv_unit_of_is_contr A)⁻¹ᵉ - - definition group_of_is_contr (A : Type) [is_contr A] : group A := - have ab_group A, from ab_group_of_is_contr A, by apply _ - - definition ab_group_lift_unit : ab_group (lift unit) := - ab_group_of_is_contr (lift unit) - - definition trivial_ab_group_lift : AbGroup := - AbGroup.mk _ ab_group_lift_unit - - definition homomorphism_of_is_contr_right (A : Group) {B : Type} (H : is_contr B) : - A →g Group.mk B (group_of_is_contr B) := - group.homomorphism.mk (λa, center _) (λa a', !is_prop.elim) - - open trunc pointed is_conn - definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] : - ab_group (π[n] A) := - begin - have is_conn 0 A, from !is_conn_of_is_conn_succ, - cases n with n, - { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, - cases n with n, - { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, - exact ab_group_homotopy_group n A - end - - -- definition is_equiv_isomorphism @@ -879,49 +174,6 @@ end group open group namespace function variables {A B : Type} {f f' : A → B} - definition is_embedding_homotopy_closed (p : f ~ f') (H : is_embedding f) : is_embedding f' := - begin - intro a a', fapply is_equiv_of_equiv_of_homotopy, - exact equiv.mk (ap f) _ ⬝e equiv_eq_closed_left _ (p a) ⬝e equiv_eq_closed_right _ (p a'), - intro q, esimp, exact (eq_bot_of_square (transpose (natural_square p q)))⁻¹ - end - - definition is_embedding_homotopy_closed_rev (p : f' ~ f) (H : is_embedding f) : is_embedding f' := - is_embedding_homotopy_closed p⁻¹ʰᵗʸ H - - definition is_surjective_homotopy_closed (p : f ~ f') (H : is_surjective f) : is_surjective f' := - begin - intro b, induction H b with a q, - exact image.mk a ((p a)⁻¹ ⬝ q) - end - - definition is_surjective_homotopy_closed_rev (p : f' ~ f) (H : is_surjective f) : - is_surjective f' := - is_surjective_homotopy_closed p⁻¹ʰᵗʸ H - - definition is_equiv_ap1_gen_of_is_embedding {A B : Type} (f : A → B) [is_embedding f] - {a a' : A} {b b' : B} (q : f a = b) (q' : f a' = b') : is_equiv (ap1_gen f q q') := - begin - induction q, induction q', - exact is_equiv.homotopy_closed _ (ap1_gen_idp_left f)⁻¹ʰᵗʸ, - end - - definition is_equiv_ap1_of_is_embedding {A B : Type*} (f : A →* B) [is_embedding f] : - is_equiv (Ω→ f) := - is_equiv_ap1_gen_of_is_embedding f (respect_pt f) (respect_pt f) - - definition loop_pequiv_loop_of_is_embedding [constructor] {A B : Type*} (f : A →* B) - [is_embedding f] : Ω A ≃* Ω B := - pequiv_of_pmap (Ω→ f) (is_equiv_ap1_of_is_embedding f) - - definition loopn_pequiv_loopn_of_is_embedding [constructor] (n : ℕ) [H : is_succ n] - {A B : Type*} (f : A →* B) [is_embedding f] : Ω[n] A ≃* Ω[n] B := - begin - induction H with n, - exact !loopn_succ_in ⬝e* - loopn_pequiv_loopn n (loop_pequiv_loop_of_is_embedding f) ⬝e* - !loopn_succ_in⁻¹ᵉ* - end definition homotopy_group_isomorphism_of_is_embedding (n : ℕ) [H : is_succ n] {A B : Type*} (f : A →* B) [H2 : is_embedding f] : πg[n] A ≃g πg[n] B := @@ -935,281 +187,18 @@ namespace function end function open function -namespace fiber - open pointed - - definition pcompose_ppoint {A B : Type*} (f : A →* B) : f ∘* ppoint f ~* pconst (pfiber f) B := - begin - fapply phomotopy.mk, - { exact point_eq }, - { exact !idp_con⁻¹ } - end - - definition point_fiber_eq {A B : Type} {f : A → B} {b : B} {x y : fiber f b} - (p : point x = point y) (q : point_eq x = ap f p ⬝ point_eq y) : - ap point (fiber_eq p q) = p := - begin - induction x with a r, induction y with a' s, esimp at *, induction p, - induction q using eq.rec_symm, induction s, reflexivity - end - - definition fiber_eq_equiv_fiber {A B : Type} {f : A → B} {b : B} (x y : fiber f b) : - 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 - ... ≃ Σ(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, - calc point_eq x =[p] point_eq y ≃ point_eq x = ap f p ⬝ point_eq y : eq_pathover_equiv_Fl - ... ≃ ap f p ⬝ point_eq y = point_eq x : eq_equiv_eq_symm - ... ≃ (point_eq x)⁻¹ ⬝ (ap f p ⬝ point_eq y) = idp : eq_equiv_inv_con_eq_idp - ... ≃ (point_eq x)⁻¹ ⬝ ap f p ⬝ point_eq y = idp : equiv_eq_closed_left _ !con.assoc⁻¹) - ... ≃ fiber (ap1_gen f (point_eq x) (point_eq y)) (idpath b) : fiber.sigma_char - - definition loop_pfiber [constructor] {A B : Type*} (f : A →* B) : Ω (pfiber f) ≃* pfiber (Ω→ f) := - pequiv_of_equiv (fiber_eq_equiv_fiber pt pt) - begin - induction f with f f₀, induction B with B b₀, esimp at (f,f₀), induction f₀, reflexivity - end - - definition point_fiber_eq_equiv_fiber {A B : Type} {f : A → B} {b : B} {x y : fiber f b} - (p : x = y) : point (fiber_eq_equiv_fiber x y p) = ap1_gen point idp idp p := - by induction p; reflexivity - - lemma ppoint_loop_pfiber {A B : Type*} (f : A →* B) : - ppoint (Ω→ f) ∘* loop_pfiber f ~* Ω→ (ppoint f) := - phomotopy.mk (point_fiber_eq_equiv_fiber) - begin - induction f with f f₀, induction B with B b₀, esimp at (f,f₀), induction f₀, reflexivity - end - - lemma ppoint_loop_pfiber_inv {A B : Type*} (f : A →* B) : - Ω→ (ppoint f) ∘* (loop_pfiber f)⁻¹ᵉ* ~* ppoint (Ω→ f) := - (phomotopy_pinv_right_of_phomotopy (ppoint_loop_pfiber f))⁻¹* - - -- rename to pfiber_pequiv_... - lemma pfiber_equiv_of_phomotopy_ppoint {A B : Type*} {f g : A →* B} (h : f ~* g) - : ppoint g ∘* pfiber_equiv_of_phomotopy h ~* ppoint f := - begin - induction f with f f₀, induction g with g g₀, induction h with h h₀, induction B with B b₀, - esimp at *, induction h₀, induction g₀, - fapply phomotopy.mk, - { reflexivity }, - { esimp [pfiber_equiv_of_phomotopy], exact !point_fiber_eq⁻¹ } - end - - lemma pequiv_postcompose_ppoint {A B B' : Type*} (f : A →* B) (g : B ≃* B') - : ppoint f ∘* fiber.pequiv_postcompose f g ~* ppoint (g ∘* f) := - begin - induction f with f f₀, induction g with g hg g₀, induction B with B b₀, - induction B' with B' b₀', esimp at *, induction g₀, induction f₀, - fapply phomotopy.mk, - { reflexivity }, - { esimp [pequiv_postcompose], symmetry, - refine !ap_compose⁻¹ ⬝ _, apply ap_constant } - end - - lemma pequiv_precompose_ppoint {A A' B : Type*} (f : A →* B) (g : A' ≃* A) - : ppoint f ∘* fiber.pequiv_precompose f g ~* g ∘* ppoint (f ∘* g) := - begin - induction f with f f₀, induction g with g hg g₀, induction B with B b₀, - induction A with A a₀', esimp at *, induction g₀, induction f₀, - reflexivity, - end - - definition pfiber_equiv_of_square_ppoint {A B C D : Type*} {f : A →* B} {g : C →* D} - (h : A ≃* C) (k : B ≃* D) (s : k ∘* f ~* g ∘* h) - : ppoint g ∘* pfiber_equiv_of_square h k s ~* h ∘* ppoint f := - begin - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ !pequiv_precompose_ppoint ⬝* _, - refine !passoc ⬝* _, - apply pwhisker_left, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ !pfiber_equiv_of_phomotopy_ppoint ⬝* _, - apply pinv_right_phomotopy_of_phomotopy, - refine !pequiv_postcompose_ppoint⁻¹*, - end - - definition is_trunc_fiber [instance] (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) - [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (fiber f b) := - is_trunc_equiv_closed_rev n !fiber.sigma_char - - definition is_trunc_pfiber [instance] (n : ℕ₋₂) {A B : Type*} (f : A →* B) - [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) := - is_trunc_fiber n f pt - - definition fiber_equiv_of_is_contr [constructor] {A B : Type} (f : A → B) (b : B) [is_contr B] : - fiber f b ≃ A := - !fiber.sigma_char ⬝e !sigma_equiv_of_is_contr_right - - definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] : - pfiber f ≃* A := - pequiv_of_equiv (fiber_equiv_of_is_contr f pt) idp - -end fiber - -namespace is_trunc - - definition center' {A : Type} (H : is_contr A) : A := center A - - definition pequiv_punit_of_is_contr [constructor] (A : Type*) (H : is_contr A) : A ≃* punit := - pequiv_of_equiv (equiv_unit_of_is_contr A) (@is_prop.elim unit _ _ _) - - definition pequiv_punit_of_is_contr' [constructor] (A : Type) (H : is_contr A) - : pointed.MK A (center A) ≃* punit := - pequiv_punit_of_is_contr (pointed.MK A (center A)) H - - -definition is_trunc_is_contr_fiber [instance] [priority 900] (n : ℕ₋₂) {A B : Type} (f : A → B) - (b : B) [is_trunc n A] [is_trunc n B] : is_trunc n (is_contr (fiber f b)) := -begin - cases n, - { apply is_contr_of_inhabited_prop, apply is_contr_fun_of_is_equiv, - apply is_equiv_of_is_contr }, - { apply is_trunc_succ_of_is_prop } -end - - -- don't make is_prop_is_trunc an instance - definition is_trunc_succ_is_trunc [instance] (n m : ℕ₋₂) (A : Type) : - is_trunc (n.+1) (is_trunc m A) := - !is_trunc_succ_of_is_prop - -end is_trunc - namespace is_conn open unit trunc_index nat is_trunc pointed.ops - definition is_conn_equiv_closed_rev (n : ℕ₋₂) {A B : Type} (f : A ≃ B) (H : is_conn n B) : - is_conn n A := - is_conn_equiv_closed n f⁻¹ᵉ _ - - definition is_conn_succ_intro {n : ℕ₋₂} {A : Type} (a : trunc (n.+1) A) - (H2 : Π(a a' : A), is_conn n (a = a')) : is_conn (n.+1) A := - begin - apply @is_contr_of_inhabited_prop, - { apply is_trunc_succ_intro, - refine trunc.rec _, intro a, refine trunc.rec _, intro a', - apply is_contr_equiv_closed !tr_eq_tr_equiv⁻¹ᵉ }, - exact a - end - - definition is_conn_pathover (n : ℕ₋₂) {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a) - (b' : B a') [is_conn (n.+1) (B a')] : is_conn n (b =[p] b') := - is_conn_equiv_closed_rev n !pathover_equiv_tr_eq _ - - lemma is_conn_sigma [instance] {A : Type} (B : A → Type) (n : ℕ₋₂) - [HA : is_conn n A] [HB : Πa, is_conn n (B a)] : is_conn n (Σa, B a) := - begin - revert A B HA HB, induction n with n IH: intro A B HA HB, - { apply is_conn_minus_two }, - apply is_conn_succ_intro, - { induction center (trunc (n.+1) A) with a, induction center (trunc (n.+1) (B a)) with b, - exact tr ⟨a, b⟩ }, - intro a a', refine is_conn_equiv_closed_rev n !sigma_eq_equiv _, - apply IH, apply is_conn_eq, intro p, apply is_conn_pathover - /- an alternative proof of the successor case -/ - -- induction center (trunc (n.+1) A) with a₀, - -- induction center (trunc (n.+1) (B a₀)) with b₀, - -- apply is_contr.mk (tr ⟨a₀, b₀⟩), - -- intro ab, induction ab with ab, induction ab with a b, - -- induction tr_eq_tr_equiv n a₀ a !is_prop.elim with p, induction p, - -- induction tr_eq_tr_equiv n b₀ b !is_prop.elim with q, induction q, - -- reflexivity - end - - lemma is_conn_prod [instance] (A B : Type) (n : ℕ₋₂) [is_conn n A] [is_conn n B] : - is_conn n (A × B) := - is_conn_equiv_closed n !sigma.equiv_prod _ - - lemma is_conn_fun_of_is_conn {A B : Type} (n : ℕ₋₂) (f : A → B) - [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn_fun n f := - λb, is_conn_equiv_closed_rev n !fiber.sigma_char _ - - lemma is_conn_pfiber {A B : Type*} (n : ℕ₋₂) (f : A →* B) - [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn n (pfiber f) := - is_conn_fun_of_is_conn n f pt - - definition is_conn_fun_trunc_elim_of_le {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) - (H : k ≤ n) [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := - begin - apply is_conn_fun.intro, - intro P, have Πb, is_trunc n (P b), from (λb, is_trunc_of_le _ H), - fconstructor, - { intro f' b, - refine is_conn_fun.elim k H2 _ _ b, intro a, exact f' (tr a) }, - { intro f', apply eq_of_homotopy, intro a, - induction a with a, esimp, rewrite [is_conn_fun.elim_β] } - end - - definition is_conn_fun_trunc_elim_of_ge {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) - (H : n ≤ k) [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := - 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, - apply is_equiv_of_equiv_of_homotopy (equiv.mk (trunc_functor n f) _ ⬝e !trunc_equiv), - intro x, induction x, reflexivity - end - - definition is_conn_fun_trunc_elim {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) - [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := - begin - eapply algebra.le_by_cases k n: intro H, - { exact is_conn_fun_trunc_elim_of_le f H }, - { exact is_conn_fun_trunc_elim_of_ge f H } - end - - lemma is_conn_fun_tr (n : ℕ₋₂) (A : Type) : is_conn_fun n (tr : A → trunc n A) := - begin - apply is_conn_fun.intro, - intro P, - fconstructor, - { intro f' b, induction b with a, exact f' a }, - { intro f', reflexivity } - end - - - definition is_contr_of_is_conn_of_is_trunc {n : ℕ₋₂} {A : Type} (H : is_trunc n A) - (K : is_conn n A) : is_contr A := - is_contr_equiv_closed (trunc_equiv n A) - definition is_conn_fun_compose {n : ℕ₋₂} {A B C : Type} (g : B → C) (f : A → B) (H : is_conn_fun n g) (K : is_conn_fun n f) : is_conn_fun n (g ∘ f) := sorry - definition is_contr_of_trivial_homotopy' (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn -1 A] - (H : Πk a, is_contr (π[k] (pointed.MK A a))) : is_contr A := - begin - assert aa : trunc -1 A, - { apply center }, - assert H3 : is_conn 0 A, - { induction aa with a, exact H 0 a }, - exact is_contr_of_trivial_homotopy n A H - end - - definition is_conn_of_trivial_homotopy (n : ℕ₋₂) (m : ℕ) (A : Type) [is_trunc n A] [is_conn 0 A] - (H : Π(k : ℕ) a, k ≤ m → is_contr (π[k] (pointed.MK A a))) : is_conn m A := - begin - apply is_contr_of_trivial_homotopy_nat m (trunc m A), - intro k a H2, - induction a with a, - apply is_trunc_equiv_closed_rev, - exact equiv_of_pequiv (homotopy_group_trunc_of_le (pointed.MK A a) _ _ H2), - exact H k a H2 - end - - definition is_conn_of_trivial_homotopy_pointed (n : ℕ₋₂) (m : ℕ) (A : Type*) [is_trunc n A] - (H : Π(k : ℕ), k ≤ m → is_contr (π[k] A)) : is_conn m A := - begin - have is_conn 0 A, proof H 0 !zero_le qed, - apply is_conn_of_trivial_homotopy n m A, - intro k a H2, revert a, apply is_conn.elim -1, - cases A with A a, exact H k H2 - end +end is_conn +namespace misc + open is_conn /- move! -/ open sigma.ops pointed definition merely_constant {A B : Type} (f : A → B) : Type := @@ -1302,102 +291,10 @@ namespace is_conn /- extra condition, something like trunc_functor 0 f is an embedding -/ : pfiber f ≃* component A := sorry -end is_conn - -namespace circle - -/- - Suppose for `f, g : A -> B` I prove a homotopy `H : f ~ g` by induction on the element in `A`. - And suppose `p : a = a'` is a path constructor in `A`. - Then `natural_square_tr H p` has type `square (H a) (H a') (ap f p) (ap g p)` and is equal - to the square which defined H on the path constructor --/ - - definition natural_square_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base) - (q : square p p (ap f loop) (ap g loop)) - : natural_square (circle.rec p (eq_pathover q)) loop = q := - begin - -- refine !natural_square_eq ⬝ _, - refine ap square_of_pathover !rec_loop ⬝ _, - exact to_right_inv !eq_pathover_equiv_square q - end - - definition circle_elim_constant [unfold 5] {A : Type} {a : A} {p : a = a} (r : p = idp) (x : S¹) : - circle.elim a p x = a := - begin - induction x, - { reflexivity }, - { apply eq_pathover_constant_right, apply hdeg_square, exact !elim_loop ⬝ r } - end - - - -end circle - -namespace susp - - definition loop_psusp_intro_natural {X Y Z : Type*} (g : psusp Y →* Z) (f : X →* Y) : - loop_psusp_intro (g ∘* psusp_functor f) ~* loop_psusp_intro g ∘* f := - pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_psusp_unit_natural⁻¹* ⬝* - !passoc⁻¹* - - definition psusp_functor_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : - psusp_functor f ~* psusp_functor g := - begin - fapply phomotopy.mk, - { intro x, induction x, - { reflexivity }, - { reflexivity }, - { apply eq_pathover, apply hdeg_square, esimp, refine !elim_merid ⬝ _ ⬝ !elim_merid⁻¹ᵖ, - exact ap merid (p a), }}, - { reflexivity }, - end - - definition psusp_functor_pid (A : Type*) : psusp_functor (pid A) ~* pid (psusp A) := - begin - fapply phomotopy.mk, - { intro x, induction x, - { reflexivity }, - { reflexivity }, - { apply eq_pathover_id_right, apply hdeg_square, apply elim_merid }}, - { reflexivity }, - end - - definition psusp_functor_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) : - psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f := - begin - fapply phomotopy.mk, - { intro x, induction x, - { reflexivity }, - { reflexivity }, - { apply eq_pathover, apply hdeg_square, esimp, - refine !elim_merid ⬝ _ ⬝ (ap_compose (psusp_functor g) _ _)⁻¹ᵖ, - refine _ ⬝ ap02 _ !elim_merid⁻¹, exact !elim_merid⁻¹ }}, - { reflexivity }, - end - - definition psusp_elim_psusp_functor {A B C : Type*} (g : B →* Ω C) (f : A →* B) : - psusp.elim g ∘* psusp_functor f ~* psusp.elim (g ∘* f) := - begin - refine !passoc ⬝* _, exact pwhisker_left _ !psusp_functor_pcompose⁻¹* - end - - definition psusp_elim_phomotopy {A B : Type*} {f g : A →* Ω B} (p : f ~* g) : psusp.elim f ~* psusp.elim g := - pwhisker_left _ (psusp_functor_phomotopy p) - - definition psusp_elim_natural {X Y Z : Type*} (g : Y →* Z) (f : X →* Ω Y) - : g ∘* psusp.elim f ~* psusp.elim (Ω→ g ∘* f) := - begin - refine _ ⬝* pwhisker_left _ !psusp_functor_pcompose⁻¹*, - refine !passoc⁻¹* ⬝* _ ⬝* !passoc, - exact pwhisker_right _ !loop_psusp_counit_natural - end - -end susp +end misc namespace category - -- replace precategory_group with precategory_Group (the former has a universe error) definition precategory_Group.{u} [instance] [constructor] : precategory.{u+1 u} Group := begin fapply precategory.mk, @@ -1597,13 +494,6 @@ end category namespace sphere - definition psphere_pequiv_iterate_psusp (n : ℕ) : psphere n ≃* iterate_psusp n pbool := - begin - induction n with n e, - { exact psphere_pequiv_pbool }, - { exact psusp_pequiv e } - end - -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) : -- f ~* pconst (S* n) (S* m) := -- begin @@ -1616,18 +506,13 @@ namespace sphere end sphere -definition image_pathover {A B : Type} (f : A → B) {x y : B} (p : x = y) (u : image f x) (v : image f y) : u =[p] v := - begin - apply is_prop.elimo - end - section injective_surjective open trunc fiber image -variables {A B C : Type} [is_set A] [is_set B] [is_set C] (f : A → B) (g : B → C) (h : A → C) (H : g ∘ f ~ h) -include H - -definition is_embedding_factor : is_embedding h → is_embedding f := + /- do we want to prove this without funext before we move it? -/ + variables {A B C : Type} (f : A → B) + definition is_embedding_factor [is_set A] [is_set B] (g : B → C) (h : A → C) (H : g ∘ f ~ h) : + is_embedding h → is_embedding f := begin induction H using homotopy.rec_on_idp, intro E, @@ -1636,7 +521,8 @@ definition is_embedding_factor : is_embedding h → is_embedding f := fapply @is_injective_of_is_embedding _ _ _ E _ _ (ap g p) end -definition is_surjective_factor : is_surjective h → is_surjective g := + definition is_surjective_factor (g : B → C) (h : A → C) (H : g ∘ f ~ h) : + is_surjective h → is_surjective g := begin induction H using homotopy.rec_on_idp, intro S, @@ -1650,194 +536,3 @@ definition is_surjective_factor : is_surjective h → is_surjective g := end end injective_surjective - -definition AbGroup_of_Group.{u} (G : Group.{u}) (H : Π x y : G, x * y = y * x) : AbGroup.{u} := -begin - induction G, - fapply AbGroup.mk, - assumption, - exact ⦃ab_group, struct, mul_comm := H⦄ -end - -definition trivial_ab_group : AbGroup.{0} := -begin - fapply AbGroup_of_Group Trivial_group, intro x y, reflexivity -end - -definition trivial_homomorphism (A B : AbGroup) : A →g B := -begin - fapply homomorphism.mk, - exact λ a, 1, - intros, symmetry, exact one_mul 1, -end - -definition from_trivial_ab_group (A : AbGroup) : trivial_ab_group →g A := - trivial_homomorphism trivial_ab_group A - -definition is_embedding_from_trivial_ab_group (A : AbGroup) : is_embedding (from_trivial_ab_group A) := - begin - fapply is_embedding_of_is_injective, - intro x y p, - induction x, induction y, reflexivity - end - -definition to_trivial_ab_group (A : AbGroup) : A →g trivial_ab_group := - trivial_homomorphism A trivial_ab_group - -/- Stuff added by Jeremy -/ - -definition exists.elim {A : Type} {p : A → Type} {B : Type} [is_prop B] (H : Exists p) - (H' : ∀ (a : A), p a → B) : B := -trunc.elim (sigma.rec H') H - -definition image.elim {A B : Type} {f : A → B} {C : Type} [is_prop C] {b : B} - (H : image f b) (H' : ∀ (a : A), f a = b → C) : C := -begin - refine (trunc.elim _ H), - intro H'', cases H'' with a Ha, exact H' a Ha -end - -definition image.intro {A B : Type} {f : A → B} {a : A} {b : B} (h : f a = b) : image f b := -begin - apply trunc.merely.intro, - apply fiber.mk, - exact h -end - -definition total_image {A B : Type} (f : A → B) : Type := sigma (image f) -local attribute is_prop.elim_set [recursor 6] -definition total_image.elim_set [unfold 8] - {A B : Type} {f : A → B} {C : Type} [is_set C] - (g : A → C) (h : Πa a', f a = f a' → g a = g a') (x : total_image f) : C := -begin - induction x with b v, - induction v using is_prop.elim_set with x x x', - { induction x with a p, exact g a }, - { induction x with a p, induction x' with a' p', induction p', exact h _ _ p } -end - -definition total_image.rec [unfold 7] - {A B : Type} {f : A → B} {C : total_image f → Type} [H : Πx, is_prop (C x)] - (g : Πa, C ⟨f a, image.mk a idp⟩) - (x : total_image f) : C x := -begin - induction x with b v, - refine @image.rec _ _ _ _ _ (λv, H ⟨b, v⟩) _ v, - intro a p, - induction p, exact g a -end - -definition image.equiv_exists {A B : Type} {f : A → B} {b : B} : image f b ≃ ∃ a, f a = b := -trunc_equiv_trunc _ (fiber.sigma_char _ _) - --- move to homomorphism.hlean -section - theorem eq_zero_of_eq_zero_of_is_embedding {A B : Type} [add_group A] [add_group B] - {f : A → B} [is_add_hom f] [is_embedding f] {a : A} (h : f a = 0) : a = 0 := - have f a = f 0, by rewrite [h, respect_zero], - show a = 0, from is_injective_of_is_embedding this -end - -/- put somewhere in algebra -/ - -structure Ring := -(carrier : Type) (struct : ring carrier) - -attribute Ring.carrier [coercion] -attribute Ring.struct [instance] - -namespace int - - definition ring_int : Ring := - Ring.mk ℤ _ - - notation `rℤ` := ring_int - - definition max0 : ℤ → ℕ - | (of_nat n) := n - | (-[1+ n]) := 0 - - lemma le_max0 : Π(n : ℤ), n ≤ of_nat (max0 n) - | (of_nat n) := proof le.refl n qed - | (-[1+ n]) := proof unit.star qed - - lemma le_of_max0_le {n : ℤ} {m : ℕ} (h : max0 n ≤ m) : n ≤ of_nat m := - le.trans (le_max0 n) (of_nat_le_of_nat_of_le h) - -end int - -namespace set_quotient - definition is_prop_set_quotient {A : Type} (R : A → A → Prop) [is_prop A] : is_prop (set_quotient R) := - begin - apply is_prop.mk, intro x y, - induction x using set_quotient.rec_prop, induction y using set_quotient.rec_prop, - exact ap class_of !is_prop.elim - end - - local attribute is_prop_set_quotient [instance] - definition is_trunc_set_quotient [instance] (n : ℕ₋₂) {A : Type} (R : A → A → Prop) [is_trunc n A] : - is_trunc n (set_quotient R) := - begin - cases n with n, { apply is_contr_of_inhabited_prop, exact class_of !center }, - cases n with n, { apply _ }, - apply is_trunc_succ_succ_of_is_set - end - - definition is_equiv_class_of [constructor] {A : Type} [is_set A] (R : A → A → Prop) - (p : Π⦃a b⦄, R a b → a = b) : is_equiv (@class_of A R) := - begin - fapply adjointify, - { intro x, induction x, exact a, exact p H }, - { intro x, induction x using set_quotient.rec_prop, reflexivity }, - { intro a, reflexivity } - end - - definition equiv_set_quotient [constructor] {A : Type} [is_set A] (R : A → A → Prop) - (p : Π⦃a b⦄, R a b → a = b) : A ≃ set_quotient R := - equiv.mk _ (is_equiv_class_of R p) - -end set_quotient - --- should be in pushout -namespace pushout -variables {TL BL TR : Type} (f : TL → BL) (g : TL → TR) - -protected theorem elim_inl {P : Type} (Pinl : BL → P) (Pinr : TR → P) - (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : BL} (p : b = b') - : ap (pushout.elim Pinl Pinr Pglue) (ap inl p) = ap Pinl p := -by cases p; reflexivity - -protected theorem elim_inr {P : Type} (Pinl : BL → P) (Pinr : TR → P) - (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : TR} (p : b = b') - : ap (pushout.elim Pinl Pinr Pglue) (ap inr p) = ap Pinr p := -by cases p; reflexivity - -end pushout - --- should be in prod -namespace prod -open prod.ops -definition pair_eq_eta {A B : Type} {u v : A × B} - (p : u = v) : pair_eq (p..1) (p..2) = prod.eta u ⬝ p ⬝ (prod.eta v)⁻¹ := -by induction p; induction u; reflexivity - -definition prod_eq_eq {A B : Type} {u v : A × B} - {p₁ q₁ : u.1 = v.1} {p₂ q₂ : u.2 = v.2} (α₁ : p₁ = q₁) (α₂ : p₂ = q₂) - : prod_eq p₁ p₂ = prod_eq q₁ q₂ := -by cases α₁; cases α₂; reflexivity - -definition prod_eq_assemble {A B : Type} {u v : A × B} - {p q : u = v} (α₁ : p..1 = q..1) (α₂ : p..2 = q..2) : p = q := -(prod_eq_eta p)⁻¹ ⬝ prod.prod_eq_eq α₁ α₂ ⬝ prod_eq_eta q - -definition eq_pr1_concat {A B : Type} {u v w : A × B} - (p : u = v) (q : v = w) - : (p ⬝ q)..1 = p..1 ⬝ q..1 := -by cases q; reflexivity - -definition eq_pr2_concat {A B : Type} {u v w : A × B} - (p : u = v) (q : v = w) - : (p ⬝ q)..2 = p..2 ⬝ q..2 := -by cases q; reflexivity - -end prod diff --git a/pointed.hlean b/pointed.hlean index ac5858b..8f1ea82 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -2,50 +2,12 @@ -- Author: Floris van Doorn -import .move_to_lib +import types.pointed2 -open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group sigma +open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group namespace pointed - 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) - - definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A := - begin - fapply phomotopy.mk, - { intro u, induction u, exact respect_pt f }, - { reflexivity } - end - - definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) := - is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*) - - definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f := - idp - - definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := - λx, idp - - definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) : - p a = q a := - ap010 to_homotopy r a - - definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B} - {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} - (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') (p : a = a') : - ap1_gen (λa, f a ⬝ f' a) (r₀ ◾ r₀') (r₁ ◾ r₁') p = - whisker_right q₀' (ap1_gen f r₀ r₁ p) ⬝ whisker_left q₁ (ap1_gen f' r₀' r₁' p) := - begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end - - definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B} - {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂} - (r₀ : f a = q₀) (r₁ : f' a = q₁) : - ap1_gen_con_left r₀ r₀ r₁ r₁ idp = - !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ := - begin induction r₀, induction r₁, reflexivity end - -- /- the pointed type of (unpointed) dependent maps -/ -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := -- pointed.mk' (Πa, P a) @@ -58,816 +20,6 @@ namespace pointed -- pequiv_of_equiv (pi_equiv_pi_right g) -- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end - section psquare - /- - Squares of pointed maps - - We treat expressions of the form - psquare f g h k :≡ k ∘* f ~* g ∘* h - as squares, where f is the top, g is the bottom, h is the left face and k is the right face. - Then the following are operations on squares - -/ - - variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} - {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} - {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} - {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} - {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} - {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} - - definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) - (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type := - f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ - - definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ := - p - - definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ := - p - - definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' := - !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹* - definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid := - !pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹* - - variables (f₀₁ f₁₀) - definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl - definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl - variables {f₀₁ f₁₀} - definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁ - definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀ - - definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) : - psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ := - !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹* - - definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : - psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) := - !passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc - - definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ := - !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝* - pwhisker_left _ - (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid) - - definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* := - (phinverse p⁻¹*)⁻¹* - - definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₀ f₁₂ f₀₁' f₂₁ := - p ⬝* pwhisker_left f₁₂ q⁻¹* - - definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) : - psquare f₁₀ f₁₂ f₀₁ f₂₁' := - pwhisker_right f₁₀ q ⬝* p - - definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare f₁₀' f₁₂ f₀₁ f₂₁ := - pwhisker_left f₂₁ q ⬝* p - - definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) : - psquare f₁₀ f₁₂' f₀₁ f₂₁ := - p ⬝* pwhisker_right f₀₁ q⁻¹* - - infix ` ⬝h* `:73 := phconcat - infix ` ⬝v* `:73 := pvconcat - infixl ` ⬝hp* `:72 := hconcat_phomotopy - infixr ` ⬝ph* `:72 := phomotopy_hconcat - infixl ` ⬝vp* `:72 := vconcat_phomotopy - infixr ` ⬝pv* `:72 := phomotopy_vconcat - postfix `⁻¹ʰ*`:(max+1) := phinverse - postfix `⁻¹ᵛ*`:(max+1) := pvinverse - - definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ := - !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc - - definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) := - !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose - - definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) := - !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose - - definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂) - (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) := - !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose - - 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 - - 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₂₁) := - begin - induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p)) - end - - end psquare - - definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : - phomotopy_of_eq (eq_of_phomotopy p) = p := - to_right_inv (pmap_eq_equiv f g) p - - definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : - ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a := - ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a - - definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B} - {Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p := - phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p) - - definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B} - {Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p := - begin - induction p using phomotopy_rec_on_eq, - induction q, exact H - end - - definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B} - {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : - phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p := - begin - unfold phomotopy_rec_on_eq, - refine ap (λp, p ▸ _) !adj ⬝ _, - refine !tr_compose⁻¹ ⬝ _, - apply apdt - end - - definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B) - {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) : - phomotopy_rec_on_idp phomotopy.rfl H = H := - !phomotopy_rec_on_eq_phomotopy_of_eq - - 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 := - calc - h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k - : eq_equiv_fn_eq (phomotopy.sigma_char f g) h k - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k) - : sigma_eq_equiv _ _ - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k - : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k)) - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h - : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) - ... ≃ Σ(p : to_homotopy h = to_homotopy k), - whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h - : 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 - - 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 := - to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩ - - definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) - (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k := - phomotopy_eq p (eq_of_square q)⁻¹ - - definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) : - eq_of_phomotopy (phomotopy.refl f) = idpath f := - begin - apply to_inv_eq_of_eq, reflexivity - end - - definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p := - begin - induction A with A a₀, induction B with B b₀, - induction f with f f₀, induction g with g g₀, induction p with p p₀, - esimp at *, induction g₀, induction p₀, - reflexivity - end - - definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) : - eq_of_phomotopy (p ⬝* q) = eq_of_phomotopy p ⬝ eq_of_phomotopy q := - begin - induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, - exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹ - end - - definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p := - begin - induction p using phomotopy_rec_on_idp, - induction A with A a₀, induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity - end - - definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h) - (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := - begin - induction r using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - induction p using phomotopy_rec_on_idp, - induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity - end - - definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f := - begin - induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity - end - - definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p := - phomotopy_eq (λa, !inv_inv) - begin - induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀, - esimp at *, induction f₀, reflexivity - end - - definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl := - begin - induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm - end - - definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl := - begin - induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm - end - - definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h} - (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := - ap011 phomotopy.trans r s - - definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} - {p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' := - ap011 pcompose2 r s - - definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* := - ap phomotopy.symm r - - infixl ` ◾** `:80 := pointed.trans2 - infixl ` ◽* `:81 := pointed.pcompose3 - postfix `⁻²**`:(max+1) := pointed.symm2 - - definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) : - (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* := - begin - induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, - exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹ - end - - definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h} - (s : q = q') : p ⬝* q = p ⬝* q' := - idp ◾** s - - definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h) - (r : p = p') : p ⬝* q = p' ⬝* q := - r ◾** idp - - definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : - pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, - induction f with f f₀, induction g with g g₀, - esimp at *, induction g₀, induction f₀, reflexivity - end - - definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) : - pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, - induction f with f f₀, induction g with g g₀, - esimp at *, induction g₀, induction f₀, reflexivity - end - - definition pcompose2_refl {A B C : Type*} (g : B →* C) (f : A →* B) : - phomotopy.refl g ◾* phomotopy.refl f = phomotopy.rfl := - !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ !refl_trans - - definition pcompose2_refl_left {A B C : Type*} (g : B →* C) {f f' : A →* B} (p : f ~* f') : - phomotopy.rfl ◾* p = pwhisker_left g p := - !pwhisker_right_refl ◾** idp ⬝ !refl_trans - - definition pcompose2_refl_right {A B C : Type*} {g g' : B →* C} (f : A →* B) (p : g ~* g') : - p ◾* phomotopy.rfl = pwhisker_right f p := - idp ◾** !pwhisker_left_refl ⬝ !trans_refl - - definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B} - (p : f₁ ~* f₂) (q : f₂ ~* f₃) : - pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q := - begin - induction p using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹, - refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹ - end - - definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C} - (p : g₁ ~* g₂) (q : g₂ ~* g₃) : - pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q := - begin - induction p using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹, - refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹ - end - - definition pwhisker_left_symm {A B C : Type*} (g : B →* C) {f₁ f₂ : A →* B} (p : f₁ ~* f₂) : - pwhisker_left g p⁻¹* = (pwhisker_left g p)⁻¹* := - begin - induction p using phomotopy_rec_on_idp, - refine _ ⬝ ap phomotopy.symm !pwhisker_left_refl⁻¹, - refine ap (pwhisker_left g) !refl_symm ⬝ !pwhisker_left_refl ⬝ !refl_symm⁻¹ - end - - definition pwhisker_right_symm {A B C : Type*} (f : A →* B) {g₁ g₂ : B →* C} (p : g₁ ~* g₂) : - pwhisker_right f p⁻¹* = (pwhisker_right f p)⁻¹* := - begin - induction p using phomotopy_rec_on_idp, - refine _ ⬝ ap phomotopy.symm !pwhisker_right_refl⁻¹, - refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹ - end - - definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r := - idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans - - definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r := - !refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s - - definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r := - s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl - - definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := - !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp - - definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q := - !refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s - - definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q := - idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans - - definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q := - !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp - - definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p := - s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl - - section phsquare - /- - Squares of pointed homotopies - -/ - - variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} - {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} - {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} - {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} - {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄} - {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄} - - definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂) - (p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type := - p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ - - definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p - definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p - - -- definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x)) - -- (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂)) - -- (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁)) - -- (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := - -- begin - -- fapply phomotopy_eq, - -- { intro x, apply eq_of_square (p x) }, - -- { generalize p pt, intro r, exact sorry } - -- end - - - definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) : - phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ := - !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc - - definition phvconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) : - phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) := - (phhconcat p⁻¹ q⁻¹)⁻¹ - - definition phhdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare phomotopy.rfl phomotopy.rfl p₁ p₂ := - !refl_trans ⬝ q⁻¹ ⬝ !trans_refl⁻¹ - definition phvdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare p₁ p₂ phomotopy.rfl phomotopy.rfl := - !trans_refl ⬝ q ⬝ !refl_trans⁻¹ - - variables (p₀₁ p₁₀) - definition phhrefl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhdeg_square idp - definition phvrefl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvdeg_square idp - variables {p₀₁ p₁₀} - definition phhrfl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhrefl p₀₁ - definition phvrfl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvrefl p₁₀ - - /- - The names are very baroque. The following stands for - "pointed homotopy path-horizontal composition" (i.e. composition on the left with a path) - The names are obtained by using the ones for squares, and putting "ph" in front of it. - In practice, use the notation ⬝ph** defined below, which might be easier to remember - -/ - definition phphconcat {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare p₁₀ p₁₂ p₀₁' p₂₁ := - by induction p; exact q - - definition phhpconcat {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') : - phsquare p₁₀ p₁₂ p₀₁ p₂₁' := - by induction p; exact q - - definition phpvconcat {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare p₁₀' p₁₂ p₀₁ p₂₁ := - by induction p; exact q - - definition phvpconcat {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') : - phsquare p₁₀ p₁₂' p₀₁ p₂₁ := - by induction p; exact q - - definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ := - begin - refine (eq_symm_trans_of_trans_eq _)⁻¹, - refine !trans_assoc⁻¹ ⬝ _, - refine (eq_trans_symm_of_trans_eq _)⁻¹, - exact (eq_of_phsquare p)⁻¹ - end - - definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* := - (phhinverse p⁻¹)⁻¹ - - infix ` ⬝h** `:78 := phhconcat - infix ` ⬝v** `:78 := phvconcat - infixr ` ⬝ph** `:77 := phphconcat - infixl ` ⬝hp** `:77 := phhpconcat - infixr ` ⬝pv** `:77 := phpvconcat - infixl ` ⬝vp** `:77 := phvpconcat - postfix `⁻¹ʰ**`:(max+1) := phhinverse - postfix `⁻¹ᵛ**`:(max+1) := phvinverse - - definition phwhisker_rt (p : f ~* f₂₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare (p₁₀ ⬝* p⁻¹*) p₁₂ p₀₁ (p ⬝* p₂₁) := - !trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ !trans_left_inv ◾** idp ⬝ !refl_trans) ⬝ q - - definition phwhisker_br (p : f₂₂ ~* f) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare p₁₀ (p₁₂ ⬝* p) p₀₁ (p₂₁ ⬝* p) := - !trans_assoc⁻¹ ⬝ q ◾** idp ⬝ !trans_assoc - - definition phmove_top_of_left' {p₀₁ : f ~* f₀₂} (p : f₀₀ ~* f) - (q : phsquare p₁₀ p₁₂ (p ⬝* p₀₁) p₂₁) : phsquare (p⁻¹* ⬝* p₁₀) p₁₂ p₀₁ p₂₁ := - !trans_assoc ⬝ (eq_symm_trans_of_trans_eq (q ⬝ !trans_assoc)⁻¹)⁻¹ - - definition phmove_bot_of_left {p₀₁ : f₀₀ ~* f} (p : f ~* f₀₂) - (q : phsquare p₁₀ p₁₂ (p₀₁ ⬝* p) p₂₁) : phsquare p₁₀ (p ⬝* p₁₂) p₀₁ p₂₁ := - q ⬝ !trans_assoc - - definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B} - (p : f ~* f') : phsquare (passoc h g f) (passoc h g f') - (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) := - begin - induction p using phomotopy_rec_on_idp, - refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝ - !pwhisker_left_refl⁻¹ ◾** idp, - exact !trans_refl ⬝ !refl_trans⁻¹ - end - - theorem passoc_phomotopy_middle {A B C D : Type*} (h : C →* D) {g g' : B →* C} (f : A →* B) - (p : g ~* g') : phsquare (passoc h g f) (passoc h g' f) - (pwhisker_right f (pwhisker_left h p)) (pwhisker_left h (pwhisker_right f p)) := - begin - induction p using phomotopy_rec_on_idp, - rewrite [pwhisker_right_refl, pwhisker_left_refl], - rewrite [pwhisker_right_refl, pwhisker_left_refl], - exact phvrfl - end - - definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B} - (p : g ~* g') (q : f ~* f') : - phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) := - begin - induction p using phomotopy_rec_on_idp, - induction q using phomotopy_rec_on_idp, - exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ - !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹ - end - - definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂) - (pwhisker_left f p₀₁) (pwhisker_left f p₂₁) := - !pwhisker_left_trans⁻¹ ⬝ ap (pwhisker_left f) p ⬝ !pwhisker_left_trans - - definition pwhisker_right_phsquare (f : C →* A) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : - phsquare (pwhisker_right f p₁₀) (pwhisker_right f p₁₂) - (pwhisker_right f p₀₁) (pwhisker_right f p₂₁) := - !pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans - - end phsquare - - definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) : - phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q := - begin induction q, induction p, exact !trans_refl⁻¹ end - - definition pcompose_left_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B} - (H : f ~* f') : ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) := - begin - induction H using phomotopy_rec_on_idp, - refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, - exact !pwhisker_left_refl⁻¹ - end - - definition pcompose_right_eq_of_phomotopy {A B C : Type*} {g g' : B →* C} (f : A →* B) - (H : g ~* g') : ap (λg, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_right f H) := - begin - induction H using phomotopy_rec_on_idp, - refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, - exact !pwhisker_right_refl⁻¹ - end - - definition phomotopy_of_eq_pcompose_left {A B C : Type*} (g : B →* C) {f f' : A →* B} - (p : f = f') : phomotopy_of_eq (ap (λf, g ∘* f) p) = pwhisker_left g (phomotopy_of_eq p) := - begin - induction p, exact !pwhisker_left_refl⁻¹ - end - - definition phomotopy_of_eq_pcompose_right {A B C : Type*} {g g' : B →* C} (f : A →* B) - (p : g = g') : phomotopy_of_eq (ap (λg, g ∘* f) p) = pwhisker_right f (phomotopy_of_eq p) := - begin - induction p, exact !pwhisker_right_refl⁻¹ - end - - definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) : - ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) := - begin - -- induction X with X x₀, induction Y with Y y₀, induction f with f f₀, esimp at *, induction f₀, - -- fapply phomotopy_eq, - -- { intro x, unfold [ap1_phomotopy], }, - -- { } - exact sorry - end - - definition ap1_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : - ap Ω→ (eq_of_phomotopy p) = eq_of_phomotopy (ap1_phomotopy p) := - begin - induction p using phomotopy_rec_on_idp, - refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, - exact !ap1_phomotopy_refl⁻¹ - end - - -- duplicate of ap_eq_of_phomotopy - definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : - ap010 pmap.to_fun (eq_of_phomotopy p) a = p a := - begin - induction p using phomotopy_rec_on_idp, - exact ap (λx, ap010 pmap.to_fun x a) !eq_of_phomotopy_refl - end - - definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) - : respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g := - idp - - definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a) - (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) - : 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], - refine !phomotopy_of_eq_con ⬝ _, - refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, - end - - definition pconst_pcompose_pconst (A B C : Type*) : - pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) := - idp - - definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) : - pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) := - begin - assert H : Π(p : pconst A B ~* f), - pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C), - { intro p, induction p using phomotopy_rec_on_idp, reflexivity }, - refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp, - end - - definition passoc_pconst_right {A B C D : Type*} (h : C →* D) (g : B →* C) : - passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) = - pcompose_pconst (h ∘* g) := - begin - fapply phomotopy_eq, - { intro a, exact !idp_con }, - { induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀, - esimp at *, induction g₀, induction h₀, reflexivity } - end - - definition passoc_pconst_middle {A A' B B' : Type*} (g : B →* B') (f : A' →* A) : - passoc g (pconst A B) f ⬝* (pwhisker_left g (pconst_pcompose f) ⬝* pcompose_pconst g) = - pwhisker_right f (pcompose_pconst g) ⬝* pconst_pcompose f := - begin - fapply phomotopy_eq, - { intro a, exact !idp_con ⬝ !idp_con }, - { induction g with g g₀, induction f with f f₀, induction B' with D d₀, induction A with C c₀, - esimp at *, induction g₀, induction f₀, reflexivity } - end - - definition passoc_pconst_left {A B C D : Type*} (g : B →* C) (f : A →* B) : - phsquare (passoc (pconst C D) g f) (pconst_pcompose f) - (pwhisker_right f (pconst_pcompose g)) (pconst_pcompose (g ∘* f)) := - begin - fapply phomotopy_eq, - { intro a, exact !idp_con }, - { induction g with g g₀, induction f with f f₀, induction C with C c₀, induction B with B b₀, - esimp at *, induction g₀, induction f₀, reflexivity } - end - - definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) : - @ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g := - begin - fapply phomotopy_mk_ppmap, - { exact passoc h g }, - { refine idp ◾** (!phomotopy_of_eq_con ⬝ - (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, - exact passoc_pconst_right h g } - end - - definition ppcompose_right_pcompose [constructor] {A B C D : Type*} (g : B →* C) (f : A →* B) : - @ppcompose_right _ _ D (g ∘* f) ~* ppcompose_right f ∘* ppcompose_right g := - begin - symmetry, - fapply phomotopy_mk_ppmap, - { intro h, exact passoc h g f }, - { refine idp ◾** !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝ - (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, - exact passoc_pconst_left g f } - end - - definition ppcompose_left_ppcompose_right {A A' B B' : Type*} (g : B →* B') (f : A' →* A) : - psquare (ppcompose_left g) (ppcompose_left g) (ppcompose_right f) (ppcompose_right f) := - begin - fapply phomotopy_mk_ppmap, - { intro h, exact passoc g h f }, - { refine idp ◾** (!phomotopy_of_eq_con ⬝ - (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝ - (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** - !phomotopy_of_eq_of_phomotopy)⁻¹, - apply passoc_pconst_middle } - end - - definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') : - pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f := - begin - fapply phomotopy_eq, - { intro a, exact to_homotopy_pt p }, - { induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀, - esimp at *, induction f₀, reflexivity } - end - - definition pid_pconst (A B : Type*) : pcompose_pconst (pid B) = pid_pcompose (pconst A B) := - by reflexivity - - definition pid_pconst_pcompose {A B C : Type*} (f : A →* B) : - phsquare (pid_pcompose (pconst B C ∘* f)) - (pcompose_pconst (pid C)) - (pwhisker_left (pid C) (pconst_pcompose f)) - (pconst_pcompose f) := - begin - fapply phomotopy_eq, - { reflexivity }, - { induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, reflexivity } - end - - definition ppcompose_left_pconst [constructor] (A B C : Type*) : - @ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) := - begin - fapply phomotopy_mk_ppmap, - { exact pconst_pcompose }, - { refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ } - end - - definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') : - @ppcompose_left A _ _ g ~* ppcompose_left g' := - begin - induction p using phomotopy_rec_on_idp, - reflexivity - end - - definition ppcompose_right_phomotopy [constructor] {A B C : Type*} {f f' : A →* B} (p : f ~* f') : - @ppcompose_right _ _ C f ~* ppcompose_right f' := - begin - induction p using phomotopy_rec_on_idp, - reflexivity - end - - definition pppcompose [constructor] (A B C : Type*) : ppmap B C →* ppmap (ppmap A B) (ppmap A C) := - pmap.mk ppcompose_left (eq_of_phomotopy !ppcompose_left_pconst) - - section psquare - - variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} - {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} - {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} - {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} - {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} - {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} - - definition ppcompose_left_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (@ppcompose_left A _ _ f₁₀) (ppcompose_left f₁₂) - (ppcompose_left f₀₁) (ppcompose_left f₂₁) := - !ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose - - definition ppcompose_right_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - psquare (@ppcompose_right _ _ A f₁₂) (ppcompose_right f₁₀) - (ppcompose_right f₂₁) (ppcompose_right f₀₁) := - !ppcompose_right_pcompose⁻¹* ⬝* ppcompose_right_phomotopy p⁻¹* ⬝* !ppcompose_right_pcompose - - definition trans_phomotopy_hconcat {f₀₁' f₀₁''} - (q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : - (q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p := - idp ◾** (ap (pwhisker_left f₁₂) !trans_symm ⬝ !pwhisker_left_trans) ⬝ !trans_assoc⁻¹ - - definition symm_phomotopy_hconcat {f₀₁'} (q : f₀₁ ~* f₀₁') - (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : q⁻¹* ⬝ph* p = p ⬝* pwhisker_left f₁₂ q := - idp ◾** ap (pwhisker_left f₁₂) !symm_symm - - definition refl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p := - idp ◾** (ap (pwhisker_left _) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl - - local attribute phomotopy.rfl [reducible] - theorem pwhisker_left_phomotopy_hconcat {f₀₁'} (r : f₀₁' ~* f₀₁) - (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : - pwhisker_left f₀₃ r ⬝ph* (p ⬝v* q) = (r ⬝ph* p) ⬝v* q := - by induction r using phomotopy_rec_on_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat] - - theorem pvcompose_pwhisker_left {f₀₁'} (r : f₀₁ ~* f₀₁') - (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : - (p ⬝v* q) ⬝* (pwhisker_left f₁₄ (pwhisker_left f₀₃ r)) = (p ⬝* pwhisker_left f₁₂ r) ⬝v* q := - by induction r using phomotopy_rec_on_idp; rewrite [+pwhisker_left_refl, + trans_refl] - - definition phconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₃₀ f₃₂ f₂₁ f₄₁} - (r : p = p') (s : q = q') : p ⬝h* q = p' ⬝h* q' := - ap011 phconcat r s - - definition pvconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₁₂ f₁₄ f₀₃ f₂₃} - (r : p = p') (s : q = q') : p ⬝v* q = p' ⬝v* q' := - ap011 pvconcat r s - - definition phinverse2 {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} - (r : p = p') : p⁻¹ʰ* = p'⁻¹ʰ* := - ap phinverse r - - definition pvinverse2 {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} - (r : p = p') : p⁻¹ᵛ* = p'⁻¹ᵛ* := - ap pvinverse r - - definition phomotopy_hconcat2 {q q' : f₀₁' ~* f₀₁} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} - (r : q = q') (s : p = p') : q ⬝ph* p = q' ⬝ph* p' := - ap011 phomotopy_hconcat r s - - definition hconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₂₁' ~* f₂₁} - (r : p = p') (s : q = q') : p ⬝hp* q = p' ⬝hp* q' := - ap011 hconcat_phomotopy r s - - definition phomotopy_vconcat2 {q q' : f₁₀' ~* f₁₀} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} - (r : q = q') (s : p = p') : q ⬝pv* p = q' ⬝pv* p' := - ap011 phomotopy_vconcat r s - - definition vconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₁₂' ~* f₁₂} - (r : p = p') (s : q = q') : p ⬝vp* q = p' ⬝vp* q' := - ap011 vconcat_phomotopy r s - - -- for consistency, should there be a second star here? - infix ` ◾h* `:79 := phconcat2 - infix ` ◾v* `:79 := pvconcat2 - infixl ` ◾hp* `:79 := hconcat_phomotopy2 - infixr ` ◾ph* `:79 := phomotopy_hconcat2 - infixl ` ◾vp* `:79 := vconcat_phomotopy2 - infixr ` ◾pv* `:79 := phomotopy_vconcat2 - postfix `⁻²ʰ*`:(max+1) := phinverse2 - postfix `⁻²ᵛ*`:(max+1) := pvinverse2 - - end psquare - - /- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it - -/ - -- fapply phomotopy_mk_ppmap, - -- { intro f, exact pwhisker_right f p }, - -- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, - -- exact pcompose_pconst_phomotopy p } - - definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) : - ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) := - !phomotopy_rec_on_idp_refl -- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) := -- begin @@ -886,7 +38,7 @@ namespace pointed ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := - (loop_pmap_commute X Y)⁻¹ᵉ* + (loop_ppmap_commute X Y)⁻¹ᵉ* definition loop_phomotopy [constructor] {A B : Type*} (f : A →* B) : Type* := pointed.MK (f ~* f) phomotopy.rfl @@ -900,21 +52,10 @@ namespace pointed : loop_phomotopy f →* loop_phomotopy (g ∘* f) := pmap.mk (λq, pwhisker_left g q) !pwhisker_left_refl - definition ppcompose_left_loop_phomotopy_refl {A B C : Type*} (g : B →* C) (f : A →* B) - : ppcompose_left_loop_phomotopy g phomotopy.rfl ~* ppcompose_left_loop_phomotopy' g f := - phomotopy.mk (λq, !refl_symm ◾** idp ◾** idp ⬝ !refl_trans ◾** idp ⬝ !trans_refl) - begin - esimp, exact sorry - end - definition loop_ppmap_pequiv' [constructor] (A B : Type*) : Ω(ppmap A B) ≃* loop_phomotopy (pconst A B) := pequiv_of_equiv (pmap_eq_equiv _ _) idp - -- definition loop_ppmap (A B : Type*) : pointed.MK (pconst A B ~* pconst A B) phomotopy.rfl ≃* - -- pointed.MK (Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl) ⟨homotopy.rfl, idp⟩ := - -- pequiv_of_equiv !phomotopy.sigma_char _ - definition ppmap_loop_pequiv' [constructor] (A B : Type*) : loop_phomotopy (pconst A B) ≃* ppmap A (Ω B) := pequiv_of_equiv (!phomotopy.sigma_char ⬝e !pmap.sigma_char⁻¹ᵉ) idp @@ -943,9 +84,6 @@ namespace pointed induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀, apply psquare_of_phomotopy, exact sorry - -- fapply phomotopy.mk, - -- { esimp, esimp [pmap_eq_equiv], intro p, }, - -- { } end definition ppmap_loop_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : @@ -967,12 +105,12 @@ namespace pointed end definition loop_pmap_commute_natural_left {A A' : Type*} (X : Type*) (f : A' →* A) : - psquare (loop_pmap_commute A X) (loop_pmap_commute A' X) + psquare (loop_ppmap_commute A X) (loop_ppmap_commute A' X) (Ω→ (ppcompose_right f)) (ppcompose_right f) := sorry definition loop_pmap_commute_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : - psquare (loop_pmap_commute A X) (loop_pmap_commute A X') + psquare (loop_ppmap_commute A X) (loop_ppmap_commute A X') (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) := loop_ppmap_pequiv'_natural_right A f ⬝h* ppmap_loop_pequiv'_natural_right A f @@ -1004,76 +142,5 @@ namespace pointed -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q := -- sorry - variables {X X' Y Y' Z : Type*} - definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) := - pmap.mk ap1 (eq_of_phomotopy !ap1_pconst) - - definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) : - ap1_gen (const A b) idp idp p = idp := - ap1_gen_idp_left (const A b) p ⬝ ap_constant p b - - definition ap1_gen_compose_const_left - {A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) : - ap1_gen_compose (const B c) f idp idp idp idp p ⬝ - ap1_gen_const c (ap1_gen f idp idp p) = - ap1_gen_const c p := - begin induction p, reflexivity end - - definition ap1_gen_compose_const_right - {A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) : - ap1_gen_compose g (const A b) idp idp idp idp p ⬝ - ap (ap1_gen g idp idp) (ap1_gen_const b p) = - ap1_gen_const (g b) p := - begin induction p, reflexivity end - - definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) : - phsquare (ap1_pcompose (pconst B C) f) - (ap1_pconst A C) - (ap1_phomotopy (pconst_pcompose f)) - (pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, induction f with f f₀, - esimp at *, induction f₀, - refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, - fapply phomotopy_eq, - { exact ap1_gen_compose_const_left c₀ f }, - { reflexivity } - end - - definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) : - phsquare (ap1_pcompose g (pconst A B)) - (ap1_pconst A C) - (ap1_phomotopy (pcompose_pconst g)) - (pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀, - esimp at *, induction g₀, - refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, - fapply phomotopy_eq, - { exact ap1_gen_compose_const_right g b₀ }, - { reflexivity } - end - - definition pap1_natural_left [constructor] (f : X' →* X) : - psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) := - begin - fapply phomotopy_mk_ppmap, - { intro g, exact !ap1_pcompose⁻¹* }, - { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ - idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, - apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ } - end - - definition pap1_natural_right [constructor] (f : Y →* Y') : - psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) := - begin - fapply phomotopy_mk_ppmap, - { intro g, exact !ap1_pcompose⁻¹* }, - { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾ - idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, - apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ } - end end pointed