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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 2b98fc7..46cb581 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -259,28 +259,8 @@ A ≃ B = Σ[ f ∈ (A → B) ] isequiv f
 ### Theorem 2.8.1
 
 ```
--- open import Function.HalfAdjointEquivalence
--- _is-⋆ : (x : 𝟙) → x ≡ ⋆
--- ⋆ is-⋆ = refl
---
--- theorem281-helper2 : {x : 𝟙} → (p : x ≡ x) → p ≡ refl
--- theorem281-helper2 {x} p =
---   let a = sym (x is-⋆) ∙ p ∙ (x is-⋆) in
---   J (λ the what → p ≡ the) ? ?
---
--- theorem281-helper : {x y : 𝟙} → (p : x ≡ y) → (x is-⋆) ∙ sym (y is-⋆) ≡ p
--- theorem281-helper {x} p =
---   J (λ the what → (x is-⋆) ∙ sym (the is-⋆) ≡ what) p (theorem281-helper2 _)
---
--- theorem281 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙
--- theorem281 x y = record
---   { to = λ _ → ⋆
---   ; from = λ _ → (x is-⋆) ∙ sym (y is-⋆)
---   ; left-inverse-of = theorem281-helper
---   -- λ z → J (λ the what → (x is-⋆) ∙ sym (the is-⋆) ≡ what) z ?
---   ; right-inverse-of = λ z → sym (z is-⋆)
---   ; left-right = ?
---   }
+theorem2∙8∙1 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙
+theorem2∙8∙1 = {!   !}
 ```
 
 ## 2.9 Π-types and the function extensionality axiom