From 7ebaf615b05f51dc4a1b6d39834f88473e03e84b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 15 Aug 2024 04:40:01 -0500
Subject: [PATCH] the cubical stuff

---
 src/CubicalHott/Chapter2.agda |  31 +++++++++++
 src/CubicalHott/Chapter3.agda |  51 +++++++++++++++++
 src/CubicalHott/Chapter6.agda | 102 ++++++++++++++++++++++++++++++++++
 src/CubicalHott/Chapter8.agda |  79 ++++++++++++++++++++++++++
 src/CubicalHott/Prelude.agda  |  18 ++++++
 5 files changed, 281 insertions(+)
 create mode 100644 src/CubicalHott/Chapter2.agda
 create mode 100644 src/CubicalHott/Chapter3.agda
 create mode 100644 src/CubicalHott/Chapter6.agda
 create mode 100644 src/CubicalHott/Chapter8.agda
 create mode 100644 src/CubicalHott/Prelude.agda

diff --git a/src/CubicalHott/Chapter2.agda b/src/CubicalHott/Chapter2.agda
new file mode 100644
index 0000000..a905d23
--- /dev/null
+++ b/src/CubicalHott/Chapter2.agda
@@ -0,0 +1,31 @@
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter2 where
+
+open import CubicalHott.Prelude
+open import Cubical.Data.Bool
+open import Cubical.Data.Unit
+open import Cubical.Data.Empty
+open import Cubical.Data.Equality using (id)
+
+private
+  variable
+    l l2 : Level
+
+module lemma2310 where
+  lemma : {A B : Type l}
+    → (P : B → Type l2)
+    → (f : A → B)
+    → {x y : A} → (p : x ≡ y)
+    → (u : P (f x))
+    → subst (P ∘ f) p u ≡ subst P (cong f p) u
+  lemma {A = A} {B = B} P f {x} {y} p u i = goal where
+    goal : P (f y)
+    goal = J (λ y' p' → P (f y')) u p 
+  
+module remark2126 where
+  largeElim : Bool → Type
+  largeElim true = Unit
+  largeElim false = ⊥
+
+  lemma : true ≢ false
+  lemma p = subst largeElim p tt
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter3.agda b/src/CubicalHott/Chapter3.agda
new file mode 100644
index 0000000..d590722
--- /dev/null
+++ b/src/CubicalHott/Chapter3.agda
@@ -0,0 +1,51 @@
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter3 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter2
+open import Cubical.Data.Bool
+open import Cubical.Data.Equality using (id; ap)
+
+private
+  variable
+    l : Level
+
+module example319 where
+  lemma : ¬ isSet (Type l)
+  lemma {l} p = remark2126.lemma fatal where
+    not* : Bool* {l} → Bool* {l}
+    not* (lift false) = lift true
+    not* (lift true) = lift false
+
+    notnot* : (x : Bool* {l}) → not* (not* x) ≡ x
+    notnot* (lift true) = refl
+    notnot* (lift false) = refl
+
+    notIso* : Iso (Bool* {l}) (Bool* {l})
+    Iso.fun notIso* = not*
+    Iso.inv notIso* = not*
+    Iso.rightInv notIso* = notnot*
+    Iso.leftInv notIso* = notnot*
+
+    notEquiv* : Bool* {l} ≃ Bool* {l}
+    notEquiv* = not* , isoToIsEquiv notIso*
+
+    fPath : Bool* {ℓ = l} ≡ Bool* {ℓ = l}
+    fPath = ua notEquiv*
+
+    getFunc : Bool* ≡ Bool* → Bool* → Bool*
+    getFunc path = pathToEquiv path .fst
+    
+    left : getFunc fPath ≡ not*
+    left = cong fst (pathToEquiv-ua notEquiv*)
+
+    right : getFunc fPath ≡ id
+    right = cong getFunc (helper ∙ sym uaIdEquiv) ∙ cong fst (pathToEquiv-ua (idEquiv Bool*)) where
+      helper : fPath ≡ refl
+      helper = p Bool* Bool* fPath refl
+
+    bogus : not* ≡ id
+    bogus = sym left ∙ right
+
+    fatal : true ≡ false
+    fatal = cong (λ f → lower (f (lift true))) (sym bogus) 
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter6.agda b/src/CubicalHott/Chapter6.agda
new file mode 100644
index 0000000..069c86c
--- /dev/null
+++ b/src/CubicalHott/Chapter6.agda
@@ -0,0 +1,102 @@
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter6 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter3
+open import Cubical.Data.Equality.Conversion
+open import Cubical.HITs.S1
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+
+private
+  variable
+    l l2 : Level
+
+-- Equation 6.2.2
+
+dep-path : {A : Type} → (P : A → Type) → {x y : A} → (p : x ≡ y) → (u : P x) → (v : P y) → Type
+dep-path P p u v = subst P p u ≡ v
+
+syntax dep-path P p u v = u ≡[ P , p ] v
+
+-- Lemma 6.2.5
+
+module lemma625 where
+  f : {A : Type} {a : A} {p : a ≡ a} → S¹ → A
+  f {a = a} base = a 
+  f {p = p} (loop i) = p i
+
+-- Lemma 6.2.8
+
+-- module lemma628 where
+--   lemma : {A : Type}
+--     → (f g : S¹ → A)
+--     → (p : f base ≡ g base)
+--     → (q : cong f loop ≡[ (λ x → x ≡ x) , p ] cong g loop)
+--     → (x : S¹) → f x ≡ g x
+--   lemma f g p q base i = p i 
+--   lemma f g p q (loop j) i = {!   !}
+
+-- Interval
+
+data [0,1] : Type where
+  ii0 : [0,1]
+  ii1 : [0,1]
+  seg : ii0 ≡ ii1
+
+-- Lemma 6.3.1
+
+module lemma631 where
+  lemma : isContr [0,1]
+  lemma = ii0 , f where
+    f : (y : [0,1]) → ii0 ≡ y
+    f ii0 = refl 
+    f ii1 = seg
+    f (seg i) j = seg (i ∧ j) 
+    
+-- Lemma 6.3.2
+
+module lemma632 where
+  lemma : {A B : Type}
+    → (f g : A → B)
+    → ((x : A) → f x ≡ g x)
+    → f ≡ g
+  lemma {A} {B} f g p i = q (seg i) where
+    p̃ : (x : A) → [0,1] → B
+    p̃ x ii0 = f x
+    p̃ x ii1 = g x
+    p̃ x (seg i) = p x i
+
+    q : [0,1] → (A → B)
+    q i x = p̃ x i
+    
+-- Lemma 6.4.1
+
+-- module lemma641 where
+--   lemma : loop ≢ refl
+--   lemma loop≡refl = example319.lemma g where
+--     goal : {A : Type l} {x : A} {p : x ≡ x} → (q' : x ≡ x) → refl ≡ q'
+--     goal {A = A} {x} {p} q' = z1 ∙ {!   !} ∙ z3 where
+--       f : S¹ → A
+--       f base = x
+--       f (loop i) = q' i
+
+--       z1 : refl ≡ cong f refl
+--       z1 = refl
+--       z2 : cong f refl ≡ cong f loop
+--       z2 = cong (cong f) loop≡refl
+--       z3 : cong f loop ≡ q'
+--       z3 = refl
+    
+--     g : isSet Type
+--     g x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') goal p q
+
+
+-- Corollary 6.10.13
+
+module corollary61013 where
+  p^ : {A : Type l} {a : A} {p : a ≡ a} → (n : ℤ) → a ≡ a
+  p^ (pos zero) = refl
+  p^ {p = p} (pos (suc x)) = p^ {p = p} (pos x) ∙ p
+  p^ {p = p} (negsuc zero) = p^ {p = p} (pos zero) ∙ sym p
+  p^ {p = p} (negsuc (suc n)) = p^ {p = p} (negsuc n) ∙ sym p ∙ sym p
diff --git a/src/CubicalHott/Chapter8.agda b/src/CubicalHott/Chapter8.agda
new file mode 100644
index 0000000..17041f1
--- /dev/null
+++ b/src/CubicalHott/Chapter8.agda
@@ -0,0 +1,79 @@
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter8 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter2
+open import CubicalHott.Chapter6
+open import Cubical.HITs.S1 hiding (encode; decode)
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+
+private
+  variable
+    l : Level
+
+module section81 where
+  Z* : Type l
+  Z* = Lift ℤ
+  
+  zsuc : Z* {l} → Z* {l}
+  zsuc (lift x) = lift (sucℤ x)
+
+  zpred : Z* {l} → Z* {l}
+  zpred (lift x) = lift (predℤ x)
+
+  zsucpred : (i : Z* {l}) → zsuc (zpred i) ≡ i
+  zsucpred (lift i) = cong lift (sucPred i)
+
+  zpredsuc : (i : Z* {l}) → zpred (zsuc i) ≡ i
+  zpredsuc (lift i) = cong lift (predSuc i)
+
+  zsuc-iso : Iso (Z* {l}) (Z* {l})
+  Iso.fun zsuc-iso = zsuc
+  Iso.inv zsuc-iso = zpred
+  Iso.rightInv zsuc-iso = zsucpred
+  Iso.leftInv zsuc-iso = zpredsuc
+
+  zsuc-equiv : Z* {l} ≃ Z* {l}
+  zsuc-equiv = isoToEquiv zsuc-iso
+
+  loop^ : ℤ → base ≡ base
+  loop^ z = corollary61013.p^ {p = loop} z
+
+  -- Definition 8.1.1
+  code : S¹ → Type l
+  code {l} base = Z*
+  code {l} (loop i) = ua zsuc-equiv i 
+
+  -- Lemma 8.1.2
+  lemma1 : (x : Z* {l}) → subst code loop x ≡ zsuc x
+  lemma1 x = lemma2310.lemma code id loop x
+
+  lemma2 : (x : Z* {l}) → subst code (sym loop) x ≡ zpred x
+  lemma2 x = lemma2310.lemma code id (sym loop) x
+
+  -- Definition 8.1.5
+  encode : (x : S¹) → (base ≡ x) → code {l} x
+  encode x p = subst code p (lift 0)
+
+  -- Definition 8.1.6
+  postulate
+    -- TODO: What the fuck? https://1lab.dev/Homotopy.Space.Circle.html#3850
+    -- decode : (x : S¹) → code {l} x → (base ≡ x)
+    -- decode base c = refl
+    -- decode (loop i) c = {!  loop^ c  !}
+  decode : (x : S¹) → code {l} x → (base ≡ x)
+  decode base (lift c) = loop^ c
+  decode (loop i) c j = {! c !}
+
+  -- Lemma 8.1.7
+  postulate
+    decode-encode : (x : S¹) → (p : base ≡ x) → decode {l} x (encode x p) ≡ p
+    -- decode-encode x p = J (λ y' p' → decode y' (encode y' p') ≡ p') h p where
+    --   h : decode base (encode base refl) ≡ refl
+    --   h = {!   !}
+    
+  -- Lemma 8.1.8
+  encode-decode : (x : S¹) → (c : code {l} x) → encode {l} x (decode x c) ≡ c
+  encode-decode base c = {!   !}
+  encode-decode (loop i) c = {!   !} 
\ No newline at end of file
diff --git a/src/CubicalHott/Prelude.agda b/src/CubicalHott/Prelude.agda
new file mode 100644
index 0000000..775ea56
--- /dev/null
+++ b/src/CubicalHott/Prelude.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --cubical #-}
+module CubicalHott.Prelude where
+
+open import Agda.Primitive using (Level) public
+open import Cubical.Foundations.Equiv public
+open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.Univalence public
+open import Cubical.Foundations.Function public
+open import Cubical.Relation.Nullary public
+open import Cubical.Data.Equality using (id) public
+
+private
+  variable
+    l : Level
+
+_≢_ : ∀ {A : Type l} → A → A → Type l
+a ≢ b = ¬ a ≡ b
\ No newline at end of file