From 1dd217f750efde7ba143713cd6c5612b069745fa Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 8 May 2024 19:14:30 -0500
Subject: [PATCH] 2.15.2

---
 src/HottBook/Chapter2.lagda.md | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 19c426a..d6a3eab 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/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)
+``` 
\ No newline at end of file