From b70841171ad48a442ed14de9770ba22f00a77915 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 27 Apr 2015 15:39:36 -0400 Subject: [PATCH] fix(hott): rename retr and sect to right_inv and left_inv --- .../category/constructions/functor.hlean | 8 +-- .../algebra/category/constructions/hset.hlean | 4 +- hott/algebra/category/iso.hlean | 2 +- hott/arity.hlean | 12 ++--- hott/init/equiv.hlean | 52 +++++++++---------- hott/init/funext.hlean | 14 ++--- hott/init/ua.hlean | 2 +- hott/types/equiv.hlean | 20 +++---- hott/types/pi.hlean | 12 ++--- hott/types/sigma.hlean | 32 ++++++------ 10 files changed, 79 insertions(+), 79 deletions(-) diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 8acfd17b1..72c2fd31c 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -125,9 +125,9 @@ namespace category {exact (eq_of_iso_ob η)}, {intros [c, c', f], --unfold eq_of_iso_ob, --TODO: report: this fails apply concat, - {apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)}, + {apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (right_inv iso_of_eq)}, apply concat, - {apply (ap (λx, _ ∘ to_fun_hom F f ∘ (to_hom x)⁻¹)), apply (retr iso_of_eq)}, + {apply (ap (λx, _ ∘ to_fun_hom F f ∘ (to_hom x)⁻¹)), apply (right_inv iso_of_eq)}, apply inverse, apply naturality_iso} end @@ -138,7 +138,7 @@ namespace category intro c, rewrite natural_map_hom_of_eq, esimp [eq_of_iso], rewrite ap010_functor_eq, esimp [hom_of_eq,eq_of_iso_ob], - rewrite (retr iso_of_eq), + rewrite (right_inv iso_of_eq), end definition eq_of_iso_iso_of_eq (p : F = G) : eq_of_iso (iso_of_eq p) = p := @@ -149,7 +149,7 @@ namespace category rewrite ap010_functor_eq, esimp [eq_of_iso_ob], rewrite componentwise_iso_iso_of_eq, - rewrite (sect iso_of_eq) + rewrite (left_inv iso_of_eq) end definition is_univalent (D : Category) (C : Precategory) : is_univalent (D ^c C) := diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean index 94a7dffaa..f15113d26 100644 --- a/hott/algebra/category/constructions/hset.hlean +++ b/hott/algebra/category/constructions/hset.hlean @@ -31,8 +31,8 @@ namespace category definition iso_of_equiv {A B : Precategory_hset} (f : A ≃ B) : A ≅ B := iso.MK (to_fun f) (equiv.to_inv f) - (eq_of_homotopy (sect (to_fun f))) - (eq_of_homotopy (retr (to_fun f))) + (eq_of_homotopy (left_inv (to_fun f))) + (eq_of_homotopy (right_inv (to_fun f))) definition equiv_of_iso {A B : Precategory_hset} (f : A ≅ B) : A ≃ B := equiv.MK (to_hom f) diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 585890b73..a40604e6c 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -208,7 +208,7 @@ namespace iso eq_of_homotopy p ▹ f = hom_of_eq (apd10 (eq_of_homotopy p) y) ∘ f ∘ inv_of_eq (apd10 (eq_of_homotopy p) x) : transport_hom_of_eq - ... = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) : {retr apd10 p} + ... = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) : {right_inv apd10 p} end structure mono [class] (f : a ⟶ b) := diff --git a/hott/arity.hlean b/hott/arity.hlean index b317cc1fd..965115872 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -144,8 +144,8 @@ namespace funext begin intro H, esimp [apd100, eq_of_homotopy2, function.compose], apply eq_of_homotopy, intro a, - apply concat, apply (ap (λx, apd10 (x a))), apply (retr apd10), - apply (retr apd10) + apply concat, apply (ap (λx, apd10 (x a))), apply (right_inv apd10), + apply (right_inv apd10) end begin intro p, cases p, apply eq_of_homotopy2_id @@ -159,9 +159,9 @@ namespace funext intro H, apply eq_of_homotopy, intro a, apply concat, {apply (ap (λx, @apd100 _ _ (λ(b : B a)(c : C a b), _) _ _ (x a))), - apply (retr apd10)}, + apply (right_inv apd10)}, --TODO: remove implicit argument after #469 is closed - apply (@retr _ _ apd100 !is_equiv_apd100) --is explicit argument needed here? + apply (@right_inv _ _ apd100 !is_equiv_apd100) --is explicit argument needed here? end begin intro p, cases p, apply eq_of_homotopy3_id @@ -173,11 +173,11 @@ namespace eq local attribute funext.is_equiv_apd100 [instance] protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type} (p : f ∼2 g) (H : Π(q : f = g), P (apd100 q)) : P p := - retr apd100 p ▹ H (eq_of_homotopy2 p) + right_inv apd100 p ▹ H (eq_of_homotopy2 p) protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type} (p : f ∼3 g) (H : Π(q : f = g), P (apd1000 q)) : P p := - retr apd1000 p ▹ H (eq_of_homotopy3 p) + right_inv apd1000 p ▹ H (eq_of_homotopy3 p) definition apd10_ap (f : X → Πa, B a) (p : x = x') : apd10 (ap f p) = ap010 f p := diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index c604cff19..c113a7f0f 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -19,9 +19,9 @@ open eq function structure is_equiv [class] {A B : Type} (f : A → B) := mk' :: (inv : B → A) - (retr : (f ∘ inv) ∼ id) - (sect : (inv ∘ f) ∼ id) - (adj : Πx, retr (f x) = ap f (sect x)) + (right_inv : (f ∘ inv) ∼ id) + (left_inv : (inv ∘ f) ∼ id) + (adj : Πx, right_inv (f x) = ap f (left_inv x)) attribute is_equiv.inv [quasireducible] @@ -50,11 +50,11 @@ namespace is_equiv -- The composition of two equivalences is, again, an equivalence. definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (g ∘ f) := is_equiv.mk (g ∘ f) (f⁻¹ ∘ g⁻¹) - (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c) - (λa, ap (inv f) (sect g (f a)) ⬝ sect f a) + (λc, ap g (right_inv f (g⁻¹ c)) ⬝ right_inv g c) + (λa, ap (inv f) (left_inv g (f a)) ⬝ left_inv f a) (λa, (whisker_left _ (adj g (f a))) ⬝ (ap_con g _ _)⁻¹ ⬝ - ap02 g ((ap_con_eq_con (retr f) (sect g (f a)))⁻¹ ⬝ + ap02 g ((ap_con_eq_con (right_inv f) (left_inv g (f a)))⁻¹ ⬝ (ap_compose (inv f) f _ ◾ adj f a) ⬝ (ap_con f _ _)⁻¹ ) ⬝ @@ -67,14 +67,14 @@ namespace is_equiv -- Any function pointwise equal to an equivalence is an equivalence as well. definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') := - let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ retr f b) in - let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ sect f a) in + let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ right_inv f b) in + let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ left_inv f a) in let adj' := (λ (a : A), let ff'a := Hty a in let invf := inv f in - let secta := sect f a in - let retrfa := retr f (f a) in - let retrf'a := retr f (f' a) in + let secta := left_inv f a in + let retrfa := right_inv f (f a) in + let retrf'a := right_inv f (f' a) in have eq1 : _ = _, from calc ap f secta ⬝ ff'a = retrfa ⬝ ff'a : by rewrite adj @@ -147,29 +147,29 @@ namespace is_equiv --The inverse of an equivalence is, again, an equivalence. definition is_equiv_inv [instance] : (is_equiv f⁻¹) := - adjointify f⁻¹ f (sect f) (retr f) + adjointify f⁻¹ f (left_inv f) (right_inv f) definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) := have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, - @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@retr _ _ f _ b)) + @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@right_inv _ _ f _ b)) definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) := have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, - @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, sect f (g a)) + @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, left_inv f (g a)) definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) := adjointify (ap f) - (λq, (inverse (sect f x)) ⬝ ap f⁻¹ q ⬝ sect f y) + (λq, (inverse (left_inv f x)) ⬝ ap f⁻¹ q ⬝ left_inv f y) (λq, !ap_con ⬝ whisker_right !ap_con _ ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) ◾ (inverse (ap_compose f⁻¹ f _)) ◾ (adj f _)⁻¹) - ⬝ con_ap_con_eq_con_con (retr f) _ _ + ⬝ con_ap_con_eq_con_con (right_inv f) _ _ ⬝ whisker_right !con.left_inv _ ⬝ !idp_con) (λp, whisker_right (whisker_left _ (ap_compose f f⁻¹ _)⁻¹) _ - ⬝ con_ap_con_eq_con_con (sect f) _ _ + ⬝ con_ap_con_eq_con_con (left_inv f) _ _ ⬝ whisker_right !con.left_inv _ ⬝ !idp_con) @@ -183,15 +183,15 @@ namespace is_equiv definition equiv_rect (P : B → Type) : (Πx, P (f x)) → (Πy, P y) := - (λg y, eq.transport _ (retr f y) (g (f⁻¹ y))) + (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y))) definition equiv_rect_comp (P : B → Type) (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x := calc equiv_rect f P df (f x) - = transport P (retr f (f x)) (df (f⁻¹ (f x))) : by esimp - ... = transport P (eq.ap f (sect f x)) (df (f⁻¹ (f x))) : by rewrite adj - ... = transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : by rewrite -transport_compose - ... = df x : by rewrite (apd df (sect f x)) + = transport P (right_inv f (f x)) (df (f⁻¹ (f x))) : by esimp + ... = transport P (eq.ap f (left_inv f x)) (df (f⁻¹ (f x))) : by rewrite adj + ... = transport (P ∘ f) (left_inv f x) (df (f⁻¹ (f x))) : by rewrite -transport_compose + ... = df x : by rewrite (apd df (left_inv f x)) end @@ -201,13 +201,13 @@ namespace is_equiv --Rewrite rules definition eq_of_eq_inv (p : a = f⁻¹ b) : f a = b := - ap f p ⬝ retr f b + ap f p ⬝ right_inv f b definition eq_of_inv_eq (p : f⁻¹ b = a) : b = f a := (eq_of_eq_inv p⁻¹)⁻¹ definition inv_eq_of_eq (p : b = f a) : f⁻¹ b = a := - ap f⁻¹ p ⬝ sect f a + ap f⁻¹ p ⬝ left_inv f a definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b := (inv_eq_of_eq p⁻¹)⁻¹ @@ -234,8 +234,8 @@ namespace equiv variables {A B C : Type} protected definition MK [reducible] (f : A → B) (g : B → A) - (retr : f ∘ g ∼ id) (sect : g ∘ f ∼ id) : A ≃ B := - equiv.mk f (adjointify f g retr sect) + (right_inv : f ∘ g ∼ id) (left_inv : g ∘ f ∼ id) : A ≃ B := + equiv.mk f (adjointify f g right_inv left_inv) definition to_inv [reducible] (f : A ≃ B) : B → A := f⁻¹ diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 4af286bd7..feeaa69e0 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -101,11 +101,11 @@ theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} := proof homotopy_ind_comp f eq_to_f idp qed, assert t2 : apd10 (sim2path f (homotopy.refl f)) = (homotopy.refl f), proof ap apd10 t1 qed, - have sect : apd10 ∘ (sim2path g) ∼ id, + have left_inv : apd10 ∘ (sim2path g) ∼ id, proof (homotopy_ind f (λ g' x, apd10 (sim2path g' x) = x) t2) g qed, - have retr : (sim2path g) ∘ apd10 ∼ id, + have right_inv : (sim2path g) ∘ apd10 ∼ id, from (λ h, eq.rec_on h (homotopy_ind_comp f _ idp)), - is_equiv.adjointify apd10 (sim2path g) sect retr + is_equiv.adjointify apd10 (sim2path g) left_inv right_inv definition funext_from_naive_funext : naive_funext → funext := compose funext_of_weak_funext weak_funext_of_naive_funext @@ -123,7 +123,7 @@ section (@compose C B A (is_equiv.inv w)) (λ (x : C → B), have eqretr : eq' = w', - from (@retr _ _ (@equiv_of_eq A B) (univalence A B) w'), + from (@right_inv _ _ (@equiv_of_eq A B) (univalence A B) w'), have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹, from inv_eq eq' w' eqretr, have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) = x, @@ -141,7 +141,7 @@ section ) (λ (x : C → A), have eqretr : eq' = w', - from (@retr _ _ (@equiv_of_eq A B) (univalence A B) w'), + from (@right_inv _ _ (@equiv_of_eq A B) (univalence A B) w'), have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹, from inv_eq eq' w' eqretr, have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) = x, @@ -249,11 +249,11 @@ definition eq_of_homotopy [reducible] : f ∼ g → f = g := --TODO: rename to eq_of_homotopy_idp definition eq_of_homotopy_idp (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f := -is_equiv.sect apd10 idp +is_equiv.left_inv apd10 idp definition naive_funext_of_ua : naive_funext := λ A P f g h, eq_of_homotopy h protected definition homotopy.rec_on {Q : (f ∼ g) → Type} (p : f ∼ g) (H : Π(q : f = g), Q (apd10 q)) : Q p := -retr apd10 p ▹ H (eq_of_homotopy p) +right_inv apd10 p ▹ H (eq_of_homotopy p) diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index e7d9f5139..36c8cb5b6 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -46,6 +46,6 @@ namespace equiv definition rec_on_of_equiv_of_eq {A B : Type} {P : (A ≃ B) → Type} (p : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P p := - retr equiv_of_eq p ▹ H (ua p) + right_inv equiv_of_eq p ▹ H (ua p) end equiv diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 806216d0b..4c09fe0bb 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -21,15 +21,15 @@ namespace is_equiv include H definition is_contr_fiber_of_is_equiv (b : B) : is_contr (fiber f b) := is_contr.mk - (fiber.mk (f⁻¹ b) (retr f b)) - (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ sect f a) (calc - retr f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ retr f b) : by rewrite inv_con_cancel_left - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (retr f (f a) ⬝ p) : by rewrite ap_con_eq_con - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (sect f a) ⬝ p) : by rewrite adj - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite con.assoc - ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_compose - ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_inv - ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ sect f a) ⬝ p : by rewrite ap_con))) + (fiber.mk (f⁻¹ b) (right_inv f b)) + (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc + right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc + ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose + ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv + ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con))) definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) := begin @@ -59,7 +59,7 @@ namespace is_equiv protected definition sigma_char : (is_equiv f) ≃ (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a)) := - equiv.MK (λH, ⟨inv f, retr f, sect f, adj f⟩) + equiv.MK (λH, ⟨inv f, right_inv f, left_inv f, adj f⟩) (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2) (λp, begin cases p with [p1, p2], diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 4617637df..54739915f 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -27,10 +27,10 @@ namespace pi /- Now we show how these things compute. -/ definition apd10_eq_of_homotopy (h : f ∼ g) : apd10 (eq_of_homotopy h) ∼ h := - apd10 (retr apd10 h) + apd10 (right_inv apd10 h) definition eq_of_homotopy_eta (p : f = g) : eq_of_homotopy (apd10 p) = p := - sect apd10 p + left_inv apd10 p definition eq_of_homotopy_idp (f : Πa, B a) : eq_of_homotopy (λx : A, refl (f x)) = refl f := !eq_of_homotopy_eta @@ -121,21 +121,21 @@ namespace pi : is_equiv (pi_functor f0 f1) := begin apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹ - (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))), + (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))), intro h, apply eq_of_homotopy, unfold pi_functor, unfold function.compose, unfold function.id, begin intro a', apply (tr_inv _ (adj f0 a')), - apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (sect f0 a') _)), + apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (left_inv f0 a') _)), apply (tr_inv (λx, x = h a') (fn_tr_eq_tr_fn _ f1 _)), unfold function.compose, - apply (tr_inv (λx, sect f0 a' ▹ x = h a') (retr (f1 _) _)), unfold function.id, + apply (tr_inv (λx, left_inv f0 a' ▹ x = h a') (right_inv (f1 _) _)), unfold function.id, apply apd end, begin intro h, apply eq_of_homotopy, intro a, - apply (tr_inv (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)), unfold function.id, + apply (tr_inv (λx, right_inv f0 a ▹ x = h a) (left_inv (f1 _) _)), unfold function.id, apply apd end end diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 3cf7e7db7..39dd02fb8 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -190,33 +190,33 @@ namespace sigma : is_equiv (sigma_functor f g) := adjointify (sigma_functor f g) (sigma_functor f⁻¹ (λ(a' : A') (b' : B' a'), - ((g (f⁻¹ a'))⁻¹ (transport B' (retr f a')⁻¹ b')))) + ((g (f⁻¹ a'))⁻¹ (transport B' (right_inv f a')⁻¹ b')))) begin intro u', cases u' with [a', b'], - apply (sigma_eq (retr f a')), - -- rewrite retr, + apply (sigma_eq (right_inv f a')), + -- rewrite right_inv, -- end - -- "rewrite retr (g (f⁻¹ a'))" - apply concat, apply (ap (λx, (transport B' (retr f a') x))), apply (retr (g (f⁻¹ a'))), - show retr f a' ▹ ((retr f a')⁻¹ ▹ b') = b', - from tr_inv_tr _ (retr f a') b' + -- "rewrite right_inv (g (f⁻¹ a'))" + apply concat, apply (ap (λx, (transport B' (right_inv f a') x))), apply (right_inv (g (f⁻¹ a'))), + show right_inv f a' ▹ ((right_inv f a')⁻¹ ▹ b') = b', + from tr_inv_tr _ (right_inv f a') b' end begin intro u, cases u with [a, b], - apply (sigma_eq (sect f a)), - show transport B (sect f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (retr f (f a))⁻¹ (g a b))) = b, + apply (sigma_eq (left_inv f a)), + show transport B (left_inv f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (right_inv f (f a))⁻¹ (g a b))) = b, from calc - transport B (sect f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (retr f (f a))⁻¹ (g a b))) - = (g a)⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a))⁻¹ (g a b))) - : by rewrite (fn_tr_eq_tr_fn (sect f a) (λ a, (g a)⁻¹)) - ... = (g a)⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a))⁻¹ (g a b))) + transport B (left_inv f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (right_inv f (f a))⁻¹ (g a b))) + = (g a)⁻¹ (transport (B' ∘ f) (left_inv f a) (transport B' (right_inv f (f a))⁻¹ (g a b))) + : by rewrite (fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)) + ... = (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' (right_inv f (f a))⁻¹ (g a b))) : ap (g a)⁻¹ !transport_compose - ... = (g a)⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a))⁻¹ (g a b))) - : ap (λ x, (g a)⁻¹ (transport B' (ap f (sect f a)) (transport B' x⁻¹ (g a b)))) (adj f a) + ... = (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' (ap f (left_inv f a))⁻¹ (g a b))) + : ap (λ x, (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' x⁻¹ (g a b)))) (adj f a) ... = (g a)⁻¹ (g a b) : {!tr_inv_tr} - ... = b : by rewrite (sect (g a) b) + ... = b : by rewrite (left_inv (g a) b) end definition sigma_equiv_sigma_of_is_equiv [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]