test

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
   {!   !}
 ```
 

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