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

simplify ppi_loop_equiv

Browse source
This commit is contained in:
Ulrik Buchholtz 2017-07-08 09:48:11 +01:00
parent 9ee02cfad5
commit ad8b52cd59
1 changed files with 5 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
pointed_pi.hlean
View file

@ -190,27 +190,13 @@ namespace pointed
induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q, induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q,
end end
definition ppi_loop_equiv_lemma (p : k ~ k)
: (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k) ≃ (p pt = idp) :=
calc (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k)
≃ (p pt ⬝ ppi_gen.resp_pt k = idp ⬝ ppi_gen.resp_pt k)
: equiv_eq_closed_right (p pt ⬝ ppi_gen.resp_pt k) (inverse (idp_con (ppi_gen.resp_pt k)))
... ≃ (p pt = idp)
: eq_equiv_con_eq_con_right
variables (k l) variables (k l)
definition ppi_loop_equiv : (k = k) ≃ Π*(a : A), Ω (pType.mk (B a) (k a)) := definition ppi_loop_equiv : (k = k) ≃ Π*(a : A), Ω (pType.mk (B a) (k a)) :=
calc (k = k) ≃ (k ~~* k) begin
: ppi_eq_equiv induction k with k p, induction p,
... ≃ Σ(p : k ~ k), p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k exact ppi_eq_equiv (ppi_gen.mk k idp) (ppi_gen.mk k idp)
: ppi_homotopy.sigma_char k k end
... ≃ Σ(p : k ~ k), p pt = idp
: sigma_equiv_sigma_right
(λ p, ppi_loop_equiv_lemma p)
... ≃ Π*(a : A), pType.mk (k a = k a) idp
: ppi.sigma_char
... ≃ Π*(a : A), Ω (pType.mk (B a) (k a))
: erfl
variables {k l} variables {k l}
-- definition eq_of_ppi_homotopy (h : k ~~* l) : k = l := -- definition eq_of_ppi_homotopy (h : k ~~* l) : k = l :=