wip

.vscode/settings.json

@@ -3,7 +3,7 @@
 	"gitdoc.enabled": false,
 	"gitdoc.autoCommitDelay": 300000,
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
-	"agdaMode.connection.commandLineOptions": "--rewriting",
+	"agdaMode.connection.commandLineOptions": "--rewriting --without-K",
 	"search.exclude": {
 		"src/CubicalHott/**": true
 	}

src/HottBook/Chapter1.lagda.md

@@ -66,7 +66,7 @@ record Σ {l₁ l₂} (A : Set l₁) (B : A → Set l₂) : Set (l₁ ⊔ l₂)
   field
     fst : A
     snd : B fst
-open Σ
+open Σ public
 {-# BUILTIN SIGMA Σ #-}
 syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
 
@@ -145,6 +145,7 @@ infix 3 ¬_
 infix 4 _≡_
 data _≡_ {A : Set l} : (a b : A) → Set l where
   instance refl : {x : A} → x ≡ x
+{-# BUILTIN EQUALITY _≡_ #-}
 {-# BUILTIN REWRITE _≡_ #-}
 ```
 

src/HottBook/Chapter2.lagda.md

@@ -486,7 +486,7 @@ module lemma2∙4∙12 where
 ### Definition 2.6.1
 
 ```
-definition2∙6∙1 : {A B : Set} {x y : A × B}
+definition2∙6∙1 : {A B : Set l} {x y : A × B}
   → (p : x ≡ y)
   → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y)
 definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p
@@ -496,11 +496,11 @@ definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p
 
 ```
 module theorem2∙6∙2 where
-  pair-≡ : {A B : Set} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y
+  pair-≡ : {A B : Set l} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y
   pair-≡ (refl , refl) = refl
 
-  theorem2∙6∙2 : {A B : Set} {x y : A × B}
-    → isequiv (definition2∙6∙1 {A} {B} {x} {y})
+  theorem2∙6∙2 : {A B : Set l} {x y : A × B}
+    → isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})
   theorem2∙6∙2 {A} {B} {x} {y} = qinv-to-isequiv (mkQinv pair-≡ backward forward)
     where
       backward : (definition2∙6∙1 ∘ pair-≡) ∼ id
@@ -508,6 +508,9 @@ module theorem2∙6∙2 where
 
       forward : (pair-≡ ∘ definition2∙6∙1) ∼ id
       forward refl = refl
+
+  pair-≃ : {A B : Set l} {x y : A × B} → (x ≡ y) ≃ ((fst x ≡ fst y) × (snd x ≡ snd y))
+  pair-≃ = definition2∙6∙1 , theorem2∙6∙2
 open theorem2∙6∙2 using (pair-≡)
 ```
 
@@ -808,7 +811,12 @@ module lemma2∙11∙2 where
     → (p : x1 ≡ x2)
     → (q : x1 ≡ x1)
     → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
-  iii {l} {A} {a} {x1} {x2} refl refl = refl
+  iii refl q =
+    let
+      a = i1 q
+      b = i2 q
+    in b ∙ ap (refl ∙_) a
+    where open lemma2∙1∙4
 ```
 
 ### Theorem 2.11.3

src/HottBook/Chapter3.lagda.md

@@ -35,6 +35,11 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 𝟙-is-Set : isSet 𝟙
 𝟙-is-Set tt tt refl refl = refl
+
+𝟙-isProp : isProp 𝟙
+𝟙-isProp x y = 
+  let (_ , equiv) = theorem2∙8∙1 x y in
+  isequiv.g equiv tt
 ```
 
 ### Example 3.1.3
@@ -48,17 +53,55 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 
 ```
 ℕ-is-Set : isSet ℕ
-ℕ-is-Set zero zero refl refl = refl
-ℕ-is-Set (suc x) (suc y) refl refl = refl
+ℕ-is-Set x y p q = wtf4
+  where
+    open theorem2∙13∙1
+    open axiom2∙10∙3
+    open isequiv
+
+    cp = encode x y p
+    cq = encode x y q
+
+    wtf : (x y : ℕ) → (p q : code x y) → p ≡ q
+    wtf zero zero p q = 𝟙-isProp p q
+    wtf (suc x) (suc y) p q = wtf x y p q
+
+    wtf2 : (x y : ℕ) → (p q : code x y) → (p ≡ q) → (decode x y p) ≡ (decode x y q)
+    wtf2 x y p q r = ap (decode x y) r
+
+    wtf3 : {x y : ℕ} → (p : x ≡ y) → (p ≡ decode x y (encode x y p))
+    wtf3 {x} {y} p = sym (theorem2∙13∙1 x y .snd .h-id p)
+
+    wtf4 : p ≡ q
+    wtf4 = (wtf3 p) ∙ wtf2 x y cp cq (wtf x y cp cq) ∙ sym (wtf3 q)
 ```
 
 ### Example 3.1.5
 
-TODO: DO this without path induction
-
 ```
-×-Set : {A B : Set} → isSet A → isSet B → isSet (A × B)
-×-Set {A} {B} A-set B-set (xa , xb) (ya , yb) refl refl = refl
+×-Set : {A B : Set l} → isSet A → isSet B → isSet (A × B)
+×-Set {A = A} {B = B} A-set B-set (xa , xb) (ya , yb) p q = goal
+  where
+    open theorem2∙6∙2
+    open axiom2∙10∙3
+
+    p' : (xa ≡ ya) × (xb ≡ yb)
+    p' = definition2∙6∙1 p
+
+    q' : (xa ≡ ya) × (xb ≡ yb)
+    q' = definition2∙6∙1 q
+
+    lol : {A B : Set l} {x y : A × B} → (x ≡ y) ≡ ((fst x ≡ fst y) × (snd x ≡ snd y))
+    lol = ua pair-≃
+
+    convert : (p : (xa , xb) ≡ (ya , yb)) → (xa ≡ ya) × (xb ≡ yb)
+    convert p = definition2∙6∙1 p
+
+    goal : p ≡ q -- (p : (xa, xb)≡(ya, yb)) (q : (xa, xb)≡(ya, yb))
+                 -- (p': xa≡ya × xb≡yb)
+
+    goal2 = p' ≡ q'
+    goal = {! ap (λ z → ?) goal2  !}
 ```
 
 ### Example 3.1.6
@@ -262,12 +305,6 @@ lemma3∙3∙2 : {P : Set}
   → (x0 : P)
   → P ≃ 𝟙
 lemma3∙3∙2 {P} pp x0 =
-  let
-    𝟙-isProp : isProp 𝟙
-    𝟙-isProp x y = 
-      let (_ , equiv) = theorem2∙8∙1 x y in
-      isequiv.g equiv tt
-  in
   lemma3∙3∙3 pp 𝟙-isProp (λ _ → tt) (λ _ → x0)
 ```
 
@@ -639,7 +676,7 @@ module lemma3∙11∙9 where
       forward p = y (sym (aContr a))
         where
           y : (q : a ≡ a) → transport P q p ≡ p
-          y refl = refl
+          y q = {!   !}
 
 
       backward : (g ∘ f) ∼ id

src/HottBook/Chapter6.lagda.md

@@ -7,6 +7,7 @@ module HottBook.Chapter6 where
 open import HottBook.Chapter1
 open import HottBook.Chapter2
 open import HottBook.Chapter3
+open import HottBook.CoreUtil
 
 private
   variable
@@ -22,7 +23,7 @@ Using the approach from here: https://github.com/HoTT/HoTT-Agda/blob/master/old/
 ## 6.2 Induction principles and dependent paths
 
 ```
-dep-path : {A : Set} {x y : A} → (P : A → Set) → (p : x ≡ y) → (u : P x) → (v : P y) → Set
+dep-path : {l l2 : Level} {A : Set l} {x y : A} → (P : A → Set l2) → (p : x ≡ y) → (u : P x) → (v : P y) → Set l2
 dep-path P p u v = transport P p u ≡ v
 
 syntax dep-path P p u v = u ≡[ P , p ] v
@@ -39,27 +40,28 @@ module Interval where
   I : Set
   I = #I
 
-  0I : I
+  0I 1I : I
   0I = #0
-
-  1I : I
   1I = #1
 
   postulate
     seg : 0I ≡ 1I
 
-  postulate
-    rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B
-
-    rec-Interval-1 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ b₀
-    rec-Interval-2 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 1I ≡ b₁
-
-  {-# REWRITE rec-Interval-1 #-}
-  {-# REWRITE rec-Interval-2 #-}
+  rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B
+  rec-Interval b₀ b₁ s #0 = b₀
+  rec-Interval b₀ b₁ s #1 = b₁
 
   postulate
     rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s
   {-# REWRITE rec-Interval-3 #-}
+
+  rec-Interval-d : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → (x : I) → B x
+  rec-Interval-d b₀ b₁ s #0 = b₀
+  rec-Interval-d b₀ b₁ s #1 = b₁
+
+  postulate
+    rec-Interval-d-3 : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → apd (rec-Interval-d {B} b₀ b₁ s) seg ≡ s
+  {-# REWRITE rec-Interval-d-3 #-}
 open Interval public
 ```
 
@@ -69,9 +71,18 @@ open Interval public
 lemma6∙3∙1 : isContr I
 lemma6∙3∙1 = 1I , f
   where
+    goal : (sym seg) ≡[ (λ z → 1I ≡ z) , seg ] refl
+
     f : (x : I) → 1I ≡ x
-    f #0 = sym seg
-    f #1 = refl
+    f = rec-Interval-d (sym seg) refl goal
+
+    goal2 : transport (λ z → 1I ≡ z) seg (sym seg) ≡ refl
+    goal = goal2
+
+    goal3 : (sym seg) ∙ seg ≡ refl
+    goal2 = lemma2∙11∙2.i seg (sym seg) ∙ goal3
+
+    goal3 = lemma2∙1∙4.ii1 seg
 ```
 
 ### Lemma 6.3.2
@@ -103,34 +114,68 @@ base = #base
 postulate
   loop : base ≡ base
 
-S¹-rec : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
-S¹-rec b l #base = b
+rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
+rec-S¹ b l #base = b
 
 postulate
-  S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (S¹-rec b l) loop ≡ l
-
-{-# REWRITE S¹-rec-loop #-}
+  rec-S¹-loop : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (rec-S¹ b l) loop ≡ l
+{-# REWRITE rec-S¹-loop #-}
 ```
 
 ### Lemma 6.4.1
 
 ```
--- lemma6∙4∙1 : loop ≢ refl
--- lemma6∙4∙1 loop≡refl =
---   {!   !}
---   where
---     f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A)
---     f {A = A} {x = x} {p = p} s =
---       let p' = transportconst A loop x
---       in (S¹-rec x (p' ∙ p)) s
---     -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p
---     -- f-loop {x = x} = S¹-rec-loop x ?
+lemma6∙4∙1 : loop ≢ refl
+lemma6∙4∙1 loop≡refl = goal3
+  where
+    -- goal : (s : S¹) (p : s ≡ s) → p ≡ refl
+    -- goal s p = z1 ∙ z2 ∙ z3
+    --   where
+    --     f : {A : Set} {x : A} {p : x ≡ x} → S¹ → A
+    --     f {x = x} {p = p} = rec-S¹ x p
 
---     goal : ⊥
+    --     z1 : p ≡ apd f loop
+    --     z1 = refl
 
---     goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A 
---     goal = example3∙1∙9 (goal2 {!   !} {!   !} {!   !})
+    --     z2 : apd f loop ≡ apd f refl
+    --     z2 = ap (apd f) loop≡refl
 
---     -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl
---     goal2 A a p x y r s = {!   !}
+    --     z3 : apd f refl ≡ refl
+    --     z3 = refl
+
+    goal2 : ∀ {l} {A : Set l} → isSet A
+    goal2 x .x refl refl = refl
+
+    goal3 : ⊥
+    goal3 = example3∙1∙9 (goal2 {A = Set})
+
+  -- where
+  --   f : {l : Level} {A : Set l} {x : A} {p : x ≡ x} → (S¹ → A)
+  --   f {A = A} {x = x} {p = p} s =
+  --     let p' = transportconst A loop x
+  --     in (rec-S¹ x (p' ∙ p)) s
+  --   -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p
+  --   -- f-loop {x = x} = S¹-rec-loop x ?
+
+  --   goal : ⊥
+
+  --   goal2 : ∀ {l} → (A : Set l) (a : A) (p : a ≡ a) → isSet A 
+  --   goal = example3∙1∙9 (goal2 Set 𝟙 refl)
+
+  --   goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl
+  --   goal2 {l} A a p x y r s = {!   !}
+  --     where
+  --       f' = f {A = A} {x = a} {p = p}
+  --       test = apd f' loop ∙ sym (apd f' loop)
+
+  --       z1 : p ≡ apd f' loop
+  --       z1 = {!   !}
+
+  --       z2 : apd f' loop ≡ apd f' refl
+  --       z2 = {!   !}
+
+  --       z3 : apd f' refl ≡ refl
+  --       z3 = refl
+
+  --       wtf = let wtf = z1 ∙ z2 ∙ z3 in {!   !}
 ```