update ch3+4

.vscode/settings.json

@@ -5,6 +5,6 @@
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
 	"agdaMode.connection.commandLineOptions": "",
 	"search.exclude": {
-		"src/HottBook/**": true
+		"src/CubicalHott/**": true
 	}
 }

src/CubicalHott/Chapter2.lagda.md

@@ -253,26 +253,26 @@ open axiom2∙10∙3
 ### Theorem 2.11.2
 
 ```
-module lemma2∙11∙2 where
+-- module lemma2∙11∙2 where
-  open ≡-Reasoning
+--   open ≡-Reasoning
 
-  i : {l : Level} {A : Type l} {a x1 x2 : A}
+--   i : {l : Level} {A : Type l} {a x1 x2 : A}
-    → (p : x1 ≡ x2)
+--     → (p : x1 ≡ x2)
-    → (q : a ≡ x1)
+--     → (q : a ≡ x1)
-    → transport (λ y → a ≡ y) p q ≡ q ∙ p
+--     → transport (λ y → a ≡ y) p q ≡ q ∙ p
-  i {l} {A} {a} {x1} {x2} p q j = {!   !}
+--   i {l} {A} {a} {x1} {x2} p q j = {!   !}
 
-  ii : {l : Level} {A : Type l} {a x1 x2 : A}
+--   ii : {l : Level} {A : Type l} {a x1 x2 : A}
-    → (p : x1 ≡ x2)
+--     → (p : x1 ≡ x2)
-    → (q : x1 ≡ a)
+--     → (q : x1 ≡ a)
-    → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
+--     → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
-  ii {l} {A} {a} {x1} {x2} p q = {!   !}
+--   ii {l} {A} {a} {x1} {x2} p q = {!   !}
 
-  iii : {l : Level} {A : Type l} {a x1 x2 : A}
+--   iii : {l : Level} {A : Type l} {a x1 x2 : A}
-    → (p : x1 ≡ x2)
+--     → (p : x1 ≡ x2)
-    → (q : x1 ≡ x1)
+--     → (q : x1 ≡ x1)
-    → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
+--     → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
-  iii {l} {A} {a} {x1} {x2} p q = {!   !}
+--   iii {l} {A} {a} {x1} {x2} p q = {!   !}
 ```
 
 ### Remark 2.12.6

src/CubicalHott/Chapter3.lagda.md

@@ -39,6 +39,14 @@ module section3∙7 where
   data ∥_∥ (A : Type) : Type where
     ∣_∣ : (a : A) → ∥ A ∥
     witness : (x y : ∥ A ∥) → x ≡ y
+
+  rec-∥_∥ : (A : Type) → {B : Type} → isProp B → (f : A → B)
+    → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
+  rec-∥ A ∥ {B} BisProp f = g , λ _ → refl
+    where
+      g : ∥ A ∥ → B
+      g ∣ a ∣ = f a
+      g (witness x y i) = BisProp (g x) (g y) i
 open section3∙7
 ```
 
@@ -64,5 +72,8 @@ postulate
 
 ```
 lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
-lemma3∙9∙1 prop = ∣_∣ , {!   !}
+lemma3∙9∙1 {P} prop = ∣_∣ , qinv-to-isequiv (mkQinv inv {!   !} {!   !})
+  where
+    inv : ∥ P ∥ → P
+    inv = {! rec-∥ P ∥  !}
 ```

src/HottBook/Chapter1.lagda.md

@@ -5,7 +5,11 @@
 module HottBook.Chapter1 where
 
 open import Agda.Primitive public
-open import Agda.Primitive.Cubical public
+open import HottBook.CoreUtil
+
+private
+  variable
+    l : Level
 ```
 
 </details>
@@ -21,7 +25,7 @@ open import Agda.Primitive.Cubical public
 ## 1.4 Dependent function types (Π-types)
 
 ```
-id : {l : Level} {A : Set l} → A → A
+id : {A : Set l} → A → A
 id x = x
 ```
 
@@ -94,10 +98,10 @@ rec-+ C f g (inr x) = g x
 ```
 
 ```
-data ⊥ {l : Level} : Set l where
+data ⊥ : Set where
 
-rec-⊥ : {l : Level} → {C : Set l} → (x : ⊥ {l}) → C
+rec-⊥ : {C : Set l} → (x : ⊥) → C
-rec-⊥ {C} ()
+rec-⊥ ()
 ```
 
 ## 1.8 The type of booleans
@@ -131,22 +135,22 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 
 ```
 infix 3 ¬_
-¬_ : ∀ {l : Level} (A : Set l) → Set l
+¬_ : (A : Set l) → Set l
-¬_ {l} A = A → ⊥ {l}
+¬_ A = A → ⊥
 ```
 
 ## 1.12 Identity types
 
 ```
 infix 4 _≡_
-data _≡_ {l} {A : Set l} : (a b : A) → Set l where
+data _≡_ {A : Set l} : (a b : A) → Set l where
   instance refl : {x : A} → x ≡ x
 ```
 
 ### 1.12.3 Disequality
 
 ```
-_≢_ : {A : Set} (x y : A) → Set
+_≢_ : {A : Set l} (x y : A) → Set l
 _≢_ x y = (p : x ≡ y) → ⊥
 ```
 

src/HottBook/Chapter2.lagda.md

@@ -5,9 +5,12 @@
 module HottBook.Chapter2 where
 
 open import Agda.Primitive.Cubical hiding (i1)
-open import HottBook.Chapter1 hiding (i1)
+open import HottBook.Chapter1
 open import HottBook.Chapter2Lemma221 public
-open import HottBook.Util
+
+private
+  variable
+    l : Level
 ```
 
 </details>
@@ -632,7 +635,7 @@ postulate
 ### Lemma 2.9.2
 
 ```
-happly : {A B : Set}
+happly : {A B : Set l}
   → {f g : A → B}
   → (p : f ≡ g)
   → (x : A)
@@ -644,7 +647,7 @@ happly {A} {B} {f} {g} p x = ap (λ h → h x) p
 
 ```
 postulate
-  funext : {l : Level} {A B : Set l}
+  funext : {A B : Set l}
     → {f g : A → B}
     → ((x : A) → f x ≡ g x)
     → f ≡ g
@@ -707,10 +710,11 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
 ### Lemma 2.10.1
 
 ```
-idtoeqv : {l : Level} {A B : Set l}
+idtoeqv : {A B : Set l} → (A ≡ B) → (A ≃ B)
-  → (A ≡ B)
+idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-homotopy)
-  → (A ≃ B)
+  where
-idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A
+    id-homotopy : (id ∘ id) ∼ id
+    id-homotopy x = refl
 ```
 
 ### Axiom 2.10.3 (Univalence)
@@ -726,7 +730,7 @@ module axiom2∙10∙3 where
     backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
     -- backward p = {!   !}
 
-  ua-eqv : {l : Level} {A : Set l} {B : Set l} → (A ≃ B) ≃ (A ≡ B)
+  ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
   ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
 
 open axiom2∙10∙3 hiding (forward; backward)
@@ -847,10 +851,12 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q =
 ### Theorem 2.12.5
 
 ```
-module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
+module theorem2∙12∙5 {A B : Set l} (a₀ : A) where
+  open import HottBook.CoreUtil using (Lift)
+
   code : A + B → Set l
   code (inl a) = a₀ ≡ a
-  code (inr b) = ⊥
+  code (inr b) = Lift ⊥
 
   encode : (x : A + B) → (p : inl a₀ ≡ x) → code x
   encode x p = transport code p refl
@@ -877,15 +883,16 @@ module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
 ### Remark 2.12.6
 
 ```
-remark2∙12∙6 : true ≢ false
+module remark2∙12∙6 where
-remark2∙12∙6 p = genBot tt
+  true≢false : true ≢ false
-  where
+  true≢false p = genBot tt
-    Bmap : 𝟚 → Set
+    where
-    Bmap true = 𝟙
+      Bmap : 𝟚 → Set
-    Bmap false = ⊥
+      Bmap true = 𝟙
+      Bmap false = ⊥
 
-    genBot : 𝟙 → ⊥
+      genBot : 𝟙 → ⊥
-    genBot = transport Bmap p
+      genBot = transport Bmap p
 ```
 
 ## 2.13 Natural numbers

src/HottBook/Chapter2Exercises.lagda.md

@@ -225,21 +225,18 @@ exercise2∙13 = f , equiv
           let p1 = ap h' p in
           let p2 = trans p1 (h-id false) in
           let p3 = trans (sym (h-id true)) p2 in
-          remark2∙12∙6 p3
+          remark2∙12∙6.true≢false p3
-
-        ⊥-elim : {l : Level} {A : Set l} → ⊥ {l} → A
-        ⊥-elim ()
 
         opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b
         opposite-prop {a} {b} p with f' (neg a) | inspect f' (neg a)
-        opposite-prop {true} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q)))
+        opposite-prop {true} {true} p | true | ingraph q = rec-⊥ (f-codomain-is-2 (trans p (sym q)))
         opposite-prop {true} {true} p | false | _ = refl
         opposite-prop {true} {false} p | true | _ = refl
-        opposite-prop {true} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q)))
+        opposite-prop {true} {false} p | false | ingraph q = rec-⊥ (f-codomain-is-2 (trans p (sym q)))
-        opposite-prop {false} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
+        opposite-prop {false} {true} p | true | ingraph q = rec-⊥ (f-codomain-is-2 (trans q (sym p)))
         opposite-prop {false} {true} p | false | ingraph q = refl
         opposite-prop {false} {false} p | true | ingraph q = refl
-        opposite-prop {false} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
+        opposite-prop {false} {false} p | false | ingraph q = rec-⊥ (f-codomain-is-2 (trans q (sym p)))
 
         f-is-id' : (f' true ≡ true) → (b : 𝟚) → f' b ≡ id b
         f-is-id' p true = p

src/HottBook/Chapter3.lagda.md

@@ -10,7 +10,12 @@ open import HottBook.Chapter1Util
 open import HottBook.Chapter2
 open import HottBook.Chapter3Definition331 public
 open import HottBook.Chapter3Lemma333 public
+open import HottBook.CoreUtil
 open import HottBook.Util
+
+private
+  variable
+    l : Level
 ```
 
 </details>
@@ -20,7 +25,7 @@ open import HottBook.Util
 ### Definition 3.1.1
 
 ```
-isSet : {l : Level} (A : Set l) → Set l
+isSet : (A : Set l) → Set l
 isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 
@@ -34,7 +39,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.3
 
 ```
-⊥-is-Set : ∀ {l} → isSet (⊥ {l})
+⊥-is-Set : isSet ⊥
 ⊥-is-Set () () p q
 ```
 
@@ -76,19 +81,19 @@ is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
 ### Lemma 3.1.8
 
 ```
-lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
+-- lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
-lemma3∙1∙8 {A} A-set x y p q r s =
+-- lemma3∙1∙8 {A} A-set x y p q r s =
-  let g = λ q → A-set x y p q in
+--   let g = λ q → A-set x y p q in
-  let
+--   let
-    what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q'
+--     what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q'
-    what r =
+--     what r =
-      let what3 = apd g r in
+--       let what3 = apd g r in
-      let what4 = lemma2∙11∙2.i r (g q) in
+--       let what4 = lemma2∙11∙2.i r (g q) in
-      let what5 = {!   !} in
+--       let what5 = {!   !} in
-      sym what4 ∙ what3
+--       sym what4 ∙ what3
-  in
+--   in
-  -- let what2 = what r in
+--   -- let what2 = what r in
-  {!   !}
+--   {!   !}
 ```
 
 ### Example 3.1.9
@@ -125,56 +130,83 @@ lemma3∙1∙8 {A} A-set x y p q r s =
 TODO: Study this more
 
 ```
-postulate
+theorem3∙2∙2 : ((A : Set l) → ¬ ¬ A → A) → ⊥
-  theorem3∙2∙2 : {l : Level} → ((A : Set l) → ¬ ¬ A → A) → ⊥ {l}
+theorem3∙2∙2 double-neg = conclusion
--- theorem3∙2∙2 f = let wtf = f 𝟚 in {!   !}
+  where
---   where
+    open axiom2∙10∙3
---     open axiom2∙10∙3
 
---     p : 𝟚 ≡ 𝟚
+    bool = Lift 𝟚
---     p = ua neg-equiv
 
---     wtf : ¬ ¬ 𝟚 → 𝟚
+    negl : bool → bool
---     wtf = f 𝟚
+    negl (lift true) = lift false
+    negl (lift false) = lift true
 
---     wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
+    negl-homotopy : (negl ∘ negl) ∼ id
---     wtf2 = apd f p
+    negl-homotopy (lift true) = refl
+    negl-homotopy (lift false) = refl
 
---     wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
+    e : bool ≃ bool
---     wtf3 u = happly wtf2 u
+    e = negl , qinv-to-isequiv (mkQinv negl negl-homotopy negl-homotopy)
 
---     wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
+    p : bool ≡ bool
---     wtf4 u = 
+    p = ua e
---       let
---         wtf5 : 
---           let A = λ A → ¬ ¬ A in
---           let B = id in
---           transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x))
---         wtf5 = equation2∙9∙4 (f 𝟚) p
---       in
---       happly wtf5 u
 
---     wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
+    fbool : ¬ ¬ bool → bool
---     wtf6 u v = funext (λ x → rec-⊥ (u x))
+    fbool = double-neg bool
 
---     wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
+    apdfp : transport (λ A → ¬ ¬ A → A) p fbool ≡ fbool
---     wtf7 u = {!   !}
+    apdfp = apd double-neg p
 
---     wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
+    u : ¬ ¬ bool
---     wtf8 u = {!  sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
+    u = λ p → p (lift true)
 
---     wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
+    foranyu : transport (λ A → ¬ ¬ A → A) p fbool u ≡ fbool u
---     wtf9 = {!   !}
+    foranyu = happly apdfp u
 
---     wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
+    what : transport (λ A → ¬ (¬ A) → A) p fbool u ≡ transport (λ X → X) p (fbool (transport (λ X → ¬ (¬ X)) (sym p) u))
---     wtf10 true p = remark2∙12∙6 (sym p)
+    what =
---     wtf10 false p = remark2∙12∙6 p
+      let
+        x = equation2∙9∙4 {A = λ X → ¬ ¬ X} {B = λ X → X} fbool p
+        in ap (λ f → f u) x
 
---     wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
+    allsame : (u v : ¬ ¬ bool) → (x : ¬ bool) → u x ≡ v x
---     wtf11 u = wtf10 (f 𝟚 u)
+    allsame u v x = rec-⊥ (u x)
 
---     wtf12 : (u : ¬ ¬ 𝟚) → ⊥
+    postulate
---     wtf12 u = wtf11 u (wtf9 u)
+      allsamef : (u v : ¬ ¬ bool) → u ≡ v
+
+    all-dn-u-same : transport (λ A → ¬ ¬ A) (sym p) u ≡ u
+    all-dn-u-same = allsamef (transport (λ A → ¬ ¬ A) (sym p) u) u
+
+    nextStep : transport (λ A → A) p (fbool u) ≡ fbool u
+    nextStep =
+      let x = ap (λ x → transport id p (fbool x)) all-dn-u-same in
+      let y = what ∙ x in
+      sym y ∙ foranyu
+
+    -- postulate
+    huhh : (Σ.fst e) (fbool u) ≡ fbool u
+    huhh =
+      let
+        equiv1 = ap ua (axiom2∙10∙3.forward e)
+
+        x : {A B : Set l} → (e : A ≃ B) → (a : A) → transport id (ua e) a ≡ Σ.fst e a
+        x e a = 
+          {!  axiom2∙10∙3.forward ? !}
+      in
+      {!   !}
+    --   sym (x e (fbool u)) ∙ nextStep
+
+    finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x)
+    finalStep (lift true) p = 
+      let wtf = ap (λ f → Lift.lower f) p in
+      remark2∙12∙6.true≢false (sym wtf)
+    finalStep (lift false) p =
+      let wtf = ap (λ f → Lift.lower f) p in
+      remark2∙12∙6.true≢false wtf
+
+    conclusion : ⊥
+    conclusion = finalStep (fbool u) huhh
 ```
 
 ### Corollary 3.2.7
@@ -244,6 +276,39 @@ module definition3∙4∙3 where
 
 ```
 module section3∙7 where
-  data ∥_∥ (A : Set) : Set where
+  postulate
-    ∣_∣ : (a : A) → ∥ A ∥
+    ∥_∥ : Set → Set
+    ∣_∣ : {A : Set} → (a : A) → ∥ A ∥
+    witness : {A : Set} → (x y : ∥ A ∥) → x ≡ y → Set
+    rec-∥_∥ : (A : Set) → {B : Set} → isProp B → (f : A → B)
+      → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
+open section3∙7
+```
+
+### Definition 3.7.1
+
+## 3.9 The principle of unique choice
+
+### Lemma 3.9.1
+
+```
+lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
+lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
+  where
+    thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ id a)
+    thing = rec-∥ P ∥ prop id
+
+    g = Σ.fst thing
+    g-prop = Σ.snd thing
+
+    prop2 : isProp ∥ P ∥
+    prop2 x y = 
+      let a = g-prop (g x) in
+      let b = g-prop (g y) in
+      let eqProp = prop (g x) (g y) in
+      let 
+        concat : g (∣ g x ∣) ≡ g (∣ g y ∣)
+        concat = a ∙ eqProp ∙ (sym b)
+      in
+      {!  prop ?  !}
 ```

src/HottBook/Chapter3Definition331.lagda.md

@@ -3,6 +3,10 @@ module HottBook.Chapter3Definition331 where
 
 open import Agda.Primitive
 open import HottBook.Chapter1
+
+private
+  variable
+    l : Level
 ```
 
 ## Definition 3.3.1
@@ -10,7 +14,7 @@ open import HottBook.Chapter1
 [//]: <> (ANCHOR: isProp)
 
 ```
-isProp : (P : Set) → Set
+isProp : (P : Set l) → Set l
 isProp P = (x y : P) → x ≡ y
 ```
 

src/HottBook/Chapter4.lagda.md

@@ -4,6 +4,20 @@ module HottBook.Chapter4 where
 open import HottBook.Chapter1
 open import HottBook.Chapter2
 open import HottBook.Chapter3
+
+private
+  variable
+    l : Level
+```
+
+# Chapter 4 Equivalences
+
+```
+record satisfies-equivalence-properties {A B : Set} {f : A → B} (isequiv : (A → B) → Set) : Set where
+  field
+    qinv→isequiv : qinv f → isequiv f
+    isequiv→qinv : isequiv f → qinv f
+    isequiv-isProp : isProp (isequiv f)
 ```
 
 ## 4.1 Quasi-inverses
@@ -11,14 +25,32 @@ open import HottBook.Chapter3
 ### Lemma 4.1.1
 
 ```
-lemma4∙1∙1 : {A B : Set}
+lemma4∙1∙1 : {A B : Set} → (f : A → B) → qinv f → qinv f ≃ ((x : A) → x ≡ x)
-  → (f : A → B)
+lemma4∙1∙1 {A} f q = {!   !}
-  → qinv f
-  → qinv f ≃ ((x : A) → x ≡ x)
-lemma4∙1∙1 f q = {!   !}
   where
     ff : qinv f → (x : A) → x ≡ x
-    ff 
+    ff = {!   !}
+```
+
+### Lemma 4.1.2
+
+```
+open section3∙7
+lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a)
+  → isSet (a ≡ a)
+  → ((x : A) → ∥ a ≡ x ∥)
+  → ((p : a ≡ a) → p ∙ q ≡ q ∙ p)
+  → Σ ((x : A) → x ≡ x) (λ f → f a ≡ q)
+lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {!   !}) , {!   !}
+  where
+    allsets : (x y : A) → isSet (x ≡ y)
+    allsets x .x refl refl refl refl = refl
+
+    B : (x : A) → Set
+    B x = Σ (x ≡ x) (λ r → (s : a ≡ x) → r ≡ (sym s) ∙ q ∙ s)
+
+    BisProp : (a : A) → isProp (B a)
+    BisProp a x y = {!   !}
 ```
 
 ### Theorem 4.1.3
@@ -26,8 +58,72 @@ lemma4∙1∙1 f q = {!   !}
 There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition.
 
 ```
-theorem4∙1∙3 : {A B : Set}
+theorem4∙1∙3 : ∀ {l} {A B : Set l}
-  → (f : A → B)
+  → Σ (A → B) (λ f → isProp (qinv f) → ⊥)
-  → isProp (qinv f) → ⊥
+theorem4∙1∙3 = {! !} , {!   !}
-theorem4∙1∙3 f p = {!   !}
+  where
+    goal : Σ (Set (lsuc l)) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
+
+```
+
+## 4.2 Half adjoint equivalences
+
+### Definition 4.2.1
+
+```
+record ishae {A B : Set} (f : A → B) : Set where
+  constructor mkIshae
+  field
+    g : B → A
+    η : (g ∘ f) ∼ id
+    ε : (f ∘ g) ∼ id
+    τ : (x : A) → ap f (η x) ≡ ε (f x)
+```
+
+### Lemma 4.2.2
+
+### Theorem 4.2.3
+
+```
+theorem4∙2∙3 : {A B : Set} (f : A → B) → qinv f → ishae f
+theorem4∙2∙3 {A} {B} f (mkQinv g ε η) = mkIshae g' η' ε' τ
+  where
+    g' : B → A
+    g' = g
+
+    η' : (g' ∘ f) ∼ id
+    η' = η
+
+    ε' : (f ∘ g') ∼ id
+    ε' x = {!   !}
+
+    τ : (x : A) → ap f (η' x) ≡ ε' (f x)
+    τ x = {!   !}
+```
+
+### Definition 4.2.7
+
+```
+module definition4∙2∙7 where
+  linv : ∀ {A B} (f : A → B) → Set
+  linv {A} {B} f = Σ (B → A) (λ g → (g ∘ f) ∼ id)
+
+  rinv : ∀ {A B} (f : A → B) → Set
+  rinv {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ∼ id)
+```
+
+### Definition 4.2.10
+
+```
+module definition4∙2∙10 where
+  open definition4∙2∙7
+
+  lcoh : ∀ {A} {B} → (f : A → B) → linv f → rinv f → Set
+  -- lcoh f (g , η) (g , ε) = ?
+```
+
+### Theorem 4.2.13
+
+```
+theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)
 ```

src/HottBook/CoreUtil.agda

@@ -0,0 +1,7 @@
+module HottBook.CoreUtil where
+
+open import Agda.Primitive
+
+record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
+  constructor lift
+  field lower : A