From 807224f3c1734a09edd61a4922c50ad7ef509b9b Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Tue, 4 Nov 2014 20:03:12 -0500 Subject: [PATCH] chore(library/hott) cleaned up the proof a bit --- library/hott/equiv.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean index bb7d4eb85..24669790c 100644 --- a/library/hott/equiv.lean +++ b/library/hott/equiv.lean @@ -212,19 +212,19 @@ namespace IsEquiv 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 _))) + (λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y) + (λq, !ap_pp + ⬝ whiskerR !ap_pp _ + ⬝ ((!ap_V ⬝ inverse2 ((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⁻¹) _))) _ + ⬝ whiskerR !concat_Vp _ + ⬝ !concat_1p) + (λp, whiskerR (whiskerL _ ((ap_compose f (f⁻¹) _)⁻¹)) _ ⬝ concat_pA1_p (sect f) _ _ - ⬝ whiskerR (concat_Vp _) _ - ⬝ concat_1p _) + ⬝ whiskerR !concat_Vp _ + ⬝ !concat_1p) end