From 9b55a90c5e8e3510b3da3ad9d2d1a3b9b63c45dd Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 02:55:44 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter3.lagda.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index da3c098..01af651 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -14,6 +14,13 @@ isSet : (A : Set) → Set
 isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 
+### Example 3.1.1
+
+```
+𝟙-is-Set : isSet 𝟙
+𝟙-is-Set tt tt p q = {!    !}
+```
+
 ## 3.2 Propositions as types?
 
 ## 3.4 Classical vs. intuitionistic logic