susp and other things
This commit is contained in:
Floris van Doorn
parent
b61fb7e685
commit
773e9f9a2e
6 changed files with 232 additions and 29 deletions
|
|
@ -363,7 +363,7 @@ namespace seq_colim
|
|||
(q : prep0 f n (Point (A 0)) = Point (A n))
|
||||
: loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
|
||||
(ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
|
||||
by rewrite [▸*, con_inv, +ap_con, ap_inv, +con.assoc]
|
||||
by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
|
||||
|
||||
definition succ_add_tr_rep {n : ℕ} (k : ℕ) (x : A n)
|
||||
: transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x :=
|
||||
|
|
|
|||
|
|
@ -49,8 +49,8 @@ definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
|
|||
begin
|
||||
fconstructor,
|
||||
{ intro p, esimp,
|
||||
refine ap1_gen_con_left p (respect_pt f) (respect_pt f)
|
||||
(respect_pt g) (respect_pt g) ⬝ _,
|
||||
refine ap1_gen_con_left (respect_pt f) (respect_pt f)
|
||||
(respect_pt g) (respect_pt g) p ⬝ _,
|
||||
refine !whisker_right_idp ◾ !whisker_left_idp2, },
|
||||
{ refine !con.assoc ⬝ _,
|
||||
refine _ ◾ idp ⬝ _, rotate 1,
|
||||
|
|
|
|||
|
|
@ -510,7 +510,7 @@ namespace smash
|
|||
idp
|
||||
(smash_functor_pconst_right_homotopy (λ a, f' (f a)) x)
|
||||
(ap (smash_functor' (pmap.mk f' (refl (f' (f a₀)))) (pmap.mk g (refl (g d₀))))
|
||||
(smash_functor_pconst_right_homotopy f x)) :=
|
||||
(smash_functor_pconst_right_homotopy f x)) :=
|
||||
begin
|
||||
induction x with a b a b,
|
||||
{ refine _ ⬝hp (functor_gluel'2 f' g (f a) (f a₀))⁻¹, exact hrfl },
|
||||
|
|
|
|||
|
|
@ -2,10 +2,10 @@
|
|||
-- in collaboration with Egbert, Stefano, Robin, Ulrik
|
||||
|
||||
/- the adjunction between the smash product and pointed maps -/
|
||||
import .smash
|
||||
import .smash .susp
|
||||
|
||||
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
|
||||
function red_susp unit sigma
|
||||
function red_susp unit sigma susp
|
||||
|
||||
|
||||
namespace smash
|
||||
|
|
@ -214,7 +214,7 @@ namespace smash
|
|||
refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹,
|
||||
refine _ ⬝ !trans_refl⁻¹,
|
||||
fapply phomotopy_eq,
|
||||
{ intro a, refine !elim_gluel'⁻¹ },
|
||||
{ intro a, esimp, refine !elim_gluel'⁻¹ },
|
||||
{ esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹,
|
||||
refine whisker_right _ !elim_gluel'_same⁻² ⬝ _ ⬝ !elim_gluer'_same⁻¹⁻²,
|
||||
apply inv_con_eq_of_eq_con, refine !idp_con ⬝ _, esimp,
|
||||
|
|
@ -392,7 +392,7 @@ namespace smash
|
|||
apply smash_pmap_counit_natural_right
|
||||
end
|
||||
|
||||
definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
|
||||
definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
|
||||
ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~*
|
||||
smash_adjoint_pmap_inv A B C' ∘* ppcompose_left (ppcompose_left f) :=
|
||||
smash_pelim_natural_right f
|
||||
|
|
@ -504,4 +504,29 @@ namespace smash
|
|||
rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
|
||||
end
|
||||
|
||||
/- Corollary 2: smashing with a suspension -/
|
||||
definition smash_psusp_elim_equiv (A B X : Type*) :
|
||||
ppmap (A ∧ psusp B) X ≃* ppmap (psusp (A ∧ B)) X :=
|
||||
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 (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
|
||||
... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X
|
||||
|
||||
definition loop_pmap_commute_natural_right (A : Type*) (f : X →* X') :
|
||||
psquare (loop_pmap_commute A X) (loop_pmap_commute A X')
|
||||
(Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
|
||||
sorry
|
||||
|
||||
|
||||
definition smash_psusp_elim_equiv_natural_right (A B : Type*) (f : X →* X') :
|
||||
psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A B X')
|
||||
(ppcompose_left f) (ppcompose_left f) :=
|
||||
smash_adjoint_pmap_natural_right f ⬝h*
|
||||
psusp_adjoint_loop_natural_right (ppcompose_left f) ⬝h*
|
||||
ppcompose_left_psquare (loop_pmap_commute_natural_right A f) ⬝h*
|
||||
(smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h*
|
||||
(psusp_adjoint_loop_natural_right f)⁻¹ʰ*
|
||||
|
||||
end smash
|
||||
|
|
|
|||
137
homotopy/susp.hlean
Normal file
137
homotopy/susp.hlean
Normal file
|
|
@ -0,0 +1,137 @@
|
|||
import ..pointed
|
||||
|
||||
open susp eq pointed function is_equiv
|
||||
variables {X X' Y Y' Z : Type*}
|
||||
|
||||
-- move
|
||||
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
|
||||
|
||||
namespace susp
|
||||
|
||||
definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : psusp X) :
|
||||
psusp_functor (pconst X Y) x = pt :=
|
||||
begin
|
||||
induction x,
|
||||
{ reflexivity },
|
||||
{ exact (merid pt)⁻¹ },
|
||||
{ apply eq_pathover, refine !elim_merid ⬝ph _ ⬝hp !ap_constant⁻¹, exact square_of_eq !con.right_inv⁻¹ }
|
||||
end
|
||||
|
||||
definition susp_functor_pconst [constructor] (X Y : Type*) : psusp_functor (pconst X Y) ~* pconst (psusp X) (psusp Y) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ exact susp_functor_pconst_homotopy },
|
||||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition psusp_pfunctor [constructor] (X Y : Type*) : ppmap X Y →* ppmap (psusp X) (psusp Y) :=
|
||||
pmap.mk psusp_functor (eq_of_phomotopy !susp_functor_pconst)
|
||||
|
||||
definition psusp_pelim [constructor] (X Y : Type*) : ppmap X (Ω Y) →* ppmap (psusp X) Y :=
|
||||
ppcompose_left (loop_psusp_counit Y) ∘* psusp_pfunctor X (Ω Y)
|
||||
|
||||
definition loop_psusp_pintro [constructor] (X Y : Type*) : ppmap (psusp X) Y →* ppmap X (Ω Y) :=
|
||||
ppcompose_right (loop_psusp_unit X) ∘* pap1 (psusp X) Y
|
||||
|
||||
definition loop_psusp_pintro_natural_left (f : X' →* X) :
|
||||
psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X' Y)
|
||||
(ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
|
||||
!pap1_natural_left ⬝h* ppcompose_right_psquare (loop_psusp_unit_natural f)⁻¹*
|
||||
|
||||
definition loop_psusp_pintro_natural_right (f : Y →* Y') :
|
||||
psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X Y')
|
||||
(ppcompose_left f) (ppcompose_left (Ω→ f)) :=
|
||||
!pap1_natural_right ⬝h* !ppcompose_left_ppcompose_right⁻¹*
|
||||
|
||||
definition is_equiv_loop_psusp_pintro [constructor] (X Y : Type*) :
|
||||
is_equiv (loop_psusp_pintro X Y) :=
|
||||
begin
|
||||
fapply adjointify,
|
||||
{ exact psusp_pelim X Y },
|
||||
{ intro g, apply eq_of_phomotopy, exact psusp_adjoint_loop_right_inv g },
|
||||
{ intro f, apply eq_of_phomotopy, exact psusp_adjoint_loop_left_inv f }
|
||||
end
|
||||
|
||||
definition psusp_adjoint_loop' [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) :=
|
||||
pequiv_of_pmap (loop_psusp_pintro X Y) (is_equiv_loop_psusp_pintro X Y)
|
||||
|
||||
definition psusp_adjoint_loop_natural_right (f : Y →* Y') :
|
||||
psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X Y')
|
||||
(ppcompose_left f) (ppcompose_left (Ω→ f)) :=
|
||||
loop_psusp_pintro_natural_right f
|
||||
|
||||
definition psusp_adjoint_loop_natural_left (f : X' →* X) :
|
||||
psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X' Y)
|
||||
(ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
|
||||
loop_psusp_pintro_natural_left f
|
||||
|
||||
end susp
|
||||
|
|
@ -10,6 +10,10 @@ open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group si
|
|||
|
||||
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,
|
||||
|
|
@ -31,16 +35,16 @@ namespace pointed
|
|||
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₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
|
||||
(r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') :
|
||||
ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') =
|
||||
whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') :=
|
||||
{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 idp r₀ r₀ r₁ r₁ =
|
||||
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
|
||||
|
||||
|
|
@ -406,6 +410,22 @@ namespace pointed
|
|||
{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
|
||||
|
|
@ -425,6 +445,17 @@ namespace pointed
|
|||
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
|
||||
|
|
@ -565,6 +596,25 @@ namespace pointed
|
|||
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
|
||||
|
|
@ -726,6 +776,11 @@ namespace pointed
|
|||
(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 :=
|
||||
|
|
@ -820,22 +875,8 @@ namespace pointed
|
|||
pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
|
||||
ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
|
||||
|
||||
definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
{ fapply equiv.MK: esimp,
|
||||
{ intro f, fapply pmap_eq,
|
||||
{ intro x, exact f x },
|
||||
{ exact (respect_pt f)⁻¹ }},
|
||||
{ intro p, fapply pmap.mk,
|
||||
{ intro x, exact ap010 pmap.to_fun p x },
|
||||
{ note z := apd respect_pt p,
|
||||
note z2 := square_of_pathover z,
|
||||
refine eq_of_hdeg_square z2 ⬝ !ap_constant }},
|
||||
{ intro p, exact sorry },
|
||||
{ intro p, exact sorry }},
|
||||
{ apply pmap_eq_idp}
|
||||
end
|
||||
definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
|
||||
(loop_pmap_commute X Y)⁻¹ᵉ*
|
||||
|
||||
/-
|
||||
Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine?
|
||||
|
|
|
|||
Loading…
Reference in a new issue