update ch3+4

src/CubicalHott/Chapter2.lagda.md

@@ -253,26 +253,26 @@ open axiom2∙10∙3
 ### Theorem 2.11.2
 
 ```
-module lemma2∙11∙2 where
-  open ≡-Reasoning
+-- module lemma2∙11∙2 where
+--   open ≡-Reasoning
 
-  i : {l : Level} {A : Type l} {a x1 x2 : A}
-    → (p : x1 ≡ x2)
-    → (q : a ≡ x1)
-    → transport (λ y → a ≡ y) p q ≡ q ∙ p
-  i {l} {A} {a} {x1} {x2} p q j = {!   !}
+--   i : {l : Level} {A : Type l} {a x1 x2 : A}
+--     → (p : x1 ≡ x2)
+--     → (q : a ≡ x1)
+--     → transport (λ y → a ≡ y) p q ≡ q ∙ p
+--   i {l} {A} {a} {x1} {x2} p q j = {!   !}
 
-  ii : {l : Level} {A : Type l} {a x1 x2 : A}
-    → (p : x1 ≡ x2)
-    → (q : x1 ≡ a)
-    → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
-  ii {l} {A} {a} {x1} {x2} p q = {!   !}
+--   ii : {l : Level} {A : Type l} {a x1 x2 : A}
+--     → (p : x1 ≡ x2)
+--     → (q : x1 ≡ a)
+--     → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
+--   ii {l} {A} {a} {x1} {x2} p q = {!   !}
 
-  iii : {l : Level} {A : Type l} {a x1 x2 : A}
-    → (p : x1 ≡ x2)
-    → (q : x1 ≡ x1)
-    → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
-  iii {l} {A} {a} {x1} {x2} p q = {!   !}
+--   iii : {l : Level} {A : Type l} {a x1 x2 : A}
+--     → (p : x1 ≡ x2)
+--     → (q : x1 ≡ x1)
+--     → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
+--   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/Chapter3.lagda.md

@@ -81,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} 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
-  {!   !}
+-- 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
+--   {!   !}
 ```
 
 ### Example 3.1.9
@@ -184,6 +184,7 @@ theorem3∙2∙2 double-neg = conclusion
       let y = what ∙ x in
       sym y ∙ foranyu
 
+    -- postulate
     huhh : (Σ.fst e) (fbool u) ≡ fbool u
     huhh =
       let
@@ -193,7 +194,8 @@ theorem3∙2∙2 double-neg = conclusion
         x e a = 
           {!  axiom2∙10∙3.forward ? !}
       in
-      sym (x e (fbool u)) ∙ nextStep
+      {!   !}
+    --   sym (x e (fbool u)) ∙ nextStep
 
     finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x)
     finalStep (lift true) p = 
@@ -274,6 +276,39 @@ module definition3∙4∙3 where
 
 ```
 module section3∙7 where
-  data ∥_∥ (A : Set) : Set where
-    ∣_∣ : (a : A) → ∥ A ∥
+  postulate
+    ∥_∥ : 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}
-  → (f : A → B)
-  → qinv f
-  → qinv f ≃ ((x : A) → x ≡ x)
-lemma4∙1∙1 f q = {!   !}
+lemma4∙1∙1 : {A B : Set} → (f : A → B) → qinv f → qinv f ≃ ((x : A) → x ≡ x)
+lemma4∙1∙1 {A} 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}
-  → (f : A → B)
-  → isProp (qinv f) → ⊥
-theorem4∙1∙3 f p = {!   !}
+theorem4∙1∙3 : ∀ {l} {A B : Set l}
+  → Σ (A → B) (λ f → isProp (qinv f) → ⊥)
+theorem4∙1∙3 = {! !} , {!   !}
+  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)
 ```