wip

src/CubicalHott/Chapter1.lagda.md

@@ -48,7 +48,7 @@ record ⊤ : Type where
 ```
 
 ```
-data ⊥ {l} : Type l where
+data ⊥ : Type where
 ```
 
 ## 1.8 The type of booleans
@@ -70,7 +70,7 @@ neg false = true
 ```
 infix 3 ¬_
 ¬_ : ∀ {l} (A : Type l) → Type l
-¬_ {l} A = A → ⊥ {l}
+¬_ A = A → ⊥
 ```
 
 ## 1.12 Identity types

src/CubicalHott/Chapter2.lagda.md

@@ -286,13 +286,14 @@ open axiom2∙10∙3
 ### 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 : 𝟚 → Type
+    where
-    Bmap true = 𝟙
+      Bmap : 𝟚 → Type
-    Bmap false = ⊥
+      Bmap true = 𝟙
+      Bmap false = ⊥
 
-    genBot : 𝟙 → ⊥
+      genBot : 𝟙 → ⊥
-    genBot = transport Bmap p
+      genBot = transport Bmap p
 ```

src/CubicalHott/Chapter2Util.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --no-load-primitives --cubical #-}
+
+module CubicalHott.Chapter2Util where
+
+open import CubicalHott.Primitives
+open import CubicalHott.CoreUtil
+open import CubicalHott.Chapter1
+open import CubicalHott.Chapter2
+
+Bool : ∀ {l} → Type l
+Bool = Lift 𝟚
+
+Bool-neg : ∀ {l} → Bool {l} → Bool {l}
+Bool-neg (lift true) = lift false
+Bool-neg (lift false) = lift true
+
+Bool-neg-homotopy : ∀ {l} → (Bool-neg {l} ∘ Bool-neg {l}) ∼ id
+Bool-neg-homotopy (lift true) = refl
+Bool-neg-homotopy (lift false) = refl
+
+Bool-neg-equiv : ∀ {l} → Bool {l} ≃ Bool {l}
+Bool-neg-equiv = Bool-neg , qinv-to-isequiv (mkQinv Bool-neg Bool-neg-homotopy Bool-neg-homotopy)

src/CubicalHott/Chapter3.lagda.md

@@ -4,6 +4,8 @@ module CubicalHott.Chapter3 where
 
 open import CubicalHott.Chapter1
 open import CubicalHott.Chapter2
+open import CubicalHott.Chapter2Util
+open import CubicalHott.CoreUtil
 ```
 
 ### Definition 3.1.1
@@ -16,13 +18,35 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.9
 
 ```
-example3∙1∙9 : {l : Level} → ¬ (isSet (Type l))
+example3∙1∙9 : ∀ {l : Level} → ¬ (isSet (Type l))
-example3∙1∙9 p =
+example3∙1∙9 p = remark2∙12∙6.true≢false lol
-  {!   !}
   where
-    lol : (x : 𝟚) → neg (neg x) ≡ x
+    open axiom2∙10∙3
-    lol true = refl
+
-    lol false = refl
+    f-path : Bool ≡ Bool
+    f-path = ua Bool-neg-equiv
+
+    bogus : id ≡ Bool-neg
+    bogus =
+      let
+        helper : f-path ≡ refl
+        helper = p Bool Bool f-path refl
+
+        wtf : idtoeqv f-path ≡ idtoeqv refl
+        wtf = ap idtoeqv helper
+
+        wtf2 : Σ.fst (idtoeqv (ua Bool-neg-equiv)) ≡ id
+        wtf2 = ap Σ.fst wtf
+
+        wtf3 : Σ.fst (idtoeqv (ua Bool-neg-equiv)) ≡ Bool-neg
+        wtf3 = ap Σ.fst (propositional-computation Bool-neg-equiv)
+
+        wtf4 : Bool-neg ≡ id
+        wtf4 = sym wtf3 ∙ wtf2
+      in {!   !}
+
+    lol : true ≡ false
+    lol = ap (λ f → Lift.lower (f (lift true))) bogus
 ```
 
 ### Definition 3.3.1

src/CubicalHott/CoreUtil.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --no-load-primitives --cubical #-}
+
+module CubicalHott.CoreUtil where
+
+open import CubicalHott.Primitives
+
+record Lift {a ℓ} (A : Type a) : Type (a ⊔ ℓ) where
+  constructor lift
+  field lower : A

src/HottBook/Chapter2.lagda.md

@@ -873,6 +873,15 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q =
 --   → (q : a ≡ a)
 --   → (r : a' ≡ a')
 --   → (transport (λ y → y ≡ y) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
+-- theorem2∙11∙5 refl q r = f , qinv-to-isequiv (mkQinv g {!   !} {!   !})
+--   where
+--     f : q ≡ r → q ∙ refl ≡ refl ∙ r
+--     f p = sym (lemma2∙1∙4.i1 q) ∙ p ∙ lemma2∙1∙4.i2 r
+
+--     g : q ∙ refl ≡ refl ∙ r → id q ≡ r
+--     g p = (lemma2∙1∙4.i1 q) ∙ p ∙ sym (lemma2∙1∙4.i2 r)
+
+--     -- forward : (f ∘ g) ∼ id
 ```
 
 ## 2.12 Coproducts

src/HottBook/Chapter6.lagda.md

@@ -9,6 +9,7 @@ module HottBook.Chapter6 where
 open import HottBook.Chapter1
 open import HottBook.Chapter2
 open import HottBook.Chapter3
+open import HottBook.Chapter6Circle
 open import HottBook.CoreUtil
 
 private
@@ -31,6 +32,40 @@ dep-path P p u v = transport P p u ≡ v
 syntax dep-path P p u v = u ≡[ P , p ] v
 ```
 
+### Lemma 6.2.5
+
+```
+lemma6∙2∙5 : {A : Set} → {a : A} → {p : a ≡ a} → S¹ → A
+lemma6∙2∙5 {A} {a} {p} = rec-S¹ a p
+  where
+    path : a ≡[ (λ _ → A) , loop ] a
+    path = transportconst A loop a
+```
+
+### Lemma 6.2.8
+
+```
+lemma6∙2∙8 : {A : Set} → {f g : S¹ → A}
+  → (p : f S¹.base ≡ g S¹.base)
+  → (q : ap f loop ≡[ (λ y → y ≡ y) , p ] (ap g loop))
+  → (x : S¹) → f x ≡ g x
+lemma6∙2∙8 {f = f} {g = g} p q = rec-S¹ p goal
+  where
+    goal : p ≡[ (λ y → f y ≡ g y) , loop ] p
+    goal2 : dep-path (λ y → f y ≡ g y) loop p p
+    goal = goal2
+    goal3 : transport (λ y → f y ≡ g y) loop p ≡ p
+    goal2 = goal3
+    postulate
+      admit : transport (λ y → f y ≡ g y) loop p ≡ p
+    goal3 = admit
+    -- goal4 : p ∙ loop ≡ loop ∙ p
+    -- goal3 = theorem2∙11∙5
+    -- goal4 : sym (ap f loop) ∙ p ∙ (ap g loop) ≡ p
+    -- goal3 = theorem2∙11∙3 loop p ∙ goal4
+    -- goal5 : 
+```
+
 ## 6.3 The interval
 
 ```
@@ -95,22 +130,7 @@ lemma6∙3∙2 {A = A} {B = B} {f = f} {g = g} p = apd q seg
 
 ## 6.4 Circles and sphere
 
-```
+{{#include HottBook.Chapter6Circle.md:circle}}
-module S¹ where
-  postulate
-    S¹ : Set
-    base : S¹
-    loop : base ≡ base
-
-    rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
-    rec-S¹-base : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → rec-S¹ {P = P} b l base ≡ b
-    {-# REWRITE rec-S¹-base #-}
-    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
-
-    -- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
-    -- {-# REWRITE rec-S¹-loop #-}
-open S¹ hiding (base)
-```
 
 ### Lemma 6.4.1
 
@@ -293,24 +313,24 @@ open Suspension public
 ### Lemma 6.5.1
 
 ```
-lemma6∙5∙1 : Susp 𝟚 ≃ S¹
+-- lemma6∙5∙1 : Susp 𝟚 ≃ S¹
-lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
+-- lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
-  where
+--   where
-    open S¹
+--     open S¹
 
-    m : 𝟚 → base ≡ base
+--     m : 𝟚 → base ≡ base
-    m true = refl
+--     m true = refl
-    m false = loop
+--     m false = loop
 
-    f : Susp 𝟚 → S¹
+--     f : Susp 𝟚 → S¹
-    f s = rec-Susp base base m s
+--     f s = rec-Susp base base m s
 
-    g : S¹ → Susp 𝟚
+--     g : S¹ → Susp 𝟚
-    g s = rec-S¹ N (merid false ∙ sym (merid true)) s
+--     g s = rec-S¹ N (merid false ∙ sym (merid true)) s
     
-    forward : (f ∘ g) ∼ id
+--     forward : (f ∘ g) ∼ id
-    forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl {!  refl !} x
+--     forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl {!  refl !} x
     
-    backward : (g ∘ f) ∼ id
+--     backward : (g ∘ f) ∼ id
-    backward x = {!   !}
+--     backward x = {!   !}
 ```

src/HottBook/Chapter6Circle.lagda.md

@@ -0,0 +1,38 @@
+```
+{-# OPTIONS --rewriting #-}
+
+module HottBook.Chapter6Circle where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+
+private
+  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
+```
+
+## Circle
+
+[//]: <> (ANCHOR: circle)
+
+```
+module S¹ where
+  postulate
+    S¹ : Set
+    base : S¹
+    loop : base ≡ base
+
+    rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
+    rec-S¹-base : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → rec-S¹ {P = P} b l base ≡ b
+    {-# REWRITE rec-S¹-base #-}
+    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
+
+    -- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
+    -- {-# REWRITE rec-S¹-loop #-}
+open S¹ hiding (base) public
+```
+
+[//]: <> (ANCHOR_END: circle)

src/HottBook/Chapter8.lagda.md

@@ -7,6 +7,10 @@
 module HottBook.Chapter8 where
 
 open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter6
+open import HottBook.Chapter6Circle
+open import HottBook.CoreUtil
 ```
 
 </details>
@@ -16,4 +20,80 @@ open import HottBook.Chapter1
 ```
 π : (n : ℕ) → (A : Set) → (a : A) → Set
 -- π n A a = ∥ ? ∥₀
+```
+
+### Definition 8.1.1
+
+Universal cover of S¹
+
+```
+data ℤ : Set where
+  pos    : ℕ → ℤ
+  negsuc : ℕ → ℤ
+{-# BUILTIN INTEGER ℤ #-}
+{-# BUILTIN INTEGERPOS    pos    #-}
+{-# BUILTIN INTEGERNEGSUC negsuc #-}
+
+zsuc : ℤ → ℤ
+zsuc (pos x) = pos (suc x)
+zsuc (negsuc zero) = pos zero
+zsuc (negsuc (suc x)) = negsuc x
+
+zpred : ℤ → ℤ
+zpred (pos zero) = negsuc zero
+zpred (pos (suc x)) = pos x
+zpred (negsuc x) = negsuc (suc x)
+
+Int : {l : Level} → Set l
+Int = Lift ℤ
+
+int-suc : {l : Level} → Int {l} → Int {l}
+int-suc (lift (pos x)) = lift (pos (suc x))
+int-suc (lift (negsuc zero)) = lift (pos zero)
+int-suc (lift (negsuc (suc x))) = lift (negsuc x)
+
+int-pred : {l : Level} → Int {l} → Int {l}
+int-pred (lift (pos zero)) = lift (negsuc zero)
+int-pred (lift (pos (suc x))) = lift (pos x)
+int-pred (lift (negsuc x)) = lift (negsuc (suc x))
+
+module definition8∙1∙1 where
+  open S¹
+  open axiom2∙10∙3
+
+  zsuc-equiv : {l : Level} → Int {l} ≃ Int {l}
+  zsuc-equiv = int-suc , qinv-to-isequiv (mkQinv int-pred forward backward)
+    where
+
+      forward : (int-suc ∘ int-pred) ∼ id
+      forward (lift (pos zero)) = refl
+      forward (lift (pos (suc x))) = refl
+      forward (lift (negsuc x)) = refl
+
+      backward : (int-pred ∘ int-suc) ∼ id
+      backward (lift (pos x)) = refl
+      backward (lift (negsuc zero)) = refl
+      backward (lift (negsuc (suc x))) = refl
+
+  code : {l : Level} → S¹ → Set l
+  code = rec-S¹ Int (ua zsuc-equiv)
+```
+
+### Lemma 8.1.2
+
+```
+module lemma8∙1∙2 where
+  open definition8∙1∙1
+  open axiom2∙10∙3
+  open ≡-Reasoning
+
+  i : {l : Level} → (x : Int {l}) → (transport code loop x) ≡ int-suc x
+  i x = begin
+    (transport code loop x) ≡⟨ lemma2∙3∙10 {! id  !} code loop x ⟩
+    (transport id (ap code loop) x) ≡⟨ {!   !} ⟩
+    -- (transport id (ua int-suc) x) ≡⟨ {!   !} ⟩
+    int-suc x ∎
+
+  -- ii : (x : ℤ) → (transport code (sym loop) x) ≡ zpred x
+  -- ii x = {!   !}
 ```

src/VanDoornDissertation/HoTT/Sphere2.agda

@@ -0,0 +1,3 @@
+{-# OPTIONS --cubical #-}
+module VanDoornDissertation.HoTT.Sphere2 where
+

src/VanDoornDissertation/Spectral/README.md

@@ -0,0 +1 @@
+This is an attempt at doing a direct translation.