fix(hott): fix cofiber.elim and redefine cofiber as the symmetric pushout
This commit is contained in:
Floris van Doorn
parent
5eafb1f6b2
commit
7430d2c73b
1 changed files with 51 additions and 39 deletions
|
|
@ -9,60 +9,51 @@ import hit.pushout function .susp types.unit
|
|||
|
||||
open eq pushout unit pointed is_trunc is_equiv susp unit equiv
|
||||
|
||||
definition cofiber {A B : Type} (f : A → B) := pushout (λ (a : A), ⋆) f
|
||||
definition cofiber {A B : Type} (f : A → B) := pushout f (λ (a : A), ⋆)
|
||||
|
||||
namespace cofiber
|
||||
section
|
||||
parameters {A B : Type} (f : A → B)
|
||||
|
||||
protected definition base : cofiber f := inl ⋆
|
||||
|
||||
protected definition cod : B → cofiber f := inr
|
||||
definition cod : B → cofiber f := inl
|
||||
definition base : cofiber f := inr ⋆
|
||||
|
||||
parameter {f}
|
||||
protected definition glue (a : A) : cofiber.base f = cofiber.cod f (f a) :=
|
||||
protected definition glue (a : A) : cofiber.cod f (f a) = cofiber.base f :=
|
||||
pushout.glue a
|
||||
|
||||
parameter (f)
|
||||
protected definition contr_of_equiv [H : is_equiv f] : is_contr (cofiber f) :=
|
||||
begin
|
||||
fapply is_contr.mk, exact base,
|
||||
intro a, induction a with [u, b],
|
||||
{ cases u, reflexivity },
|
||||
{ exact !glue ⬝ ap inr (right_inv f b) },
|
||||
{ apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _,
|
||||
apply move_bot_of_left, refine !idp_con ⬝ph _, apply transpose, esimp,
|
||||
refine _ ⬝hp (ap (ap inr) !adj⁻¹), refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap },
|
||||
end
|
||||
|
||||
parameter {f}
|
||||
protected definition rec {P : cofiber f → Type}
|
||||
(Pbase : P base) (Pcod : Π (b : B), P (cod b))
|
||||
(Pglue : Π (a : A), pathover P Pbase (glue a) (Pcod (f a))) :
|
||||
protected definition rec {P : cofiber f → Type} (Pcod : Π (b : B), P (cod b)) (Pbase : P base)
|
||||
(Pglue : Π (a : A), pathover P (Pcod (f a)) (glue a) Pbase) :
|
||||
(Π y, P y) :=
|
||||
begin
|
||||
intro y, induction y, induction x, exact Pbase, exact Pcod x, esimp, exact Pglue x,
|
||||
intro y, induction y, exact Pcod x, induction x, exact Pbase, exact Pglue x
|
||||
end
|
||||
|
||||
protected definition rec_on {P : cofiber f → Type} (y : cofiber f)
|
||||
(Pbase : P base) (Pcod : Π (b : B), P (cod b))
|
||||
(Pglue : Π (a : A), pathover P Pbase (glue a) (Pcod (f a))) : P y :=
|
||||
cofiber.rec Pbase Pcod Pglue y
|
||||
(Pcod : Π (b : B), P (cod b)) (Pbase : P base)
|
||||
(Pglue : Π (a : A), pathover P (Pcod (f a)) (glue a) Pbase) : P y :=
|
||||
cofiber.rec Pcod Pbase Pglue y
|
||||
|
||||
protected definition elim {P : Type} (Pbase : P) (Pcod : B → P)
|
||||
(Pglue : Π (x : A), Pbase = Pcod (f x)) (y : cofiber f) : P :=
|
||||
pushout.elim (λu, Pbase) Pcod Pglue y
|
||||
protected theorem rec_glue {P : cofiber f → Type} (Pcod : Π (b : B), P (cod b)) (Pbase : P base)
|
||||
(Pglue : Π (a : A), pathover P (Pcod (f a)) (glue a) Pbase) (a : A)
|
||||
: apd (cofiber.rec Pcod Pbase Pglue) (cofiber.glue a) = Pglue a :=
|
||||
!pushout.rec_glue
|
||||
|
||||
protected definition elim_on {P : Type} (y : cofiber f) (Pbase : P) (Pcod : B → P)
|
||||
(Pglue : Π (x : A), Pbase = Pcod (f x)) : P :=
|
||||
cofiber.elim Pbase Pcod Pglue y
|
||||
protected definition elim {P : Type} (Pcod : B → P) (Pbase : P)
|
||||
(Pglue : Π (x : A), Pcod (f x) = Pbase) (y : cofiber f) : P :=
|
||||
pushout.elim Pcod (λu, Pbase) Pglue y
|
||||
|
||||
protected theorem elim_glue {P : Type} (y : cofiber f) (Pbase : P) (Pcod : B → P)
|
||||
(Pglue : Π (x : A), Pbase = Pcod (f x)) (a : A)
|
||||
: ap (elim Pbase Pcod Pglue) (glue a) = Pglue a :=
|
||||
protected definition elim_on {P : Type} (y : cofiber f) (Pcod : B → P) (Pbase : P)
|
||||
(Pglue : Π (x : A), Pcod (f x) = Pbase) : P :=
|
||||
cofiber.elim Pcod Pbase Pglue y
|
||||
|
||||
protected theorem elim_glue {P : Type} (Pcod : B → P) (Pbase : P)
|
||||
(Pglue : Π (x : A), Pcod (f x) = Pbase) (a : A)
|
||||
: ap (cofiber.elim Pcod Pbase Pglue) (cofiber.glue a) = Pglue a :=
|
||||
!pushout.elim_glue
|
||||
|
||||
end
|
||||
|
||||
end cofiber
|
||||
|
||||
attribute cofiber.base cofiber.cod [constructor]
|
||||
|
|
@ -78,21 +69,42 @@ notation `ℂ` := pcofiber
|
|||
|
||||
namespace cofiber
|
||||
|
||||
variables (A : Type*)
|
||||
variables {A B : Type*} (f : A →* B)
|
||||
|
||||
definition cofiber_unit : pcofiber (pconst A punit) ≃* psusp A :=
|
||||
definition is_contr_cofiber_of_equiv [H : is_equiv f] : is_contr (cofiber f) :=
|
||||
begin
|
||||
fapply is_contr.mk, exact cofiber.base f,
|
||||
intro a, induction a with b a,
|
||||
{ exact !glue⁻¹ ⬝ ap inl (right_inv f b) },
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover_constant_left_id_right, apply move_top_of_left,
|
||||
refine _ ⬝pv natural_square_tr cofiber.glue (left_inv f a) ⬝vp !ap_constant,
|
||||
refine ap02 inl _ ⬝ !ap_compose⁻¹, exact adj f a },
|
||||
end
|
||||
|
||||
definition pcod [constructor] (f : A →* B) : B →* pcofiber f :=
|
||||
pmap.mk (cofiber.cod f) (ap inl (respect_pt f)⁻¹ ⬝ cofiber.glue pt)
|
||||
|
||||
definition pcod_pcompose [constructor] (f : A →* B) : pcod f ∘* f ~* pconst A (ℂ f) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro a, exact cofiber.glue a },
|
||||
{ exact !con_inv_cancel_left⁻¹ ⬝ idp ◾ (!ap_inv⁻¹ ◾ idp) }
|
||||
end
|
||||
|
||||
definition pcofiber_punit (A : Type*) : pcofiber (pconst A punit) ≃* psusp A :=
|
||||
begin
|
||||
fapply pequiv_of_pmap,
|
||||
{ fconstructor, intro x, induction x, exact north, exact south, exact merid x,
|
||||
reflexivity },
|
||||
exact (merid pt)⁻¹ },
|
||||
{ esimp, fapply adjointify,
|
||||
{ intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a },
|
||||
{ intro s, induction s, do 2 reflexivity, esimp,
|
||||
apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square,
|
||||
refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
|
||||
refine ap _ !elim_merid ⬝ _, apply elim_glue },
|
||||
{ intro c, induction c with s, reflexivity,
|
||||
induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square,
|
||||
{ intro c, induction c with u, induction u, reflexivity,
|
||||
reflexivity, esimp, apply eq_pathover, apply hdeg_square,
|
||||
refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
|
||||
refine ap02 _ !elim_glue ⬝ _, apply elim_merid }},
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in a new issue