2.15.2

src/HottBook/Chapter2.lagda.md

@@ -460,7 +460,7 @@ theorem2∙13∙1 m n = encode m n , equiv
 
         -- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c
         res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c
-        res = {!    !}
+        res =     
 
       in res
 
@@ -471,3 +471,24 @@ theorem2∙13∙1 m n = encode m n , equiv
       ; h-id = backward m n
       }
 ```
+
+## 2.15 Universal properties
+
+Definition 2.15.1
+
+```
+definition2∙15∙1 : {X A B : Set}
+  → (X → A × B)
+  → (X → A) × (X → B)
+definition2∙15∙1 f = Σ.fst ∘ f , Σ.snd ∘ f
+```
+
+### Theorem 2.15.2
+
+```
+theorem2∙15∙2 : {X A B : Set} → isequiv (definition2∙15∙1 {X} {A} {B})
+theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
+  where
+    g : (X → A) × (X → B) → (X → A × B)
+    g (f1 , f2) = λ x → (f1 x , f2 x)
+```