From 663827023bfcc94512f3f5637fcde24b4dae3419 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 29 Jun 2024 13:25:09 -0500
Subject: [PATCH] test

---
 src/HottBook/Chapter3.lagda.md | 10 ++++++++++
 src/HottBook/Chapter4.lagda.md | 11 ++++++++++-
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 3a4cf74..36f88bd 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -78,6 +78,16 @@ is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
 ```
 lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
 lemma3∙1∙8 {A} A-set x y p q r s =
+  let g = λ q → A-set x y p q in
+  let
+    what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q'
+    what r =
+      let what3 = apd g r in
+      let what4 = lemma2∙11∙2.i r (g q) in
+      let what5 = {!   !} in
+      sym what4 ∙ what3
+  in
+  -- let what2 = what r in
   {!   !}
 ```
 
diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md
index e1e6d35..17525f8 100644
--- a/src/HottBook/Chapter4.lagda.md
+++ b/src/HottBook/Chapter4.lagda.md
@@ -8,8 +8,17 @@ open import HottBook.Chapter3
 
 ## 4.1 Quasi-inverses
 
+### Lemma 4.1.1
+
 ```
--- qinv : {A B : Type} (f : A → B) → 
+lemma4∙1∙1 : {A B : Set}
+  → (f : A → B)
+  → qinv f
+  → qinv f ≃ ((x : A) → x ≡ x)
+lemma4∙1∙1 f q = {!   !}
+  where
+    ff : qinv f → (x : A) → x ≡ x
+    ff 
 ```
 
 ### Theorem 4.1.3