a

.vscode/settings.json

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

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} ()
+rec-⊥ : {C : Set l} → (x : ⊥) → 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
-¬_ {l} A = A → ⊥ {l}
+¬_ : (A : Set l) → Set 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}
-  → (A ≡ B)
-  → (A ≃ B)
-idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A
+idtoeqv : {A B : Set l} → (A ≡ B) → (A ≃ B)
+idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-homotopy)
+  where
+    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
-remark2∙12∙6 p = genBot tt
-  where
-    Bmap : 𝟚 → Set
-    Bmap true = 𝟙
-    Bmap false = ⊥
+module remark2∙12∙6 where
+  true≢false : true ≢ false
+  true≢false p = genBot tt
+    where
+      Bmap : 𝟚 → Set
+      Bmap true = 𝟙
+      Bmap false = ⊥
 
-    genBot : 𝟙 → ⊥
-    genBot = transport Bmap p
+      genBot : 𝟙 → ⊥
+      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
-
-        ⊥-elim : {l : Level} {A : Set l} → ⊥ {l} → A
-        ⊥-elim ()
+          remark2∙12∙6.true≢false p3
 
         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 {false} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
+        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 = 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
 ```
 
@@ -125,56 +130,81 @@ lemma3∙1∙8 {A} A-set x y p q r s =
 TODO: Study this more
 
 ```
-postulate
-  theorem3∙2∙2 : {l : Level} → ((A : Set l) → ¬ ¬ A → A) → ⊥ {l}
--- theorem3∙2∙2 f = let wtf = f 𝟚 in {!   !}
---   where
---     open axiom2∙10∙3
+theorem3∙2∙2 : ((A : Set l) → ¬ ¬ A → A) → ⊥
+theorem3∙2∙2 double-neg = conclusion
+  where
+    open axiom2∙10∙3
 
---     p : 𝟚 ≡ 𝟚
---     p = ua neg-equiv
+    bool = Lift 𝟚
 
---     wtf : ¬ ¬ 𝟚 → 𝟚
---     wtf = f 𝟚
+    negl : bool → bool
+    negl (lift true) = lift false
+    negl (lift false) = lift true
 
---     wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
---     wtf2 = apd f p
+    negl-homotopy : (negl ∘ negl) ∼ id
+    negl-homotopy (lift true) = refl
+    negl-homotopy (lift false) = refl
 
---     wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
---     wtf3 u = happly wtf2 u
+    e : bool ≃ bool
+    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))
---     wtf4 u = 
---       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
+    p : bool ≡ bool
+    p = ua e
 
---     wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
---     wtf6 u v = funext (λ x → rec-⊥ (u x))
+    fbool : ¬ ¬ bool → bool
+    fbool = double-neg bool
 
---     wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
---     wtf7 u = {!   !}
+    apdfp : transport (λ A → ¬ ¬ A → A) p fbool ≡ fbool
+    apdfp = apd double-neg p
 
---     wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
---     wtf8 u = {!  sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
+    u : ¬ ¬ bool
+    u = λ p → p (lift true)
 
---     wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
---     wtf9 = {!   !}
+    foranyu : transport (λ A → ¬ ¬ A → A) p fbool u ≡ fbool u
+    foranyu = happly apdfp u
 
---     wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
---     wtf10 true p = remark2∙12∙6 (sym p)
---     wtf10 false p = remark2∙12∙6 p
+    what : transport (λ A → ¬ (¬ A) → A) p fbool u ≡ transport (λ X → X) p (fbool (transport (λ X → ¬ (¬ X)) (sym p) u))
+    what =
+      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))
---     wtf11 u = wtf10 (f 𝟚 u)
+    allsame : (u v : ¬ ¬ bool) → (x : ¬ bool) → u x ≡ v x
+    allsame u v x = rec-⊥ (u x)
 
---     wtf12 : (u : ¬ ¬ 𝟚) → ⊥
---     wtf12 u = wtf11 u (wtf9 u)
+    postulate
+      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
+
+    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

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