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

feat(library/hott) add theorem: if f is an equivalence, so is ap f

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-04 19:50:30 -05:00 committed by Leonardo de Moura
parent b3ad8c704a
commit 2712b9b18f
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/hott/equiv.lean
View file

@ -210,6 +210,22 @@ namespace IsEquiv
definition contr (Hf : IsEquiv f) (HA: Contr A) : (Contr B) :=
Contr.Contr_mk (f (center HA)) (λb, moveR_M Hf (contr HA (inv f b)))
definition ap (Hf : IsEquiv f) (x y : A) : IsEquiv (@ap A B f x y) :=
adjointify (ap f)
(λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y) --sorry sorry
(λq, ap_pp f _ _
⬝ whiskerR (ap_pp f _ _) _
⬝ ((ap_V f _ ⬝ inverse2 (inverse (adj f _)))
◾ (inverse (ap_compose (f⁻¹) f _))
◾ (adj f _)⁻¹)
⬝ concat_pA1_p (retr f) _ _
⬝ whiskerR (concat_Vp _) _
⬝ concat_1p _)
(λp, whiskerR (whiskerL _ (inverse (ap_compose f (f⁻¹) _))) _
⬝ concat_pA1_p (sect f) _ _
⬝ whiskerR (concat_Vp _) _
⬝ concat_1p _)
end
end IsEquiv