michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hit/susp): finish the proof that loop space is adjoint to the suspension

Browse source
This commit is contained in:
Floris van Doorn 2015-06-17 19:31:05 -04:00
parent 124c9d3d8a
commit 2748525c21
5 changed files with 214 additions and 229 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

294
hott/hit/susp.hlean
View file

@ -27,10 +27,10 @@ namespace susp
protected definition rec {P : susp A → Type} (PN : P north) (PS : P south)
(Pm : Π(a : A), PN =[merid a] PS) (x : susp A) : P x :=
begin
fapply pushout.rec_on _ _ x,
{ intro u, cases u, exact PN},
{ intro u, cases u, exact PS},
{ exact Pm},
induction x with u u,
{ cases u, exact PN},
{ cases u, exact PS},
{ apply Pm},
end
protected definition rec_on [reducible] {P : susp A → Type} (y : susp A)
@ -80,15 +80,17 @@ attribute susp.elim_type_on [unfold-c 2]
namespace susp
open pointed
definition pointed_susp [instance] [constructor] (A : Type) : pointed (susp A) :=
variables {X Y Z : Pointed}
definition pointed_susp [instance] [constructor] (X : Type) : pointed (susp X) :=
pointed.mk north
definition Susp [constructor] (A : Type) : Pointed :=
pointed.mk' (susp A)
definition Susp [constructor] (X : Type) : Pointed :=
pointed.mk' (susp X)
definition Susp_functor {X Y : Pointed} (f : X →* Y) : Susp X →* Susp Y :=
definition Susp_functor (f : X →* Y) : Susp X →* Susp Y :=
begin
fapply pmap.mk,
constructor,
{ intro x, induction x,
apply north,
apply south,
@ -96,10 +98,10 @@ namespace susp
{ reflexivity}
end
definition Susp_functor_compose {X Y Z : Pointed} (g : Y →* Z) (f : X →* Y)
definition Susp_functor_compose (g : Y →* Z) (f : X →* Y)
: Susp_functor (g ∘* f) ~* Susp_functor g ∘* Susp_functor f :=
begin
fapply phomotopy.mk,
constructor,
{ intro a, induction a,
{ reflexivity},
{ reflexivity},
@ -112,198 +114,116 @@ namespace susp
definition loop_susp_unit [constructor] (X : Pointed) : X →* Ω(Susp X) :=
begin
fapply pmap.mk,
constructor,
{ intro x, exact merid x ⬝ (merid pt)⁻¹},
{ apply con.right_inv},
end
definition loop_susp_unit_natural {X Y : Pointed} (f : X →* Y)
definition loop_susp_unit_natural (f : X →* Y)
: loop_susp_unit Y ∘* f ~* ap1 (Susp_functor f) ∘* loop_susp_unit X :=
begin
induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
fapply phomotopy.mk,
{ intro x', esimp [Susp_functor],
refine _ ⬝ !idp_con⁻¹,
refine _ ⬝ !ap_con⁻¹,
exact (!elim_merid ◾ (!ap_inv ⬝ inverse2 !elim_merid))⁻¹},
constructor,
{ intro x', esimp [Susp_functor], symmetry,
exact
!idp_con ⬝
(!ap_con ⬝
whisker_left _ !ap_inv) ⬝
(!elim_merid ◾ (inverse2 !elim_merid))
},
{ rewrite [▸*,idp_con (con.right_inv _)],
exact sorry}, --apply inv_con_eq_of_eq_con,
apply inv_con_eq_of_eq_con,
refine _ ⬝ !con.assoc',
rewrite inverse2_right_inv,
refine _ ⬝ !con.assoc',
rewrite [ap_con_right_inv,↑Susp_functor,idp_con_idp,-ap_compose]},
end
-- p ⬝ q ⬝ r means (p ⬝ q) ⬝ r
definition loop_susp_counit [constructor] (X : Pointed) : Susp (Ω X) →* X :=
begin
constructor,
{ intro x, induction x, exact pt, exact pt, exact a},
{ reflexivity},
end
definition susp_adjoint_loop (A B : Pointed)
: map₊ (pointed.mk' (susp A)) B ≃ map₊ A (Ω B) := sorry
definition loop_susp_counit_natural (f : X →* Y)
: f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (Susp_functor (ap1 f)) :=
begin
induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
constructor,
{ intro x', induction x' with p,
{ reflexivity},
{ reflexivity},
{ esimp, apply pathover_eq, apply hdeg_square,
xrewrite [ap_compose _ f,ap_compose _ (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*,
+elim_merid,▸*,idp_con]}},
{ reflexivity}
end
exit
definition loop_susp_counit_unit (X : Pointed)
: ap1 (loop_susp_counit X) ∘* loop_susp_unit (Ω X) ~* pid (Ω X) :=
begin
induction X with X x, constructor,
{ intro p, esimp,
refine !idp_con ⬝
(!ap_con ⬝
whisker_left _ !ap_inv) ⬝
(!elim_merid ◾ inverse2 !elim_merid)},
{ rewrite [▸*,inverse2_right_inv (elim_merid function.id idp)],
refine !con.assoc ⬝ _,
xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose]}
end
Definition loop_susp_unit_natural {X Y : pType} (f : X ->* Y)
: loop_susp_unit Y o* f
==* loops_functor (psusp_functor f) o* loop_susp_unit X.
Proof.
pointed_reduce.
refine (Build_pHomotopy _ _); cbn.
- intros x; symmetry.
refine (concat_1p _@ (concat_p1 _ @ _)).
refine (ap_pp (Susp_rec North South (merid o f))
(merid x) (merid (point X))^ @ _).
refine ((1 @@ ap_V _ _) @ _).
refine (Susp_comp_nd_merid _ @@ inverse2 (Susp_comp_nd_merid _)).
- cbn. rewrite !inv_pp, !concat_pp_p, concat_1p; symmetry.
apply moveL_Vp.
refine (concat_pV_inverse2 _ _ (Susp_comp_nd_merid (point X)) @ _).
do 2 apply moveL_Vp.
refine (ap_pp_concat_pV _ _ @ _).
do 2 apply moveL_Vp.
rewrite concat_p1_1, concat_1p_1.
cbn; symmetry.
refine (concat_p1 _ @ _).
refine (ap_compose (fun p' => (ap (Susp_rec North South (merid o f))) p' @ 1)
(fun p' => 1 @ p')
(concat_pV (merid (point X))) @ _).
apply ap.
refine (ap_compose (ap (Susp_rec North South (merid o f)))
(fun p' => p' @ 1) _).
Qed.
definition loop_susp_unit_counit (X : Pointed)
: loop_susp_counit (Susp X) ∘* Susp_functor (loop_susp_unit X) ~* pid (Susp X) :=
begin
induction X with X x, constructor,
{ intro x', induction x',
{ reflexivity},
{ exact merid pt},
{ apply pathover_eq,
xrewrite [▸*, ap_id, ap_compose _ (susp.elim north north (λa, a)), +elim_merid,▸*],
apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹}},
{ reflexivity}
end
Definition loop_susp_counit (X : pType) : psusp (loops X) ->* X.
Proof.
refine (Build_pMap (psusp (loops X)) X
(Susp_rec (point X) (point X) idmap) 1).
Defined.
Definition loop_susp_counit_natural {X Y : pType} (f : X ->* Y)
: f o* loop_susp_counit X
==* loop_susp_counit Y o* psusp_functor (loops_functor f).
Proof.
pointed_reduce.
refine (Build_pHomotopy _ _); simpl.
- refine (Susp_ind _ _ _ _); cbn; try reflexivity; intros p.
rewrite transport_paths_FlFr, ap_compose, concat_p1.
apply moveR_Vp.
refine (ap_compose
(Susp_rec North South (fun x0 => merid (1 @ (ap f x0 @ 1))))
(Susp_rec (point Y) (point Y) idmap) (merid p) @ _).
do 2 rewrite Susp_comp_nd_merid.
refine (Susp_comp_nd_merid _ @ _). (** Not sure why [rewrite] fails here *)
apply concat_1p.
- reflexivity.
Qed.
(** Now the triangle identities *)
Definition loop_susp_triangle1 (X : pType)
: loops_functor (loop_susp_counit X) o* loop_susp_unit (loops X)
==* pmap_idmap (loops X).
Proof.
refine (Build_pHomotopy _ _).
- intros p; cbn.
refine (concat_1p _ @ (concat_p1 _ @ _)).
refine (ap_pp (Susp_rec (point X) (point X) idmap)
(merid p) (merid (point (point X = point X)))^ @ _).
refine ((1 @@ ap_V _ _) @ _).
refine ((Susp_comp_nd_merid p @@ inverse2 (Susp_comp_nd_merid (point (loops X)))) @ _).
exact (concat_p1 _).
- destruct X as [X x]; cbn; unfold point.
apply whiskerR.
rewrite (concat_pV_inverse2
(ap (Susp_rec x x idmap) (merid 1))
1 (Susp_comp_nd_merid 1)).
rewrite (ap_pp_concat_pV (Susp_rec x x idmap) (merid 1)).
rewrite ap_compose, (ap_compose _ (fun p => p @ 1)).
rewrite concat_1p_1; apply ap.
apply concat_p1_1.
Qed.
Definition loop_susp_triangle2 (X : pType)
: loop_susp_counit (psusp X) o* psusp_functor (loop_susp_unit X)
==* pmap_idmap (psusp X).
Proof.
refine (Build_pHomotopy _ _);
[ refine (Susp_ind _ _ _ _) | ]; try reflexivity; cbn.
- exact (merid (point X)).
- intros x.
rewrite transport_paths_FlFr, ap_idmap, ap_compose.
rewrite Susp_comp_nd_merid.
apply moveR_pM; rewrite concat_p1.
refine (inverse2 (Susp_comp_nd_merid _) @ _).
rewrite inv_pp, inv_V; reflexivity.
Qed.
(** Now we can finally construct the adjunction equivalence. *)
Definition loop_susp_adjoint `{Funext} (A B : pType)
: (psusp A ->* B) <~> (A ->* loops B).
Proof.
refine (equiv_adjointify
(fun f => loops_functor f o* loop_susp_unit A)
(fun g => loop_susp_counit B o* psusp_functor g) _ _).
- intros g. apply path_pmap.
refine (pmap_prewhisker _ (loops_functor_compose _ _) @* _).
refine (pmap_compose_assoc _ _ _ @* _).
refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _).
refine ((pmap_compose_assoc _ _ _)^* @* _).
refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _).
apply pmap_postcompose_idmap.
- intros f. apply path_pmap.
refine (pmap_postwhisker _ (psusp_functor_compose _ _) @* _).
refine ((pmap_compose_assoc _ _ _)^* @* _).
refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _).
refine (pmap_compose_assoc _ _ _ @* _).
refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _).
apply pmap_precompose_idmap.
Defined.
(** And its naturality is easy. *)
Definition loop_susp_adjoint_nat_r `{Funext} (A B B' : pType)
(f : psusp A ->* B) (g : B ->* B')
: loop_susp_adjoint A B' (g o* f)
==* loops_functor g o* loop_susp_adjoint A B f.
Proof.
cbn.
refine (_ @* pmap_compose_assoc _ _ _).
apply pmap_prewhisker.
refine (loops_functor_compose g f).
Defined.
Definition loop_susp_adjoint_nat_l `{Funext} (A A' B : pType)
(f : A ->* loops B) (g : A' ->* A)
: (loop_susp_adjoint A' B)^-1 (f o* g)
==* (loop_susp_adjoint A B)^-1 f o* psusp_functor g.
Proof.
cbn.
refine (_ @* (pmap_compose_assoc _ _ _)^*).
apply pmap_postwhisker.
refine (psusp_functor_compose f g).
Defined.
definition susp_adjoint_loop (A B : Pointed)
: map₊ (pointed.mk' (susp A)) B ≃ map₊ A (Ω B) :=
definition susp_adjoint_loop (X Y : Pointed) : map₊ (pointed.mk' (susp X)) Y ≃ map₊ X (Ω Y) :=
begin
fapply equiv.MK,
{ intro f, fapply pointed_map.mk,
intro a, refine !respect_pt⁻¹ ⬝ ap f (merid a ⬝ (merid pt)⁻¹) ⬝ !respect_pt,
refine ap _ !con.right_inv ⬝ !con.left_inv},
{ intro g, fapply pointed_map.mk,
{ esimp, intro a, induction a,
exact pt,
exact pt,
exact g a} ,
{ reflexivity}},
{ intro g, fapply pointed_map_eq,
intro a, esimp [respect_pt], refine !idp_con ⬝ !ap_con ⬝ ap _ !ap_inv
⬝ ap _ !elim_merid ⬝ ap _ !elim_merid ⬝ ap _ (respect_pt g) ⬝ _, exact idp,
-- rewrite [ap_con,ap_inv,+elim_merid,idp_con,respect_pt],
esimp, exact sorry},
{ intro f, fapply pointed_map_eq,
{ esimp, intro a, induction a; all_goals esimp,
exact !respect_pt⁻¹,
exact !respect_pt⁻¹ ⬝ ap f (merid pt),
apply pathover_eq, exact sorry},
{ esimp, exact !con.left_inv⁻¹}},
{ intro f, exact ap1 f ∘* loop_susp_unit X},
{ intro g, exact loop_susp_counit Y ∘* Susp_functor g},
{ intro g, apply eq_of_phomotopy, esimp,
refine !pwhisker_right !ap1_compose ⬝* _,
refine !passoc ⬝* _,
refine !pwhisker_left !loop_susp_unit_natural⁻¹* ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine !pwhisker_right !loop_susp_counit_unit ⬝* _,
apply pid_comp},
{ intro f, apply eq_of_phomotopy, esimp,
refine !pwhisker_left !Susp_functor_compose ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _,
refine !passoc ⬝* _,
refine !pwhisker_left !loop_susp_unit_counit ⬝* _,
apply comp_pid},
end
definition susp_adjoint_loop_nat_right (f : Susp X →* Y) (g : Y →* Z)
: susp_adjoint_loop X Z (g ∘* f) ~* ap1 g ∘* susp_adjoint_loop X Y f :=
begin
esimp [susp_adjoint_loop],
refine _ ⬝* !passoc,
apply pwhisker_right,
apply ap1_compose
end
definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y)
: (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* Susp_functor g :=
begin
esimp [susp_adjoint_loop],
refine _ ⬝* !passoc⁻¹*,
apply pwhisker_left,
apply Susp_functor_compose
end
end susp

4
hott/init/path.hlean
View file

@ -63,11 +63,11 @@ namespace eq
eq.rec_on r (eq.rec_on q idp)
-- The left inverse law.
definition con.right_inv (p : x = y) : p ⬝ p⁻¹ = idp :=
definition con.right_inv [unfold-c 4] (p : x = y) : p ⬝ p⁻¹ = idp :=
eq.rec_on p idp
-- The right inverse law.
definition con.left_inv (p : x = y) : p⁻¹ ⬝ p = idp :=
definition con.left_inv [unfold-c 4] (p : x = y) : p⁻¹ ⬝ p = idp :=
eq.rec_on p idp
/- Several auxiliary theorems about canceling inverses across associativity. These are somewhat

58
hott/types/eq.hlean
View file

@ -15,50 +15,64 @@ namespace eq
/- Path spaces -/
variables {A B : Type} {a a1 a2 a3 a4 : A} {b b1 b2 : B} {f g : A → B} {h : B → A}
{p p' p'' : a1 = a2}
/- The path spaces of a path space are not, of course, determined; they are just the
higher-dimensional structure of the original space. -/
/- some lemmas about whiskering or other higher paths -/
definition whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'')
theorem whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'')
: whisker_left p (r ⬝ s) = whisker_left p r ⬝ whisker_left p s :=
begin
cases p, cases r, cases s, exact idp
cases p, cases r, cases s, reflexivity
end
definition whisker_right_con_right {p p' p'' : a1 = a2} (q : a2 = a3) (r : p = p') (s : p' = p'')
theorem whisker_right_con_right (q : a2 = a3) (r : p = p') (s : p' = p'')
: whisker_right (r ⬝ s) q = whisker_right r q ⬝ whisker_right s q :=
begin
cases q, cases r, cases s, exact idp
cases q, cases r, cases s, reflexivity
end
definition whisker_left_con_left (p : a1 = a2) (p' : a2 = a3) {q q' : a3 = a4} (r : q = q')
theorem whisker_left_con_left (p : a1 = a2) (p' : a2 = a3) {q q' : a3 = a4} (r : q = q')
: whisker_left (p ⬝ p') r = !con.assoc ⬝ whisker_left p (whisker_left p' r) ⬝ !con.assoc' :=
begin
cases p', cases p, cases r, cases q, exact idp
cases p', cases p, cases r, cases q, reflexivity
end
definition whisker_right_con_left {p p' : a1 = a2} (q : a2 = a3) (q' : a3 = a4) (r : p = p')
theorem whisker_right_con_left {p p' : a1 = a2} (q : a2 = a3) (q' : a3 = a4) (r : p = p')
: whisker_right r (q ⬝ q') = !con.assoc' ⬝ whisker_right (whisker_right r q) q' ⬝ !con.assoc :=
begin
cases q', cases q, cases r, cases p, exact idp
cases q', cases q, cases r, cases p, reflexivity
end
definition whisker_left_inv_left (p : a2 = a1) {q q' : a2 = a3} (r : q = q')
theorem whisker_left_inv_left (p : a2 = a1) {q q' : a2 = a3} (r : q = q')
: !con_inv_cancel_left⁻¹ ⬝ whisker_left p (whisker_left p⁻¹ r) ⬝ !con_inv_cancel_left = r :=
begin
cases p, cases r, cases q, exact idp
cases p, cases r, cases q, reflexivity
end
definition con_right_inv2 (p : a1 = a2) : (con.right_inv p)⁻¹ ⬝ con.right_inv p = idp :=
by cases p;exact idp
theorem ap_eq_ap10 {f g : A → B} (p : f = g) (a : A) : ap (λh, h a) p = ap10 p a :=
by cases p;reflexivity
definition con_left_inv2 (p : a1 = a2) : (con.left_inv p)⁻¹ ⬝ con.left_inv p = idp :=
by cases p;exact idp
theorem inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p :=
by cases r;cases p;reflexivity
definition ap_eq_ap10 {f g : A → B} (p : f = g) (a : A) : ap (λh, h a) p = ap10 p a :=
by cases p;exact idp
theorem inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p :=
by cases r;cases p;reflexivity
theorem ap_con_right_inv (f : A → B) (p : a1 = a2)
: ap_con f p p⁻¹ ⬝ whisker_left _ (ap_inv f p) ⬝ con.right_inv (ap f p)
= ap (ap f) (con.right_inv p) :=
by cases p;reflexivity
theorem ap_con_left_inv (f : A → B) (p : a1 = a2)
: ap_con f p⁻¹ p ⬝ whisker_right (ap_inv f p) _ ⬝ con.left_inv (ap f p)
= ap (ap f) (con.left_inv p) :=
by cases p;reflexivity
theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
by cases q;reflexivity
/- Transporting in path spaces.
@ -177,7 +191,7 @@ namespace eq
is_equiv.mk (concat p) (concat p⁻¹)
(con_inv_cancel_left p)
(inv_con_cancel_left p)
(λq, by cases p;cases q;exact idp)
(λq, by cases p;cases q;reflexivity)
local attribute is_equiv_concat_left [instance]
definition equiv_eq_closed_left [constructor] (a3 : A) (p : a1 = a2) : (a1 = a3) ≃ (a2 = a3) :=
@ -188,7 +202,7 @@ namespace eq
is_equiv.mk (λq, q ⬝ p) (λq, q ⬝ p⁻¹)
(λq, inv_con_cancel_right q p)
(λq, con_inv_cancel_right q p)
(λq, by cases p;cases q;exact idp)
(λq, by cases p;cases q;reflexivity)
local attribute is_equiv_concat_right [instance]
definition equiv_eq_closed_right [constructor] (a1 : A) (p : a2 = a3) : (a1 = a2) ≃ (a1 = a3) :=
@ -208,10 +222,10 @@ namespace eq
apply concat2,
{apply concat, {apply whisker_left_con_right},
apply concat2,
{cases p, cases q, exact idp},
{exact idp}},
{cases p, cases r, exact idp}},
{intro s, cases s, cases q, cases p, exact idp}
{cases p, cases q, reflexivity},
{reflexivity}},
{cases p, cases r, reflexivity}},
{intro s, cases s, cases q, cases p, reflexivity}
end
definition eq_equiv_con_eq_con_left (p : a1 = a2) (q r : a2 = a3) : (q = r) ≃ (p ⬝ q = p ⬝ r) :=

85
hott/types/pointed.hlean
View file

@ -30,7 +30,8 @@ namespace pointed
pointed.mk (Point A)
-- Any contractible type is pointed
definition pointed_of_is_contr [instance] [constructor] (A : Type) [H : is_contr A] : pointed A :=
definition pointed_of_is_contr [instance] [priority 800] [constructor]
(A : Type) [H : is_contr A] : pointed A :=
pointed.mk !center
-- A pi type with a pointed target is pointed
@ -99,15 +100,13 @@ open pmap
namespace pointed
variables {A B C D : Pointed}
abbreviation respect_pt [unfold-c 3] := @pmap.resp_pt
notation `map₊` := pmap
infix `→*`:30 := pmap
attribute pmap.map [coercion]
definition pmap_eq {f g : map₊ A B}
(r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
variables {A B C D : Pointed} {f g h : A →* B}
definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
begin
cases f with f p, cases g with g q,
esimp at *,
@ -131,22 +130,36 @@ namespace pointed
infix `~*`:50 := phomotopy
abbreviation to_homotopy_pt [unfold-c 5] := @phomotopy.homotopy_pt
abbreviation to_homotopy [coercion] [unfold-c 5] {f g : A →* B} (p : f ~* g) : Πa, f a = g a :=
abbreviation to_homotopy [coercion] [unfold-c 5] (p : f ~* g) : Πa, f a = g a :=
phomotopy.homotopy p
definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) :=
begin
fapply phomotopy.mk, intro a, reflexivity,
constructor, intro a, reflexivity,
cases A, cases B, cases C, cases D, cases f with f pf, cases g with g pg, cases h with h ph,
esimp at *,
induction pf, induction pg, induction ph, reflexivity
end
definition pid_comp (f : A →* B) : pid B ∘* f ~* f :=
begin
constructor,
{ intro a, reflexivity},
{ esimp, exact !idp_con ⬝ !ap_id⁻¹}
end
definition comp_pid (f : A →* B) : f ∘* pid A ~* f :=
begin
constructor,
{ intro a, reflexivity},
{ reflexivity}
end
definition pmap_equiv_left (A : Type) (B : Pointed) : A₊ →* B ≃ (A → B) :=
begin
fapply equiv.MK,
{ intro f a, cases f with f p, exact f (some a)},
{ intro f, fapply pmap.mk,
{ intro f, constructor,
intro a, cases a, exact pt, exact f a,
reflexivity},
{ intro f, reflexivity},
@ -180,7 +193,7 @@ namespace pointed
begin
fapply equiv.MK,
{ intro f, cases f with f p, exact f tt},
{ intro b, fapply pmap.mk,
{ intro b, constructor,
intro u, cases u, exact pt, exact b,
reflexivity},
{ intro b, reflexivity},
@ -196,37 +209,75 @@ namespace pointed
{ intros A B f, rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Ω A),
↑Iterated_loop_space, ↓Iterated_loop_space n (Ω B)],
apply IH (Ω A),
{ esimp, fapply pmap.mk,
{ esimp, constructor,
intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt,
esimp, apply con.left_inv}}
end
definition ap1 [constructor] (f : A →* B) := apn (succ 0) f
definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := apn (succ 0) f
protected definition phomotopy.trans [trans] {f g h : A →* B} (p : f ~* g) (q : g ~* h)
definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
begin
induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
induction pg, induction pf,
constructor,
{ intro p, esimp, apply whisker_left, exact ap_compose f g p ⬝ ap (ap g) !idp_con⁻¹},
{ reflexivity}
end
protected definition phomotopy.refl [refl] (f : A →* B) : f ~* f :=
begin
constructor,
{ intro a, exact idp},
{ apply idp_con}
end
protected definition phomotopy.trans [trans] (p : f ~* g) (q : g ~* h)
: f ~* h :=
begin
fapply phomotopy.mk,
constructor,
{ intro a, exact p a ⬝ q a},
{ induction f, induction g, induction p with p p', induction q with q q', esimp at *,
induction p', induction q', esimp, apply con.assoc}
end
protected definition phomotopy.symm [symm] {f g : A →* B} (p : f ~* g) : g ~* f :=
protected definition phomotopy.symm [symm] (p : f ~* g) : g ~* f :=
begin
fapply phomotopy.mk,
constructor,
{ intro a, exact (p a)⁻¹},
{ induction f, induction p with p p', esimp at *,
induction p', esimp, apply inv_con_cancel_left}
end
definition eq_of_phomotopy {f g : A →* B} (p : f ~* g) : f = g :=
infix `⬝*`:75 := phomotopy.trans
postfix `⁻¹*`:(max+1) := phomotopy.symm
definition eq_of_phomotopy (p : f ~* g) : f = g :=
begin
fapply pmap_eq,
{ intro a, exact p a},
{ exact !to_homotopy_pt⁻¹}
end
definition pwhisker_left (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g :=
begin
constructor,
{ intro a, exact ap h (p a)},
{ induction A, induction B, induction C,
induction f with f pf, induction g with g pg, induction h with h ph,
induction p with p p', esimp at *, induction ph, induction pg, induction p', reflexivity}
end
definition pwhisker_right (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h :=
begin
constructor,
{ intro a, exact p (h a)},
{ induction A, induction B, induction C,
induction f with f pf, induction g with g pg, induction h with h ph,
induction p with p p', esimp at *, induction ph, induction pg, induction p', esimp,
exact !idp_con⁻¹}
end
structure pequiv (A B : Pointed) :=
(to_pmap : A →* B)
(is_equiv_to_pmap : is_equiv to_pmap)

2
hott/types/trunc.hlean
View file

@ -165,7 +165,7 @@ namespace is_trunc
{ esimp, transitivity _,
apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹),
esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv},
{ esimp, apply con_right_inv2}},
{ esimp, apply con.left_inv}},
transitivity _,
apply iff.pi_iff_pi, intro p,
rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Loop_space (pointed.Mk p)),H],