From 47a3a63375fca65c7151b82ac56b47115debe014 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 22 Dec 2023 10:20:33 -0600
Subject: [PATCH] waht

---
 .vscode/settings.json                      |  3 +
 src/2023-11-27-asdf.agda                   | 13 ++++
 src/2023-12-21-some-group-theory-shit.agda | 15 +++++
 src/CubicalHott/Chapter1.lagda.md          |  0
 src/CubicalHott/Chapter1Exercises.agda     | 31 ++++++++++
 src/CubicalHott/Chapter2.lagda.md          | 69 ++++++++++++++++++++++
 src/CubicalHott/Chapter2Exercises.agda     |  8 +++
 7 files changed, 139 insertions(+)
 create mode 100644 .vscode/settings.json
 create mode 100644 src/2023-11-27-asdf.agda
 create mode 100644 src/2023-12-21-some-group-theory-shit.agda
 create mode 100644 src/CubicalHott/Chapter1.lagda.md
 create mode 100644 src/CubicalHott/Chapter1Exercises.agda
 create mode 100644 src/CubicalHott/Chapter2.lagda.md
 create mode 100644 src/CubicalHott/Chapter2Exercises.agda

diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..d2b262b
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,3 @@
+{
+  "editor.unicodeHighlight.ambiguousCharacters": false
+}
diff --git a/src/2023-11-27-asdf.agda b/src/2023-11-27-asdf.agda
new file mode 100644
index 0000000..d42db40
--- /dev/null
+++ b/src/2023-11-27-asdf.agda
@@ -0,0 +1,13 @@
+module 2023-11-27-asdf where
+
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality as Eq
+
+postulate
+    S1 : Set
+    base : S1
+    loop : base ≡ base
+
+asdf : (c : S1)
+    → ((x : A) → x ≡ c)
\ No newline at end of file
diff --git a/src/2023-12-21-some-group-theory-shit.agda b/src/2023-12-21-some-group-theory-shit.agda
new file mode 100644
index 0000000..581f3a6
--- /dev/null
+++ b/src/2023-12-21-some-group-theory-shit.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --cubical #-}
+-- http://jesse.jaksin14.angelfire.com/Proofs/Group_Theory.pdf
+
+open import Agda.Primitive hiding (Prop)
+
+open import Cubical.Core.Everything
+
+is-Semigroup : (l : Level) → (S : Type l) → Type l
+is-Semigroup l S = Σ[ mul ∈ (S → S → S) ] ((x y z : S) → mul (mul x y) z ≡ mul x (mul y z))
+
+Semigroup : (l : Level) → Type (lsuc l)
+Semigroup l = Σ[ G ∈ Type l ] (is-Semigroup l G)
+
+is-Group : (l : Level) → (S : Semigroup l) → Type l
+is-Group l S = {!   !}
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter1.lagda.md b/src/CubicalHott/Chapter1.lagda.md
new file mode 100644
index 0000000..e69de29
diff --git a/src/CubicalHott/Chapter1Exercises.agda b/src/CubicalHott/Chapter1Exercises.agda
new file mode 100644
index 0000000..dc43fa1
--- /dev/null
+++ b/src/CubicalHott/Chapter1Exercises.agda
@@ -0,0 +1,31 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Chapter1Exercises where
+
+open import Cubical.Core.Everything
+open import Cubical.Core.Primitives public
+open import Data.Empty
+
+refl : {ℓ : Level} {A : Set ℓ} {x : A} → Path A x x
+refl {x = x} = λ i → x
+
+-- Exercise 1.1. Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C. Show that we have h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f .
+infix 10 _∘_
+_∘_ : {A B C : Set} → (g : B → C) → (f : A → B) → A → C
+(g ∘ f) a = g (f a)
+
+exercise-1-1 : {A B C D : Set}
+  → (f : A → B)
+  → (g : B → C)
+  → (h : C → D)
+  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
+exercise-1-1 f g h = refl {x = h ∘ (g ∘ f)}
+
+-- TODO: Explain how this works
+
+-- Exercise 1.11. Show that for any type A, we have ¬¬¬A → ¬A.
+¬_ : (A : Set) → Set
+¬ A = ⊥
+
+exercise-1-11 : {A : Set} → ¬ (¬ (¬ A)) → ¬ A
+exercise-1-11 ()
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md
new file mode 100644
index 0000000..8f57bb6
--- /dev/null
+++ b/src/CubicalHott/Chapter2.lagda.md
@@ -0,0 +1,69 @@
+```
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter2 where
+open import Cubical.Core.Everything
+```
+
+# 2.1 Types are higher groupoids
+
+```
+lemma-2-1-2 : {A : Set}
+  → {x y z : A}
+  → x ≡ y
+  → y ≡ z
+  → x ≡ z
+lemma-2-1-2 {A} {x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
+
+_∙_ = lemma-2-1-2
+```
+
+# 2.2 Functions are functors
+
+```
+lemma-2-2-1 : {A B : Set} {x y : A}
+  → (f : A → B)
+  → x ≡ y
+  → f x ≡ f y
+lemma-2-2-1 f p i = f (p i)
+
+ap = lemma-2-2-1
+```
+
+# 2.4 Homotopies and equivalences
+
+```
+definition-2-4-1 : {A : Set} {P : A → Set}
+  → (f g : (x : A) → P x)
+  → Set
+definition-2-4-1 {A} f g = (x : A) → f x ≡ g x
+
+_∼_ = definition-2-4-1
+
+lemma-2-4-2-1 : {A : Set} {P : A → Set}
+  → (f : (x : A) → P x)
+  → f ∼ f
+lemma-2-4-2-1 f x i = f x
+
+lemma-2-4-2-2 : {A : Set} {P : A → Set}
+  → (f g : (x : A) → P x)
+  → (f∼g : f ∼ g)
+  → g ∼ f
+lemma-2-4-2-2 f g f∼g x i = f∼g x (~ i)
+
+lemma-2-4-2-3 : {A : Set} {P : A → Set}
+  → (f g h : (x : A) → P x)
+  → (f∼g : f ∼ g)
+  → (g∼h : g ∼ h)
+  → f ∼ h
+lemma-2-4-2-3 {A} f g h f∼g g∼h x = (f∼g x) ∙ (g∼h x)
+-- TODO: Wtf how does this work?
+
+lemma-2-4-3 : {A B : Set}
+  → (f g : A → B)
+  → (H : f ∼ g)
+  → {x y : A}
+  → (p : x ≡ y)
+  → (H x ∙ ap g p) ≡ (ap f p ∙ H y)
+lemma-2-4-3 f g H {x} {y} p i =
+  {!   !}
+```
diff --git a/src/CubicalHott/Chapter2Exercises.agda b/src/CubicalHott/Chapter2Exercises.agda
new file mode 100644
index 0000000..6dc8ca1
--- /dev/null
+++ b/src/CubicalHott/Chapter2Exercises.agda
@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Chapter2Exercises where
+
+-- Exercise 2.4. Define, by induction on n, a general notion of n-dimensional
+-- path in a type A, simultaneously with the type of boundaries for such paths.
+
+-- Exercise 2.13. Show that (2 ≃ 2) ≃ 2.