From d48ae4c0c859f29672a0b98f2e60b9015fa31fb8 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 03:34:11 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2.lagda.md | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 46cb581..ad638ff 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -260,7 +260,27 @@ A ≃ B = Σ[ f ∈ (A → B) ] isequiv f
 
 ```
 theorem2∙8∙1 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙
-theorem2∙8∙1 = {!   !}
+theorem2∙8∙1 x y = func x y , equiv x y
+  where
+    func : (x y : 𝟙) → (x ≡ y) → 𝟙
+    func x y _ = tt
+
+    rev : (x y : 𝟙) → 𝟙 → (x ≡ y)
+    rev tt tt _ = refl
+
+    forward : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id
+    forward tt tt refl = refl
+
+    backward : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id
+    backward tt tt tt = refl
+
+    equiv : (x y : 𝟙) → isequiv (func x y)
+    equiv x y = record
+      { g = rev x y
+      ; g-id = forward x y
+      ; h = rev x y
+      ; h-id = backward x y
+      }
 ```
 
 ## 2.9 Π-types and the function extensionality axiom
@@ -373,7 +393,7 @@ theorem2∙13∙1 m n = encode m n , equiv
         c (suc x) = ap (λ p → ap suc p) (c x)
 
     backward : (m n : ℕ) → (c : code m n) → (decode m n ∘ encode m n) c ≡ id c
-    backward zero zero c = {! refl  !}
+    backward zero zero c = {!   !}
     backward (suc m) (suc n) c = {!   !}
 
     equiv = record