Complete equivalence-trans

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

@@ -404,13 +404,51 @@ which are discussed in Sections [2.6](06-cartesian-product-types.rzk.md) and [2.
 ### Transitivity
 
 ```rzk
--- #def equivalence-trans
---     (A B C : U)
---     : equivalence A B → equivalence B C → equivalence A C
---     := \ (f, isequiv-f) (g, isequiv-g) →
+#define qinv-trans
+  ( A B C : U)
+  ( f : A → B)
+  ( g : B → C)
+  : qinv A B f → qinv B C g → qinv A C (compose A B C g f)
+  :=
+  \ (f⁻¹ , (α-f , β-f)) (g⁻¹ , (α-g , β-g)) →
+    ( compose C B A f⁻¹ g⁻¹
+    , ( \ c →
+          path-concat 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)
+          ( ap B A f⁻¹
+            ( g⁻¹ (g (f a)))
+            ( f a)
+            ( β-g (f a)))
+          ( β-f a)))
+
+#define equivalence-trans
+  ( A B C : U)
+  : equivalence A B
+  → equivalence B C
+  → equivalence A C
+  :=
+  \ (f , isequiv-f) (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
 
 ``` title="Proof for corollary 2.4.4. Homotopy with id"
 lemma 2.4.3 :  H(x) • g  (p)   = f (p)   • H y