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

chore(library/hott) cleaned up the proof a bit

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-04 20:03:12 -05:00 committed by Leonardo de Moura
parent 2712b9b18f
commit 807224f3c1
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/hott/equiv.lean
View file

@ -212,19 +212,19 @@ namespace IsEquiv
definition ap (Hf : IsEquiv f) (x y : A) : IsEquiv (@ap A B f x y) := definition ap (Hf : IsEquiv f) (x y : A) : IsEquiv (@ap A B f x y) :=
adjointify (ap f) adjointify (ap f)
(λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y) --sorry sorry (λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y)
(λq, ap_pp f _ _ (λq, !ap_pp
⬝ whiskerR (ap_pp f _ _) _ ⬝ whiskerR !ap_pp _
⬝ ((ap_V f _ ⬝ inverse2 (inverse (adj f _))) ⬝ ((!ap_V ⬝ inverse2 ((adj f _)⁻¹))
◾ (inverse (ap_compose (f⁻¹) f _)) ◾ (inverse (ap_compose (f⁻¹) f _))
◾ (adj f _)⁻¹) ◾ (adj f _)⁻¹)
⬝ concat_pA1_p (retr f) _ _ ⬝ concat_pA1_p (retr f) _ _
⬝ whiskerR (concat_Vp _) _ ⬝ whiskerR !concat_Vp _
⬝ concat_1p _) ⬝ !concat_1p)
(λp, whiskerR (whiskerL _ (inverse (ap_compose f (f⁻¹) _))) _ (λp, whiskerR (whiskerL _ ((ap_compose f (f⁻¹) _)⁻¹)) _
⬝ concat_pA1_p (sect f) _ _ ⬝ concat_pA1_p (sect f) _ _
⬝ whiskerR (concat_Vp _) _ ⬝ whiskerR !concat_Vp _
⬝ concat_1p _) ⬝ !concat_1p)
end end