087c44d614
For example, the pointed suspension operation was called Susp before this commit, but now is called psusp
99 lines
3.6 KiB
Text
99 lines
3.6 KiB
Text
/-
|
|
Copyright (c) 2016 Jakob von Raumer. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Jakob von Raumer
|
|
|
|
The Cofiber Type
|
|
-/
|
|
import hit.pointed_pushout function .susp
|
|
|
|
open eq pushout unit pointed is_trunc is_equiv susp unit
|
|
|
|
definition cofiber {A B : Type} (f : A → B) := pushout (λ (a : A), ⋆) f
|
|
|
|
namespace cofiber
|
|
section
|
|
parameters {A B : Type} (f : A → B)
|
|
|
|
protected definition base [constructor] : cofiber f := inl ⋆
|
|
|
|
protected definition cod [constructor] : B → cofiber f := inr
|
|
|
|
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
|
|
|
|
protected definition rec {A : Type} {B : Type} {f : A → B} {P : cofiber f → Type}
|
|
(Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (glue x) (Pinr (f x))) :
|
|
(Π y, P y) :=
|
|
begin
|
|
intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
|
|
end
|
|
|
|
protected definition rec_on {A : Type} {B : Type} {f : A → B} {P : cofiber f → Type}
|
|
(y : cofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (glue x) (Pinr (f x))) : P y :=
|
|
begin
|
|
induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
|
|
end
|
|
|
|
end
|
|
end cofiber
|
|
|
|
-- pointed version
|
|
|
|
definition pcofiber {A B : Type*} (f : A →* B) : Type* := ppushout (pconst A punit) f
|
|
|
|
namespace cofiber
|
|
|
|
protected definition prec {A B : Type*} {f : A →* B} {P : pcofiber f → Type}
|
|
(Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) :
|
|
(Π (y : pcofiber f), P y) :=
|
|
begin
|
|
intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
|
|
end
|
|
|
|
protected definition prec_on {A B : Type*} {f : A →* B} {P : pcofiber f → Type}
|
|
(y : pcofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) : P y :=
|
|
begin
|
|
induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
|
|
end
|
|
|
|
protected definition pelim_on {A B C : Type*} {f : A →* B} (y : pcofiber f)
|
|
(c : C) (g : B → C) (p : Π x, c = g (f x)) : C :=
|
|
begin
|
|
fapply pushout.elim_on y, exact (λ x, c), exact g, exact p
|
|
end
|
|
|
|
--TODO more pointed recursors
|
|
|
|
variables (A : Type*)
|
|
|
|
definition cofiber_unit : pcofiber (pconst A punit) ≃* psusp A :=
|
|
begin
|
|
fapply pequiv_of_pmap,
|
|
{ fconstructor, intro x, induction x, exact north, exact south, exact merid x,
|
|
reflexivity },
|
|
{ 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 [n, s], induction n, reflexivity,
|
|
induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square,
|
|
refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
|
|
refine ap _ !elim_glue ⬝ _, apply elim_merid },
|
|
end
|
|
|
|
end cofiber
|