From be0d5977f6c9048231b138b9d10e144f23bab7cc Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 19 Aug 2018 13:52:20 +0200 Subject: [PATCH] move to lib and older things --- homotopy/EM.hlean | 12 + homotopy/pushout.hlean | 13 + homotopy/wedge.hlean | 162 ++++++- move_to_lib.hlean | 980 +++++++++-------------------------------- pointed.hlean | 26 ++ 5 files changed, 408 insertions(+), 785 deletions(-) diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 9349091..9b3cec4 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -326,6 +326,18 @@ namespace EM EMadd1_pequiv_succ_natural f n !isomorphism.refl !isomorphism.refl (π→g[n+2] f) proof λa, idp qed + definition EMadd1_pmap_equiv (n : ℕ) (X Y : Type*) [is_conn (n+1) X] [is_trunc (n+1+1) X] + [is_conn (n+1) Y] [is_trunc (n+1+1) Y] : (X →* Y) ≃ πag[n+2] X →g πag[n+2] Y := + begin + fapply equiv.MK, + { exact π→g[n+2] }, + { exact λφ, (EMadd1_pequiv_type Y n ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ* }, + { intro φ, apply homomorphism_eq, + refine homotopy_group_functor_compose (n+2) _ _ ⬝hty _, exact sorry }, -- easy but tedious + { intro f, apply eq_of_phomotopy, refine (phomotopy_pinv_right_of_phomotopy _)⁻¹*, + apply EMadd1_pequiv_type_natural } + end + /- The Eilenberg-MacLane space K(G,n) with the same homotopy group as X on level n. On paper this is written K(πₙ(X), n). The problem is that for * n = 0 the expression π₀(X) is a pointed set, and K(X,0) needs X to be a pointed set diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index 844b4e9..c8f1a05 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -700,6 +700,19 @@ end apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ } end + definition pcofiber_elim_unique {X Y Z : Type*} {f : X →* Y} + {g₁ g₂ : pcofiber f →* Z} (h : g₁ ∘* pcod f ~* g₂ ∘* pcod f) + (sq : Πx, square (h (f x)) (respect_pt g₁ ⬝ (respect_pt g₂)⁻¹) + (ap g₁ (cofiber.glue x)) (ap g₂ (cofiber.glue x))) : g₁ ~* g₂ := + begin + fapply phomotopy.mk, + { intro x, induction x with y x, + { exact h y }, + { exact respect_pt g₁ ⬝ (respect_pt g₂)⁻¹ }, + { apply eq_pathover, exact sq x }}, + { apply inv_con_cancel_right } + end + /- The maps Z^{C_f} --> Z^Y --> Z^X are exact at Z^Y. Here Y^X means pointed maps from X to Y and C_f is the cofiber of f. diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean index 2e30696..939a415 100644 --- a/homotopy/wedge.hlean +++ b/homotopy/wedge.hlean @@ -1,6 +1,6 @@ -- Authors: Floris van Doorn -import homotopy.wedge +import homotopy.wedge homotopy.cofiber ..move_to_lib .pushout open wedge pushout eq prod sum pointed equiv is_equiv unit lift bool option @@ -107,4 +107,164 @@ equiv.MK add_point_of_wedge_pbool wedge_pbool_of_add_point calc plift.{u v} (A ∨ B) ≃* A ∨ B : by exact !pequiv_plift⁻¹ᵉ* ... ≃* plift.{u v} A ∨ plift.{u v} B : by exact wedge_pequiv !pequiv_plift !pequiv_plift + protected definition pelim [constructor] {X Y Z : Type*} (f : X →* Z) (g : Y →* Z) : X ∨ Y →* Z := + pmap.mk (wedge.elim f g (respect_pt f ⬝ (respect_pt g)⁻¹)) (respect_pt f) + + definition wedge_pr1 [constructor] (X Y : Type*) : X ∨ Y →* X := wedge.pelim (pid X) (pconst Y X) + definition wedge_pr2 [constructor] (X Y : Type*) : X ∨ Y →* Y := wedge.pelim (pconst X Y) (pid Y) + + open fiber prod cofiber pi + +variables {X Y : Type*} +definition pcofiber_pprod_incl1_of_pfiber_wedge_pr2' [unfold 3] + (x : pfiber (wedge_pr2 X Y)) : pcofiber (pprod_incl1 (Ω Y) X) := +begin + induction x with x p, induction x with x y, + { exact cod _ (p, x) }, + { exact pt }, + { apply arrow_pathover_constant_right, intro p, apply cofiber.glue } +end + +--set_option pp.all true +/- + X : Type* has a nondegenerate basepoint iff + it has the homotopy extension property iff + Π(f : X → Y) (y : Y) (p : f pt = y), ∃(g : X → Y) (h : f ~ g) (q : y = g pt), h pt = p ⬝ q + (or Σ?) +-/ + +definition pfiber_wedge_pr2_of_pcofiber_pprod_incl1' [unfold 3] + (x : pcofiber (pprod_incl1 (Ω Y) X)) : pfiber (wedge_pr2 X Y) := +begin + induction x with v p, + { induction v with p x, exact fiber.mk (inl x) p }, + { exact fiber.mk (inr pt) idp }, + { esimp, apply fiber_eq (wedge.glue ⬝ ap inr p), symmetry, + refine !ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose'⁻¹ ⬝ !ap_id) ⬝ !idp_con } +end + +variables (X Y) +definition pcofiber_pprod_incl1_of_pfiber_wedge_pr2 [constructor] : + pfiber (wedge_pr2 X Y) →* pcofiber (pprod_incl1 (Ω Y) X) := +pmap.mk pcofiber_pprod_incl1_of_pfiber_wedge_pr2' (cofiber.glue idp) + +-- definition pfiber_wedge_pr2_of_pprod [constructor] : +-- Ω Y ×* X →* pfiber (wedge_pr2 X Y) := +-- begin +-- fapply pmap.mk, +-- { intro v, induction v with p x, exact fiber.mk (inl x) p }, +-- { reflexivity } +-- end + +definition pfiber_wedge_pr2_of_pcofiber_pprod_incl1 [constructor] : + pcofiber (pprod_incl1 (Ω Y) X) →* pfiber (wedge_pr2 X Y) := +pmap.mk pfiber_wedge_pr2_of_pcofiber_pprod_incl1' + begin refine (fiber_eq wedge.glue _)⁻¹, exact !wedge.elim_glue⁻¹ end +-- pcofiber.elim (pfiber_wedge_pr2_of_pprod X Y) +-- begin +-- fapply phomotopy.mk, +-- { intro p, apply fiber_eq (wedge.glue ⬝ ap inr p ⬝ wedge.glue⁻¹), symmetry, +-- refine !ap_con ⬝ (!ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose'⁻¹ ⬝ !ap_id)) ◾ +-- (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ _, exact idp_con p }, +-- { esimp, refine fiber_eq2 (con.right_inv wedge.glue) _ ⬝ !fiber_eq_eta⁻¹, +-- rewrite [idp_con, ↑fiber_eq_pr2, con2_idp, whisker_right_idp, whisker_right_idp], +-- -- refine _ ⬝ (eq_bot_of_square (transpose (ap_con_right_inv_sq +-- -- (wedge.elim (λx : X, Point Y) (@id Y) idp) wedge.glue)))⁻¹, +-- -- refine whisker_right _ !con_inv ⬝ _, +-- exact sorry +-- } +-- end + +--set_option pp.notation false +set_option pp.binder_types true +open sigma.ops +definition pfiber_wedge_pr2_pequiv_pcofiber_pprod_incl1 [constructor] : + pfiber (wedge_pr2 X Y) ≃* pcofiber (pprod_incl1 (Ω Y) X) := +pequiv.MK (pcofiber_pprod_incl1_of_pfiber_wedge_pr2 _ _) + (pfiber_wedge_pr2_of_pcofiber_pprod_incl1 _ _) + abstract begin + fapply phomotopy.mk, + { intro x, esimp, induction x with x p, induction x with x y, + { reflexivity }, + { refine (fiber_eq (ap inr p) _)⁻¹, refine !ap_id⁻¹ ⬝ !ap_compose' }, + { apply @pi_pathover_right' _ _ _ _ (λ(xp : Σ(x : X ∨ Y), pppi.to_fun (wedge_pr2 X Y) x = pt), + pfiber_wedge_pr2_of_pcofiber_pprod_incl1' + (pcofiber_pprod_incl1_of_pfiber_wedge_pr2' (mk xp.1 xp.2)) = mk xp.1 xp.2), + intro p, apply eq_pathover, exact sorry }}, + { symmetry, refine !cofiber.elim_glue ◾ idp ⬝ _, apply con_inv_eq_idp, + apply ap (fiber_eq wedge.glue), esimp, rewrite [idp_con], refine !whisker_right_idp⁻² } + end end + abstract begin + exact sorry + end end +-- apply eq_pathover_id_right, refine ap_compose pcofiber_pprod_incl1_of_pfiber_wedge_pr2 _ _ ⬝ ap02 _ !elim_glue ⬝ph _ +-- apply eq_pathover_id_right, refine ap_compose pfiber_wedge_pr2_of_pcofiber_pprod_incl1 _ _ ⬝ ap02 _ !elim_glue ⬝ph _ + +/- move -/ +definition ap1_idp {A B : Type*} (f : A →* B) : Ω→ f idp = idp := +respect_pt (Ω→ f) + +definition ap1_phomotopy_idp {A B : Type*} {f g : A →* B} (h : f ~* g) : + Ω⇒ h idp = !respect_pt ⬝ !respect_pt⁻¹ := +sorry + + +variables {A} {B : Type*} {f : A →* B} {g : B →* A} (h : f ∘* g ~* pid B) +include h +definition nar_of_noo' (p : Ω A) : Ω (pfiber f) ×* Ω B := +begin + refine (_, Ω→ f p), + have z : Ω A →* Ω A, from pmap.mk (λp, Ω→ (g ∘* f) p ⬝ p⁻¹) proof (respect_pt (Ω→ (g ∘* f))) qed, + refine fiber_eq ((Ω→ g ∘* Ω→ f) p ⬝ p⁻¹) (!idp_con⁻¹ ⬝ whisker_right (respect_pt f) _⁻¹), + induction B with B b₀, induction f with f f₀, esimp at * ⊢, induction f₀, + refine !idp_con⁻¹ ⬝ ap1_con (pmap_of_map f pt) _ _ ⬝ + ((ap1_pcompose (pmap_of_map f pt) g _)⁻¹ ⬝ Ω⇒ h _ ⬝ ap1_pid _) ◾ ap1_inv _ _ ⬝ !con.right_inv +end + +definition noo_of_nar' (x : Ω (pfiber f) ×* Ω B) : Ω A := +begin + induction x with p q, exact Ω→ (ppoint f) p ⬝ Ω→ g q +end + +variables (f g) +definition nar_of_noo [constructor] : + Ω A →* Ω (pfiber f) ×* Ω B := +begin + refine pmap.mk (nar_of_noo' h) (prod_eq _ (ap1_gen_idp f (respect_pt f))), + esimp [nar_of_noo'], + refine fiber_eq2 (ap (ap1_gen _ _ _) (ap1_gen_idp f _) ⬝ !ap1_gen_idp) _ ⬝ !fiber_eq_eta⁻¹, + induction B with B b₀, induction f with f f₀, esimp at * ⊢, induction f₀, esimp, + refine (!idp_con ⬝ !whisker_right_idp) ◾ !whisker_right_idp ⬝ _, esimp [fiber_eq_pr2], + apply inv_con_eq_idp, + refine ap (ap02 f) !idp_con ⬝ _, + esimp [ap1_con, ap1_gen_con, ap1_inv, ap1_gen_inv], + refine _ ⬝ whisker_left _ (!con2_idp ⬝ !whisker_right_idp ⬝ idp ◾ ap1_phomotopy_idp h)⁻¹ᵖ, + esimp, exact sorry +end + +definition noo_of_nar [constructor] : + Ω (pfiber f) ×* Ω B →* Ω A := +pmap.mk (noo_of_nar' h) (respect_pt (Ω→ (ppoint f)) ◾ respect_pt (Ω→ g)) + +definition noo_pequiv_nar [constructor] : + Ω A ≃* Ω (pfiber f) ×* Ω B := +pequiv.MK (nar_of_noo f g h) (noo_of_nar f g h) + abstract begin + exact sorry + end end + abstract begin + exact sorry + end end +-- apply eq_pathover_id_right, refine ap_compose nar_of_noo _ _ ⬝ ap02 _ !elim_glue ⬝ph _ +-- apply eq_pathover_id_right, refine ap_compose noo_of_nar _ _ ⬝ ap02 _ !elim_glue ⬝ph _ + + definition loop_pequiv_of_cross_section {A B : Type*} (f : A →* B) (g : B →* A) + (h : f ∘* g ~* pid B) : Ω A ≃* Ω (pfiber f) ×* Ω B := + + + + + + + end wedge diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 8b1b094..5e7e23f 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -5,617 +5,55 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_q open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group is_trunc function unit prod bool -attribute pType.sigma_char sigma_pi_equiv_pi_sigma sigma.coind_unc [constructor] -attribute ap1_gen [unfold 8 9 10] -attribute ap010 [unfold 7] -attribute tro_invo_tro [unfold 9] -- TODO: move - -- TODO: homotopy_of_eq and apd10 should be the same - -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?) universe variable u - -namespace algebra - -variables {A : Type} [add_ab_inf_group A] -definition add_sub_cancel_middle (a b : A) : a + (b - a) = b := -!add.comm ⬝ !sub_add_cancel - -end algebra +/- +eq_of_homotopy_eta > eq_of_homotopy_apd10 +pathover_of_tr_eq_idp > pathover_idp_of_eq +pathover_of_tr_eq_idp' > pathover_of_tr_eq_idp +homotopy_group_isomorphism_of_ptrunc_pequiv > ghomotopy_group_isomorphism_of_ptrunc_pequiv +equiv_pathover <> equiv_pathover2 +homotopy_group_functor_succ_phomotopy_in > homotopy_group_succ_in_natural +homotopy_group_succ_in_natural > homotopy_group_succ_in_natural_unpointed +le_step_left > le_of_succ_le +pmap.eta > pmap_eta +pType.sigma_char' > pType.sigma_char +cghomotopy_group to aghomotopy_group +-/ namespace eq - -- this should maybe replace whisker_left_idp and whisker_left_idp_con - definition whisker_left_idp_square {A : Type} {a a' : A} {p q : a = a'} (r : p = q) : - square (whisker_left idp r) r (idp_con p) (idp_con q) := - begin induction r, exact hrfl end + definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A} + {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : + transport C (ap g₁ p)⁻¹ (f (transport C p z)) = f z := + by induction p; reflexivity - definition ap_con_idp_left {A B : Type} (f : A → B) {a a' : A} (p : a = a') : - square (ap_con f idp p) idp (ap02 f (idp_con p)) (idp_con (ap f p)) := - begin induction p, exact ids end - - definition pathover_tr_pathover_idp_of_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} {p : a = a'} - (q : b =[p] b') : - pathover_tr p b ⬝o pathover_idp_of_eq (tr_eq_of_pathover q) = q := - begin induction q; reflexivity end - - -- rename pathover_of_tr_eq_idp - definition pathover_of_tr_eq_idp' {A : Type} {B : A → Type} {a a₂ : A} (p : a = a₂) (b : B a) : - pathover_of_tr_eq idp = pathover_tr p b := - by induction p; constructor - -definition homotopy.symm_symm {A : Type} {P : A → Type} {f g : Πx, P x} (H : f ~ g) : - H⁻¹ʰᵗʸ⁻¹ʰᵗʸ = H := -begin apply eq_of_homotopy, intro x, apply inv_inv end - - definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g') - (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) := - begin induction p, reflexivity end - - definition apd10_prepostcompose {A B : Type} {C : B → Type} {D : A → Type} - (f : A → B) (h : Πa, C (f a) → D a) {g g' : Πb, C b} - (p : g = g') (a : A) : - apd10 (ap (λg a, h a (g (f a))) p) a = ap (h a) (apd10 p (f a)) := - begin induction p, reflexivity end - - definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type} - {a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) ⦃a₂ : A⦄ (p : a₀ = a₂) : P p := - begin - induction p₀, induction p, exact H - end - - definition eq.rec_to2 {A : Type} {P : Π⦃a₀ a₁⦄, a₀ = a₁ → Type} - {a₀ a₀' a₁' : A} (p' : a₀' = a₁') (p₀ : a₀ = a₀') (H : P p') ⦃a₁ : A⦄ (p : a₀ = a₁) : P p := - begin - induction p₀, induction p', induction p, exact H - end - - definition eq.rec_right_inv {A : Type} (f : A ≃ A) {P : Π⦃a₀ a₁⦄, f a₀ = a₁ → Type} - (H : Πa, P (right_inv f a)) ⦃a₀ a₁ : A⦄ (p : f a₀ = a₁) : P p := - begin - revert a₀ p, refine equiv_rect f⁻¹ᵉ _ _, - intro a₀ p, exact eq.rec_to (right_inv f a₀) (H a₀) p, - end - - definition eq.rec_equiv {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type} - (H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p := - begin - assert qr : Σ(q : a₀ = a₁), ap f q = p, - { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, - cases qr with q r, apply transport P r, induction q, exact H - end - - definition eq.rec_equiv_symm {A B : Type} {a₁ : A} (f : A ≃ B) {P : Π{a₀}, f a₀ = f a₁ → Type} - (H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p := - begin - assert qr : Σ(q : a₀ = a₁), ap f q = p, - { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, - cases qr with q r, apply transport P r, induction q, exact H - end - - definition eq.rec_equiv_to_same {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type} - ⦃a₁' : A⦄ (p' : f a₀ = f a₁') (H : P p') ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p := - begin - revert a₁' p' H a₁ p, - refine eq.rec_equiv f _, - exact eq.rec_equiv f - end - - definition eq.rec_equiv_to {A A' B : Type} {a₀ : A} (f : A ≃ B) (g : A' ≃ B) - {P : Π{a₁}, f a₀ = g a₁ → Type} - ⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p := - begin - assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p, - { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p), - whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ }, - assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p', - { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'), - whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ }, - induction qr with q r, induction q'r' with q' r', - induction q, induction q', - induction r, induction r', - exact H - end - - definition eq.rec_grading {A A' B : Type} {a : A} (f : A ≃ B) (g : A' ≃ B) - {P : Π{b}, f a = b → Type} - {a' : A'} (p' : f a = g a') (H : P p') ⦃b : B⦄ (p : f a = b) : P p := - begin - revert b p, refine equiv_rect g _ _, - exact eq.rec_equiv_to f g p' H - end - - definition eq.rec_grading_unbased {A B B' C : Type} (f : A ≃ B) (g : B ≃ C) (h : B' ≃ C) - {P : Π{b c}, g b = c → Type} - {a' : A} {b' : B'} (p' : g (f a') = h b') (H : P p') ⦃b : B⦄ ⦃c : C⦄ (q : f a' = b) - (p : g b = c) : P p := - begin - induction q, exact eq.rec_grading (f ⬝e g) h p' H p - 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 - -- -- refine ptrunc_functor_phomotopy 0 !apn_pinv ⬝hty _, - -- -- intro x, esimp, - -- end - - -- definition natural_square_tr_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 - - lemma homotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*} - (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B := - (ghomotopy_group_ptrunc_of_le H A)⁻¹ᵍ ⬝g - homotopy_group_isomorphism_of_pequiv n f ⬝g - ghomotopy_group_ptrunc_of_le H B - -definition fundamental_group_isomorphism {X : Type*} {G : Group} - (e : Ω X ≃ G) (hom_e : Πp q, e (p ⬝ q) = e p * e q) : π₁ X ≃g G := -isomorphism_of_equiv (trunc_equiv_trunc 0 e ⬝e (trunc_equiv 0 G)) - begin intro p q, induction p with p, induction q with q, exact hom_e p q end - -definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a') - {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') - (r : to_fun f =[p] to_fun g) : f =[p] g := -begin - fapply pathover_of_fn_pathover_fn, - { intro a, apply equiv.sigma_char }, - { apply sigma_pathover _ _ _ r, apply is_prop.elimo } -end - -definition equiv_pathover_inv {A : Type} {a a' : A} (p : a = a') - {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') - (r : to_inv f =[p] to_inv g) : f =[p] g := -begin - /- this proof is a bit weird, but it works -/ - apply equiv_pathover2, - change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ, - apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ), - apply equiv_pathover2, - exact r -end - -definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A} - {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : - transport C (ap g₁ p)⁻¹ (f (transport C p z)) = f z := -by induction p; reflexivity - -definition transport_lemma2 {A : Type} {C : A → Type} {g₁ : A → A} - {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : - transport C (ap g₁ p) (f z) = f (transport C p z) := -by induction p; reflexivity - -definition eq_of_pathover_apo {A C : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} - {p : a = a'} (g : Πa, B a → C) (q : b =[p] b') : - eq_of_pathover (apo g q) = apd011 g p q := -by induction q; reflexivity - - definition apd02 [unfold 8] {A : Type} {B : A → Type} (f : Πa, B a) {a a' : A} {p q : a = a'} - (r : p = q) : change_path r (apd f p) = apd f q := - by induction r; reflexivity - - definition pathover_ap_cono {A A' : Type} {a₁ a₂ a₃ : A} - {p₁ : a₁ = a₂} {p₂ : a₂ = a₃} (B' : A' → Type) (f : A → A') - {b₁ : B' (f a₁)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)} - (q₁ : b₁ =[p₁] b₂) (q₂ : b₂ =[p₂] b₃) : - pathover_ap B' f (q₁ ⬝o q₂) = - change_path !ap_con⁻¹ (pathover_ap B' f q₁ ⬝o pathover_ap B' f q₂) := - by induction q₁; induction q₂; reflexivity - - definition concato_eq_eq {A : Type} {B : A → Type} {a₁ a₂ : A} {p₁ : a₁ = a₂} - {b₁ : B a₁} {b₂ b₂' : B a₂} (r : b₁ =[p₁] b₂) (q : b₂ = b₂') : - r ⬝op q = r ⬝o pathover_idp_of_eq q := - by induction q; reflexivity - -definition ap_apd0111 {A₁ A₂ A₃ : Type} {B : A₁ → Type} {C : Π⦃a⦄, B a → Type} {a a₂ : A₁} - {b : B a} {b₂ : B a₂} {c : C b} {c₂ : C b₂} - (g : A₂ → A₃) (f : Πa b, C b → A₂) (Ha : a = a₂) (Hb : b =[Ha] b₂) - (Hc : c =[apd011 C Ha Hb] c₂) : - ap g (apd0111 f Ha Hb Hc) = apd0111 (λa b c, (g (f a b c))) Ha Hb Hc := -by induction Hb; induction Hc using idp_rec_on; reflexivity - -section squareover - - variables {A A' : Type} {B : A → Type} - {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A} - /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ - {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} - /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ - {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} - /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = 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₄₃} - - {b : B a} - {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀} - {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂} - {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄} - /-b₀₀-/ {q₁₀ : b₀₀ =[p₁₀] b₂₀} /-b₂₀-/ {q₃₀ : b₂₀ =[p₃₀] b₄₀} /-b₄₀-/ - /-b₀₂-/ {q₁₂ : b₀₂ =[p₁₂] b₂₂} /-b₂₂-/ {q₃₂ : b₂₂ =[p₃₂] b₄₂} /-b₄₂-/ - /-b₀₄-/ {q₁₄ : b₀₄ =[p₁₄] b₂₄} /-b₂₄-/ {q₃₄ : b₂₄ =[p₃₄] b₄₄} /-b₄₄-/ - {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-t₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-t₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂} - {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-t₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-t₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄} - - definition move_right_of_top_over {p : a₀₀ = a} {p' : a = a₂₀} - {s : square p p₁₂ p₀₁ (p' ⬝ p₂₁)} {q : b₀₀ =[p] b} {q' : b =[p'] b₂₀} - (t : squareover B (move_top_of_right s) (q ⬝o q') q₁₂ q₀₁ q₂₁) : - squareover B s q q₁₂ q₀₁ (q' ⬝o q₂₁) := - begin induction q', induction q, induction q₂₁, exact t end - - /- TODO: replace the version in the library by this -/ - definition hconcato_pathover' {p : a₂₀ = a₂₂} {sp : p = p₂₁} {s : square p₁₀ p₁₂ p₀₁ p} - {q : b₂₀ =[p] b₂₂} (t₁₁ : squareover B (s ⬝hp sp) q₁₀ q₁₂ q₀₁ q₂₁) - (r : change_path sp q = q₂₁) : squareover B s q₁₀ q₁₂ q₀₁ q := - by induction sp; induction r; exact t₁₁ - - variables (s₁₁ q₀₁ q₁₀ q₂₁ q₁₂) - definition squareover_fill_t : Σ (q : b₀₀ =[p₁₀] b₂₀), squareover B s₁₁ q q₁₂ q₀₁ q₂₁ := - begin - induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on, - induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ - end - - definition squareover_fill_b : Σ (q : b₀₂ =[p₁₂] b₂₂), squareover B s₁₁ q₁₀ q q₀₁ q₂₁ := - begin - induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on, - induction q₁₀ using idp_rec_on, exact ⟨idpo, idso⟩ - end - - definition squareover_fill_l : Σ (q : b₀₀ =[p₀₁] b₀₂), squareover B s₁₁ q₁₀ q₁₂ q q₂₁ := - begin - induction s₁₁, induction q₁₀ using idp_rec_on, induction q₂₁ using idp_rec_on, - induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ - end - - definition squareover_fill_r : Σ (q : b₂₀ =[p₂₁] b₂₂) , squareover B s₁₁ q₁₀ q₁₂ q₀₁ q := - begin - induction s₁₁, induction q₀₁ using idp_rec_on, induction q₁₀ using idp_rec_on, - induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩ - end - - -end squareover - -/- move this to types.eq, and replace the proof there -/ - section - parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) - (c₀ : code a₀) - include H c₀ - protected definition encode2 {a : A} (q : a₀ = a) : code a := - transport code q c₀ - - protected definition decode2' {a : A} (c : code a) : a₀ = a := - have ⟨a₀, c₀⟩ = ⟨a, c⟩ :> Σa, code a, from !is_prop.elim, - this..1 - - protected definition decode2 {a : A} (c : code a) : a₀ = a := - (decode2' c₀)⁻¹ ⬝ decode2' c - - open sigma.ops - definition total_space_method2 (a : A) : (a₀ = a) ≃ code a := - begin - fapply equiv.MK, - { exact encode2 }, - { exact decode2 }, - { intro c, unfold [encode2, decode2, decode2'], - rewrite [is_prop_elim_self, ▸*, idp_con], - apply tr_eq_of_pathover, apply eq_pr2 }, - { intro q, induction q, esimp, apply con.left_inv, }, - end - end - -definition total_space_method2_refl {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) - (c₀ : code a₀) : total_space_method2 a₀ code H c₀ a₀ idp = c₀ := -begin - reflexivity -end - - 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 trunc_functor_hsquare (n : ℕ₋₂) (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : - hsquare (trunc_functor n f₁₀) (trunc_functor n f₁₂) - (trunc_functor n f₀₁) (trunc_functor n f₂₁) := - λa, !trunc_functor_compose⁻¹ ⬝ trunc_functor_homotopy n h a ⬝ !trunc_functor_compose - - attribute hhconcat hvconcat [unfold_full] - - definition rfl_hhconcat (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : homotopy.rfl ⬝htyh q ~ q := - homotopy.rfl - - definition hhconcat_rfl (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : q ⬝htyh homotopy.rfl ~ q := - λx, !idp_con ⬝ ap_id (q x) - - definition rfl_hvconcat (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : homotopy.rfl ⬝htyv q ~ q := - λx, !idp_con - - definition hvconcat_rfl (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : q ⬝htyv homotopy.rfl ~ q := - λx, !ap_id - - end hsquare - definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) : - hsquare (homotopy_group_succ_in A n) (homotopy_group_succ_in B n) (π→[n+1] f) (π→[n] (Ω→ f)) := - trunc_functor_hsquare _ (loopn_succ_in_natural n f)⁻¹* - - definition homotopy2.refl {A} {B : A → Type} {C : Π⦃a⦄, B a → Type} (f : Πa (b : B a), C b) : - f ~2 f := - λa b, idp - - definition homotopy2.rfl [refl] {A} {B : A → Type} {C : Π⦃a⦄, B a → Type} - {f : Πa (b : B a), C b} : f ~2 f := - λa b, idp - - definition homotopy3.refl {A} {B : A → Type} {C : Πa, B a → Type} - {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} (f : Πa b (c : C a b), D c) : f ~3 f := - λa b c, idp - - definition homotopy3.rfl {A} {B : A → Type} {C : Πa, B a → Type} - {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} {f : Πa b (c : C a b), D c} : f ~3 f := - λa b c, idp - - definition eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type} - {a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) : - eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp := - by induction q; reflexivity + definition transport_lemma2 {A : Type} {C : A → Type} {g₁ : A → A} + {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : + transport C (ap g₁ p) (f z) = f (transport C p z) := + by induction p; reflexivity end eq open eq namespace nat - protected definition rec_down (P : ℕ → Type) (s : ℕ) (H0 : P s) (Hs : Πn, P (n+1) → P n) : P 0 := - begin - induction s with s IH, - { exact H0 }, - { exact IH (Hs s H0) } - end - - definition rec_down_le (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) (Hs : Πn, P (n+1) → P n) - : Πn, P n := - begin - induction s with s IH: intro n, - { exact H0 n (zero_le n) }, - { apply IH, intro n' H, induction H with n' H IH2, apply Hs, exact H0 _ !le.refl, - exact H0 _ (succ_le_succ H) } - end - - definition rec_down_le_univ {P : ℕ → Type} {s : ℕ} {H0 : Π⦃n⦄, s ≤ n → P n} - {Hs : Π⦃n⦄, P (n+1) → P n} (Q : Π⦃n⦄, P n → P (n + 1) → Type) - (HQ0 : Πn (H : s ≤ n), Q (H0 H) (H0 (le.step H))) (HQs : Πn (p : P (n+1)), Q (Hs p) p) : - Πn, Q (rec_down_le P s H0 Hs n) (rec_down_le P s H0 Hs (n + 1)) := - begin - induction s with s IH: intro n, - { apply HQ0 }, - { apply IH, intro n' H, induction H with n' H IH2, - { esimp, apply HQs }, - { apply HQ0 }} - end - - definition rec_down_le_beta_ge (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) - (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : s ≤ n) : rec_down_le P s H0 Hs n = H0 n Hn := - begin - revert n Hn, induction s with s IH: intro n Hn, - { exact ap (H0 n) !is_prop.elim }, - { have Hn' : s ≤ n, from le.trans !self_le_succ Hn, - refine IH _ _ Hn' ⬝ _, - induction Hn' with n Hn' IH', - { exfalso, exact not_succ_le_self Hn }, - { exact ap (H0 (succ n)) !is_prop.elim }} - end - - definition rec_down_le_beta_lt (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) - (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : n < s) : - rec_down_le P s H0 Hs n = Hs n (rec_down_le P s H0 Hs (n+1)) := - begin - revert n Hn, induction s with s IH: intro n Hn, - { exfalso, exact not_succ_le_zero n Hn }, - { have Hn' : n ≤ s, from le_of_succ_le_succ Hn, - --esimp [rec_down_le], - exact sorry - -- induction Hn' with s Hn IH, - -- { }, - -- { } -} - end - - /- this generalizes iterate_commute -/ - definition iterate_hsquare {A B : Type} {f : A → A} {g : B → B} - (h : A → B) (p : hsquare f g h h) (n : ℕ) : hsquare (f^[n]) (g^[n]) h h := - begin - induction n with n q, - exact homotopy.rfl, - exact q ⬝htyh p - end - -definition iterate_equiv2 {A : Type} {C : A → Type} (f : A → A) (h : Πa, C a ≃ C (f a)) - (k : ℕ) (a : A) : C a ≃ C (f^[k] a) := -begin induction k with k IH, reflexivity, exact IH ⬝e h (f^[k] a) end - - - - /- replace proof of le_of_succ_le by this -/ - definition le_step_left {n m : ℕ} (H : succ n ≤ m) : n ≤ m := - by induction H with H m H'; exact le_succ n; exact le.step H' - - /- TODO: make proof of le_succ_of_le simpler -/ - - definition nat.add_le_add_left2 {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := - by induction H with m H H₂; reflexivity; exact le.step H₂ +-- definition rec_down_le_beta_lt (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) +-- (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : n < s) : +-- rec_down_le P s H0 Hs n = Hs n (rec_down_le P s H0 Hs (n+1)) := +-- begin +-- revert n Hn, induction s with s IH: intro n Hn, +-- { exfalso, exact not_succ_le_zero n Hn }, +-- { have Hn' : n ≤ s, from le_of_succ_le_succ Hn, +-- --esimp [rec_down_le], +-- exact sorry +-- -- induction Hn' with s Hn IH, +-- -- { }, +-- -- { } +-- } +-- end end nat - -namespace trunc_index - open is_conn nat trunc is_trunc - lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n := - by induction n with n p; reflexivity; exact ap succ p - - protected definition of_nat_monotone {n k : ℕ} : n ≤ k → of_nat n ≤ of_nat k := - begin - intro H, induction H with k H K, - { apply le.tr_refl }, - { apply le.step K } - end - - lemma add_plus_two_comm (n k : ℕ₋₂) : n +2+ k = k +2+ n := - begin - induction n with n IH, - { exact minus_two_add_plus_two k }, - { exact !succ_add_plus_two ⬝ ap succ IH} - end - - lemma sub_one_add_plus_two_sub_one (n m : ℕ) : n.-1 +2+ m.-1 = of_nat (n + m) := - begin - induction m with m IH, - { reflexivity }, - { exact ap succ IH } - end - -end trunc_index - -namespace int - - private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n := - le.intro ( - calc n + 1 + -[1+ k] + k - = n + 1 + (-(k + 1)) + k : by reflexivity - ... = n + 1 + (- 1 - k) + k : by krewrite (neg_add_rev k 1) - ... = n + 1 + (- 1 - k + k) : add.assoc - ... = n + 1 + (- 1 + -k + k) : by reflexivity - ... = n + 1 + (- 1 + (-k + k)) : add.assoc - ... = n + 1 + (- 1 + 0) : add.left_inv - ... = n + (1 + (- 1 + 0)) : add.assoc - ... = n : int.add_zero) - - private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k := - le.intro ( - calc -[1+ n] + 1 + k + n - = - (n + 1) + 1 + k + n : by reflexivity - ... = -n - 1 + 1 + k + n : by rewrite (neg_add n 1) - ... = -n + (- 1 + 1) + k + n : by krewrite (int.add_assoc (-n) (- 1) 1) - ... = -n + 0 + k + n : add.left_inv 1 - ... = -n + k + n : int.add_zero - ... = k + -n + n : int.add_comm - ... = k + (-n + n) : int.add_assoc - ... = k + 0 : add.left_inv n - ... = k : int.add_zero) - - open trunc_index - /- - The function from integers to truncation indices which sends - positive numbers to themselves, and negative numbers to negative - 2. In particular -1 is sent to -2, but since we only work with - pointed types, that doesn't matter for us -/ - definition maxm2 [unfold 1] : ℤ → ℕ₋₂ := - λ n, int.cases_on n trunc_index.of_nat (λk, -2) - - -- we also need the max -1 - function - definition maxm1 [unfold 1] : ℤ → ℕ₋₂ := - λ n, int.cases_on n trunc_index.of_nat (λk, -1) - - definition maxm2_le_maxm1 (n : ℤ) : maxm2 n ≤ maxm1 n := - begin - induction n with n n, - { exact le.tr_refl n }, - { exact minus_two_le -1 } - end - - -- the is maxm1 minus 1 - definition maxm1m1 [unfold 1] : ℤ → ℕ₋₂ := - λ n, int.cases_on n (λ k, k.-1) (λ k, -2) - - definition maxm1_eq_succ (n : ℤ) : maxm1 n = (maxm1m1 n).+1 := - begin - induction n with n n, - { reflexivity }, - { reflexivity } - end - - definition maxm2_le_maxm0 (n : ℤ) : maxm2 n ≤ max0 n := - begin - induction n with n n, - { exact le.tr_refl n }, - { exact minus_two_le 0 } - end - - definition max0_le_of_le {n : ℤ} {m : ℕ} (H : n ≤ of_nat m) - : nat.le (max0 n) m := - begin - induction n with n n, - { exact le_of_of_nat_le_of_nat H }, - { exact nat.zero_le m } - end - - definition not_neg_succ_le_of_nat {n m : ℕ} : ¬m ≤ -[1+n] := - by cases m: exact id - - definition maxm2_monotone {n m : ℤ} (H : n ≤ m) : maxm2 n ≤ maxm2 m := - begin - induction n with n n, - { induction m with m m, - { apply of_nat_le_of_nat, exact le_of_of_nat_le_of_nat H }, - { exfalso, exact not_neg_succ_le_of_nat H }}, - { apply minus_two_le } - end - - definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n := - le.intro !sub_add_cancel - - definition sub_nat_lt (n : ℤ) (m : ℕ) : n - m < n + 1 := - add_le_add_right (sub_nat_le n m) 1 - - definition sub_one_le (n : ℤ) : n - 1 ≤ n := - sub_nat_le n 1 - - definition le_add_nat (n : ℤ) (m : ℕ) : n ≤ n + m := - le.intro rfl - - definition le_add_one (n : ℤ) : n ≤ n + 1:= - le_add_nat n 1 - - open trunc_index - - definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) := - begin - rewrite [-(maxm1_eq_succ n)], - induction n with n n, - { induction k with k k, - { induction k with k IH, - { apply le.tr_refl }, - { exact succ_le_succ IH } }, - { exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₁) - (maxm2_le_maxm1 n) } }, - { krewrite (add_plus_two_comm -1 (maxm1m1 k)), - rewrite [-(maxm1_eq_succ k)], - exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₂) - (maxm2_le_maxm1 k) } - end - -end int open int - -namespace pmap - - /- rename: pmap_eta in namespace pointed -/ - definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f := - begin induction f, reflexivity end - -end pmap - -namespace lift - - definition is_trunc_plift [instance] [priority 1450] (A : Type*) (n : ℕ₋₂) - [H : is_trunc n A] : is_trunc n (plift A) := - is_trunc_lift A n - - definition lift_functor2 {A B C : Type} (f : A → B → C) (x : lift A) (y : lift B) : lift C := - up (f (down x) (down y)) - -end lift - -- definition ppi_eq_equiv_internal : (k = l) ≃ (k ~* l) := -- calc (k = l) ≃ ppi.sigma_char P p₀ k = ppi.sigma_char P p₀ l -- : eq_equiv_fn_eq (ppi.sigma_char P p₀) k l @@ -639,211 +77,101 @@ end lift namespace pointed /- move to pointed -/ open sigma.ops -definition pType.sigma_char' [constructor] : pType.{u} ≃ Σ(X : Type.{u}), X := -begin - fapply equiv.MK, - { intro X, exact ⟨X, pt⟩ }, - { intro X, exact pointed.MK X.1 X.2 }, - { intro x, induction x with X x, reflexivity }, - { intro x, induction x with X x, reflexivity }, -end -definition ap_equiv_eq {X Y : Type} {e e' : X ≃ Y} (p : e ~ e') (x : X) : - ap (λ(e : X ≃ Y), e x) (equiv_eq p) = p x := -begin - cases e with e He, cases e' with e' He', esimp at *, esimp [equiv_eq], - refine homotopy.rec_on' p _, intro q, induction q, esimp [equiv_eq', equiv_mk_eq], - assert H : He = He', apply is_prop.elim, induction H, rewrite [is_prop_elimo_self] -end - -definition pequiv.sigma_char_equiv [constructor] (X Y : Type*) : - (X ≃* Y) ≃ Σ(e : X ≃ Y), e pt = pt := -begin - fapply equiv.MK, - { intro e, exact ⟨equiv_of_pequiv e, respect_pt e⟩ }, - { intro e, exact pequiv_of_equiv e.1 e.2 }, - { intro e, induction e with e p, fapply sigma_eq, - apply equiv_eq, reflexivity, esimp, - apply eq_pathover_constant_right, esimp, - refine _ ⬝ph vrfl, - apply ap_equiv_eq }, - { intro e, apply pequiv_eq, fapply phomotopy.mk, intro x, reflexivity, - refine !idp_con ⬝ _, reflexivity }, -end - -definition pequiv.sigma_char_pmap [constructor] (X Y : Type*) : - (X ≃* Y) ≃ Σ(f : X →* Y), is_equiv f := -begin - fapply equiv.MK, - { intro e, exact ⟨ pequiv.to_pmap e , pequiv.to_is_equiv e ⟩ }, - { intro w, exact pequiv_of_pmap w.1 w.2 }, - { intro w, induction w with f p, fapply sigma_eq, - { reflexivity }, { apply is_prop.elimo } }, - { intro e, apply pequiv_eq, fapply phomotopy.mk, - { intro x, reflexivity }, - { refine !idp_con ⬝ _, reflexivity } } -end - -definition pType_eq_equiv (X Y : Type*) : (X = Y) ≃ (X ≃* Y) := -begin - refine eq_equiv_fn_eq pType.sigma_char' X Y ⬝e !sigma_eq_equiv ⬝e _, esimp, - transitivity Σ(p : X = Y), cast p pt = pt, - apply sigma_equiv_sigma_right, intro p, apply pathover_equiv_tr_eq, - transitivity Σ(e : X ≃ Y), e pt = pt, - refine sigma_equiv_sigma (eq_equiv_equiv X Y) (λp, equiv.rfl), - exact (pequiv.sigma_char_equiv X Y)⁻¹ᵉ -end end pointed open pointed namespace trunc open trunc_index sigma.ops -definition ptrunctype.sigma_char [constructor] (n : ℕ₋₂) : - n-Type* ≃ Σ(X : Type*), is_trunc n X := -equiv.MK (λX, ⟨ptrunctype.to_pType X, _⟩) - (λX, ptrunctype.mk (carrier X.1) X.2 pt) - begin intro X, induction X with X HX, induction X, reflexivity end - begin intro X, induction X, reflexivity end + -- TODO: redefine loopn_ptrunc_pequiv + definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) : + Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~* + (loopn_ptrunc_pequiv n k B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→[k] f) := + begin + revert n, induction k with k IH: intro n, + { reflexivity }, + { exact sorry } + end -definition is_embedding_ptrunctype_to_pType (n : ℕ₋₂) : is_embedding (@ptrunctype.to_pType n) := -begin - intro X Y, fapply is_equiv_of_equiv_of_homotopy, - { exact eq_equiv_fn_eq (ptrunctype.sigma_char n) _ _ ⬝e subtype_eq_equiv _ _ }, - intro p, induction p, reflexivity -end + definition ptrunctype.sigma_char [constructor] (n : ℕ₋₂) : + n-Type* ≃ Σ(X : Type*), is_trunc n X := + equiv.MK (λX, ⟨ptrunctype.to_pType X, _⟩) + (λX, ptrunctype.mk (carrier X.1) X.2 pt) + begin intro X, induction X with X HX, induction X, reflexivity end + begin intro X, induction X, reflexivity end -definition ptrunctype_eq_equiv {n : ℕ₋₂} (X Y : n-Type*) : (X = Y) ≃ (X ≃* Y) := -equiv.mk _ (is_embedding_ptrunctype_to_pType n X Y) ⬝e pType_eq_equiv X Y + definition is_embedding_ptrunctype_to_pType (n : ℕ₋₂) : is_embedding (@ptrunctype.to_pType n) := + begin + intro X Y, fapply is_equiv_of_equiv_of_homotopy, + { exact eq_equiv_fn_eq (ptrunctype.sigma_char n) _ _ ⬝e subtype_eq_equiv _ _ }, + intro p, induction p, reflexivity + end -/- replace trunc_trunc_equiv_left by this -/ -definition trunc_trunc_equiv_left' [constructor] (A : Type) {n m : ℕ₋₂} (H : n ≤ m) - : trunc n (trunc m A) ≃ trunc n A := -begin - note H2 := is_trunc_of_le (trunc n A) H, - fapply equiv.MK, - { intro x, induction x with x, induction x with x, exact tr x }, - { exact trunc_functor n tr }, - { intro x, induction x with x, reflexivity}, - { intro x, induction x with x, induction x with x, reflexivity} -end + definition ptrunctype_eq_equiv {n : ℕ₋₂} (X Y : n-Type*) : (X = Y) ≃ (X ≃* Y) := + equiv.mk _ (is_embedding_ptrunctype_to_pType n X Y) ⬝e pType_eq_equiv X Y -definition is_equiv_ptrunc_functor_ptr [constructor] (A : Type*) {n m : ℕ₋₂} (H : n ≤ m) - : is_equiv (ptrunc_functor n (ptr m A)) := -to_is_equiv (trunc_trunc_equiv_left' A H)⁻¹ᵉ + definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q := + tua (equiv_of_is_prop (iff.mp H) (iff.mpr H)) -definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q := -tua (equiv_of_is_prop (iff.mp H) (iff.mpr H)) + definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*) + (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) := + is_trunc_trunc_of_is_trunc A n m -definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ := -equiv.MK add_two sub_two add_two_sub_two sub_two_add_two + definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*} + (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A := + have is_trunc m A, from is_trunc_of_le A H1, + have is_trunc k A, from is_trunc_of_le A H2, + pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A)) + abstract begin + refine !ptrunc_elim_pcompose⁻¹* ⬝* _, + exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, + end end + abstract begin + refine !ptrunc_elim_pcompose⁻¹* ⬝* _, + exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, + end end -definition is_set_trunc_index [instance] : is_set ℕ₋₂ := -is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat + definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*) + : ptrunc k X ≃* ptrunc l X := + pequiv_ap (λ n, ptrunc n X) p -definition is_contr_ptrunc_minus_one (A : Type*) : is_contr (ptrunc -1 A) := -is_contr_of_inhabited_prop pt + definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*) + : ptrunc k X →* ptrunc l X := + have is_trunc k (ptrunc l X), from is_trunc_of_le _ p, + ptrunc.elim _ (ptr l X) --- TODO: redefine loopn_ptrunc_pequiv -definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) : - Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~* - (loopn_ptrunc_pequiv n k B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→[k] f) := -begin - revert n, induction k with k IH: intro n, - { reflexivity }, - { exact sorry } -end + definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ := + begin cases n with n, exact -2, exact n end -definition ptrunc_pequiv_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc n A] - [is_trunc n B] : f ∘* ptrunc_pequiv n A ~* ptrunc_pequiv n B ∘* ptrunc_functor n f := -begin - fapply phomotopy.mk, - { intro a, induction a with a, reflexivity }, - { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_compose'⁻¹ ⬝ _, apply ap_id } -end + /- A more general version of ptrunc_elim_phomotopy, where the proofs of truncatedness might be different -/ + definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B) + (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g := + begin + fapply phomotopy.mk, + { intro x, induction x with a, exact p a }, + { exact to_homotopy_pt p } + end -definition ptr_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) : - ptrunc_functor n f ∘* ptr n A ~* ptr n B ∘* f := -begin - fapply phomotopy.mk, - { intro a, reflexivity }, - { reflexivity } -end + definition pmap_ptrunc_equiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : + (ptrunc n A →* B) ≃ (A →* B) := + begin + fapply equiv.MK, + { intro g, exact g ∘* ptr n A }, + { exact ptrunc.elim n }, + { intro f, apply eq_of_phomotopy, apply ptrunc_elim_ptr }, + { intro g, apply eq_of_phomotopy, + exact ptrunc_elim_pcompose n g (ptr n A) ⬝* pwhisker_left g (ptrunc_elim_ptr_phomotopy_pid n A) ⬝* + pcompose_pid g } + end -definition ptrunc_elim_pcompose (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) [is_trunc n B] - [is_trunc n C] : ptrunc.elim n (g ∘* f) ~* g ∘* ptrunc.elim n f := -begin - fapply phomotopy.mk, - { intro a, induction a with a, reflexivity }, - { apply idp_con } -end + definition pmap_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : + ppmap (ptrunc n A) B ≃* ppmap A B := + pequiv_of_equiv (pmap_ptrunc_equiv n A B) (eq_of_phomotopy (pconst_pcompose (ptr n A))) -definition ptrunc_elim_ptr_phomotopy_pid (n : ℕ₋₂) (A : Type*): - ptrunc.elim n (ptr n A) ~* pid (ptrunc n A) := -begin - fapply phomotopy.mk, - { intro a, induction a with a, reflexivity }, - { apply idp_con } -end - -definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*) - (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) := -is_trunc_trunc_of_is_trunc A n m - -definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*} - (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A := -have is_trunc m A, from is_trunc_of_le A H1, -have is_trunc k A, from is_trunc_of_le A H2, -pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A)) - abstract begin - refine !ptrunc_elim_pcompose⁻¹* ⬝* _, - exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, - end end - abstract begin - refine !ptrunc_elim_pcompose⁻¹* ⬝* _, - exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, - end end - -definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*) - : ptrunc k X ≃* ptrunc l X := -pequiv_ap (λ n, ptrunc n X) p - -definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*) - : ptrunc k X →* ptrunc l X := -have is_trunc k (ptrunc l X), from is_trunc_of_le _ p, -ptrunc.elim _ (ptr l X) - -definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ := -begin cases n with n, exact -2, exact n end - -/- A more general version of ptrunc_elim_phomotopy, where the proofs of truncatedness might be different -/ -definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B) - (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g := -begin - fapply phomotopy.mk, - { intro x, induction x with a, exact p a }, - { exact to_homotopy_pt p } -end - -definition pmap_ptrunc_equiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : - (ptrunc n A →* B) ≃ (A →* B) := -begin - fapply equiv.MK, - { intro g, exact g ∘* ptr n A }, - { exact ptrunc.elim n }, - { intro f, apply eq_of_phomotopy, apply ptrunc_elim_ptr }, - { intro g, apply eq_of_phomotopy, - exact ptrunc_elim_pcompose n g (ptr n A) ⬝* pwhisker_left g (ptrunc_elim_ptr_phomotopy_pid n A) ⬝* - pcompose_pid g } -end - -definition pmap_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : - ppmap (ptrunc n A) B ≃* ppmap A B := -pequiv_of_equiv (pmap_ptrunc_equiv n A B) (eq_of_phomotopy (pconst_pcompose (ptr n A))) - -definition loopn_ptrunc_pequiv_nat (n : ℕ) (k : ℕ) (A : Type*) : - Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) := -loopn_pequiv_loopn k (ptrunc_change_index (of_nat_add_of_nat n k)⁻¹ A) ⬝e* loopn_ptrunc_pequiv n k A + definition loopn_ptrunc_pequiv_nat (n : ℕ) (k : ℕ) (A : Type*) : + Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) := + loopn_pequiv_loopn k (ptrunc_change_index (of_nat_add_of_nat n k)⁻¹ A) ⬝e* loopn_ptrunc_pequiv n k A end trunc open trunc @@ -886,6 +214,45 @@ namespace is_trunc (H2 : is_conn (m.-1) A) : is_trunc m A := is_trunc_of_is_trunc_loopn m 0 A H H2 + definition is_trunc_of_trivial_homotopy {n : ℕ} {m : ℕ₋₂} {A : Type} (H : is_trunc m A) + (H2 : Πk a, k > n → is_contr (π[k] (pointed.MK A a))) : is_trunc n A := + begin + fapply is_trunc_is_equiv_closed_rev, { exact @tr n A }, + apply whitehead_principle m, + { apply is_equiv_trunc_functor_of_is_conn_fun, + note z := is_conn_fun_tr n A, + apply is_conn_fun_of_le _ (of_nat_le_of_nat (zero_le n)), }, + intro a k, + apply @nat.lt_ge_by_cases n (k+1), + { intro H3, apply @is_equiv_of_is_contr, exact H2 _ _ H3, + refine @trivial_homotopy_group_of_is_trunc _ _ _ _ H3, apply is_trunc_trunc }, + { intro H3, apply @(is_equiv_π_of_is_connected _ H3), apply is_conn_fun_tr } + end + + definition is_trunc_of_trivial_homotopy_pointed {n : ℕ} {m : ℕ₋₂} {A : Type*} (H : is_trunc m A) + (Hconn : is_conn 0 A) (H2 : Πk, k > n → is_contr (π[k] A)) : is_trunc n A := + begin + apply is_trunc_of_trivial_homotopy H, + intro k a H3, revert a, apply is_conn.elim -1, + cases A with A a₀, exact H2 k H3 + end + + definition is_trunc_of_is_trunc_succ {n : ℕ} {A : Type} (H : is_trunc (n.+1) A) + (H2 : Πa, is_contr (π[n+1] (pointed.MK A a))) : is_trunc n A := + begin + apply is_trunc_of_trivial_homotopy H, + intro k a H3, induction H3 with k H3 IH, exact H2 a, + apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3 + end + + definition is_trunc_of_is_trunc_succ_pointed {n : ℕ} {A : Type*} (H : is_trunc (n.+1) A) + (Hconn : is_conn 0 A) (H2 : is_contr (π[n+1] A)) : is_trunc n A := + begin + apply is_trunc_of_trivial_homotopy_pointed H Hconn, + intro k H3, induction H3 with k H3 IH, exact H2, + apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3 + end + end is_trunc namespace sigma open sigma.ops @@ -1383,11 +750,30 @@ begin induction p2, induction p1, induction r₃, reflexivity end -definition fiber_eq_equiv' [constructor] {A B : Type} {f : A → B} {b : B} (x y : fiber f b) - : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) := +definition fiber_eq_equiv' [constructor] {A B : Type} {f : A → B} {b : B} (x y : fiber f b) : + (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) := @equiv_change_inv _ _ (fiber_eq_equiv x y) (λpq, fiber_eq pq.1 pq.2) begin intro pq, cases pq, reflexivity end +definition fiber_eq2_equiv {A B : Type} {f : A → B} {b : B} {x y : fiber f b} + (p₁ p₂ : point x = point y) (q₁ : point_eq x = ap f p₁ ⬝ point_eq y) + (q₂ : point_eq x = ap f p₂ ⬝ point_eq y) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) ≃ + (Σ(r : p₁ = p₂), q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) := +begin + refine (eq_equiv_fn_eq_of_equiv (fiber_eq_equiv' x y)⁻¹ᵉ _ _)⁻¹ᵉ ⬝e sigma_eq_equiv _ _ ⬝e _, + apply sigma_equiv_sigma_right, esimp, intro r, + refine !eq_pathover_equiv_square ⬝e _, + refine eq_hconcat_equiv !ap_constant ⬝e hconcat_eq_equiv (ap_compose (λx, x ⬝ _) _ _) ⬝e _, + refine !square_equiv_eq ⬝e _, + exact eq_equiv_eq_closed idp (idp_con q₂) +end + +definition fiber_eq2 {A B : Type} {f : A → B} {b : B} {x y : fiber f b} + {p₁ p₂ : point x = point y} {q₁ : point_eq x = ap f p₁ ⬝ point_eq y} + {q₂ : point_eq x = ap f p₂ ⬝ point_eq y} (r : p₁ = p₂) + (s : q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) := +(fiber_eq2_equiv p₁ p₂ q₁ q₂)⁻¹ᵉ ⟨r, s⟩ + definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) := is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end @@ -1522,6 +908,18 @@ namespace function exact sorry end + definition is_embedding_of_square {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C) + (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hf : is_embedding f) : is_embedding g := + begin + apply is_embedding_homotopy_closed, exact inv_homotopy_of_homotopy_pre _ _ _ s, + apply is_embedding_compose, apply is_embedding_compose, + apply is_embedding_of_is_equiv, exact Hf, apply is_embedding_of_is_equiv + end + + definition is_embedding_of_square_rev {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C) + (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hg : is_embedding g) : is_embedding f := + is_embedding_of_square h⁻¹ᵉ k⁻¹ᵉ s⁻¹ʰᵗʸᵛ Hg + end function open function namespace is_conn @@ -1970,6 +1368,9 @@ namespace prod infix ` ×→ `:63 := prod_functor infix ` ×≃ `:63 := prod_equiv_prod + definition pprod_incl1 [constructor] (X Y : Type*) : X →* X ×* Y := pmap.mk (λx, (x, pt)) idp + definition pprod_incl2 [constructor] (X Y : Type*) : Y →* X ×* Y := pmap.mk (λy, (pt, y)) idp + end prod namespace equiv @@ -2118,6 +1519,17 @@ end end list +namespace chain_complex + +open fin +definition LES_is_contr_of_is_embedding_of_is_surjective (n : ℕ) {X Y : pType.{u}} (f : X →* Y) + (H : is_embedding (π→[n] f)) (H2 : is_surjective (π→[n+1] f)) : is_contr (π[n] (pfiber f)) := +begin + rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ (LES_of_homotopy_groups f) (n, 0) + (is_exact_LES_of_homotopy_groups f _) proof H qed proof H2 qed +end + +end chain_complex namespace susp open trunc_index diff --git a/pointed.hlean b/pointed.hlean index fd5b27f..a0b9d2b 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -606,5 +606,31 @@ definition ap1_gen_idp_eq {A B : Type} (f : A → B) {a : A} (q : f a = f a) (r ap1_gen_idp f q = ap (λx, ap1_gen f x x idp) r := begin cases r, reflexivity end +definition pointed_change_point [constructor] (A : Type*) {a : A} (p : a = pt) : + pointed.MK A a ≃* A := +pequiv_of_eq_pt p ⬝e* (pointed_eta_pequiv A)⁻¹ᵉ* + +definition change_path_psquare {A B : Type*} (f : A →* B) + {a' : A} {b' : B} (p : a' = pt) (q : pt = b') : + psquare (pointed_change_point _ p) + (pointed_change_point _ q⁻¹) + (pmap.mk f (ap f p ⬝ respect_pt f ⬝ q)) f := +begin + fapply phomotopy.mk, exact homotopy.rfl, + exact !idp_con ⬝ !ap_id ◾ !ap_id ⬝ !con_inv_cancel_right ⬝ whisker_right _ (ap02 f !ap_id⁻¹) +end + +definition change_path_psquare_cod {A B : Type*} (f : A →* B) {b' : B} (p : pt = b') : + f ~* pointed_change_point _ p⁻¹ ∘* pmap.mk f (respect_pt f ⬝ p) := +begin + fapply phomotopy.mk, exact homotopy.rfl, exact !idp_con ⬝ !ap_id ◾ !ap_id ⬝ !con_inv_cancel_right +end + +definition change_path_psquare_cod' {A B : Type} (f : A → B) (a : A) {b' : B} (p : f a = b') : + pointed_change_point _ p ∘* pmap_of_map f a ~* pmap.mk f p := +begin + fapply phomotopy.mk, exact homotopy.rfl, refine whisker_left idp (ap_id p)⁻¹ +end + end pointed