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

---
 src/HottBook/Chapter3.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 5daed49..263c259 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -18,7 +18,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 
 ```
 𝟙-is-Set : isSet 𝟙
-𝟙-is-Set tt tt p q = {!    !}
+𝟙-is-Set tt tt p q = J (λ x y p' → p' ≡ q) (λ x → {!   !}) tt tt p
 ```
 
 ### Example 3.1.3