Complete equivalence-trans

src/1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk.md

@@ -403,7 +403,7 @@ which are discussed in Sections [2.6](06-cartesian-product-types.rzk.md) and [2.
 
 ### Transitivity
 
-```
+```rzk
 #define qinv-trans
   ( A B C : U)
   ( f : A → B)
@@ -426,36 +426,26 @@ which are discussed in Sections [2.6](06-cartesian-product-types.rzk.md) and [2.
           path-concat A
           ( f⁻¹ (g⁻¹ (g (f a))))
           ( f⁻¹ (f a))
-          (a)
+          ( a)
           ( ap B A f⁻¹
-            (g⁻¹ (g (f a)))
-            (f a)
-            ( α-f (g⁻¹ c)))
-          ( α-g c)))
+            ( g⁻¹ (g (f a)))
+            ( f a)
+            ( β-g (f a)))
+          ( β-f a)))
 
-#def equivalence-trans
+#define equivalence-trans
   ( A B C : U)
-  : equivalence A B → equivalence B C → equivalence A C
+  : equivalence A B
+  → equivalence B C
+  → equivalence A C
   :=
   \ (f , isequiv-f) (g , isequiv-g) →
-    ( \ ((f⁻¹ , (α-f , β-f)) : (qinv A B f)) ((g⁻¹ , (α-g , β-g)) : (qinv B C g)) →
-        ( compose A B C g f
-        , qinv-to-isequiv A C (compose A B C g f)
-            ( compose C B A f⁻¹ g⁻¹
-            , ( \ c → path-concat C -- g f f⁻¹ g⁻¹ c = g g⁻¹ c = c
-                ( g (f (f⁻¹ (g⁻¹ (c)))))
-                ( g (g⁻¹ (c)))
-                ( c)
-                ( ap B C g (f (f⁻¹ (g⁻¹ (c)))) (g⁻¹ (c)) (α-f (g⁻¹ (c))))
-                ( α-g c)
-              , \ a → path-concat A -- f⁻¹ g⁻¹ g f a = f⁻¹ f a = a
-                ( f⁻¹ (g⁻¹ (g (f (a)))))
-                ( f⁻¹ (f (a)))
-                ( a)
-                ( ap B A f⁻¹ (g⁻¹ (g (f (a)))) (f (a)) (β-g (f (a))))
-                ( β-f a)))))
-  ( isequiv-to-qinv A B f isequiv-f)
-  ( isequiv-to-qinv B C g isequiv-g)
+    ( compose A B C g f
+    , qinv-to-isequiv A C
+      ( compose A B C g f)
+      ( qinv-trans A B C f g
+        ( isequiv-to-qinv A B f isequiv-f)
+        ( isequiv-to-qinv B C g isequiv-g)))
 ```
 
 ## Proof of Corollary 2.4.4