From 596980e9ffeabbbe9a246de75380c2e4afa2fa1d Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 12 Sep 2024 00:43:14 -0500
Subject: [PATCH] initial

---
 .gitignore             |  2 ++
 .vscode/settings.json  |  6 +++++
 cubical-hott.agda-lib  |  2 ++
 src/Chapter1.agda      |  0
 src/Chapter2.lagda.typ | 59 ++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 69 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 .vscode/settings.json
 create mode 100644 cubical-hott.agda-lib
 create mode 100644 src/Chapter1.agda
 create mode 100644 src/Chapter2.lagda.typ

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..9401034
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+_build
+*.pdf
\ No newline at end of file
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..c0fe5db
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,6 @@
+{
+	"agdaMode.connection.commandLineOptions": "--safe --cubical --without-K",
+	"files.associations": {
+		"*.lagda.typ": "agda"
+	}
+}
diff --git a/cubical-hott.agda-lib b/cubical-hott.agda-lib
new file mode 100644
index 0000000..31949b1
--- /dev/null
+++ b/cubical-hott.agda-lib
@@ -0,0 +1,2 @@
+include: src
+depend: cubical
\ No newline at end of file
diff --git a/src/Chapter1.agda b/src/Chapter1.agda
new file mode 100644
index 0000000..e69de29
diff --git a/src/Chapter2.lagda.typ b/src/Chapter2.lagda.typ
new file mode 100644
index 0000000..56c63fc
--- /dev/null
+++ b/src/Chapter2.lagda.typ
@@ -0,0 +1,59 @@
+```
+module Chapter2 where
+open import Cubical.Foundations.Prelude
+```
+
+=== Lemma 2.1.1
+
+```
+lemma2-1-1 : {A : Type} {x y : A}
+  → (x ≡ y) → (y ≡ x)
+lemma2-1-1 p i = p (~ i)
+```
+
+=== Lemma 2.1.2
+
+```
+lemma2-1-2 : {A : Type} {x y z : A}
+  → (x ≡ y) → (y ≡ z) → (x ≡ z)
+lemma2-1-2 {x = x} p q i = hcomp (λ where
+    j (i = i0) → x
+    j (i = i1) → q j
+  ) (p i)
+```
+
+=== Lemma 2.1.4
+
+```
+module lemma2-1-4 where
+  variable
+    A : Type
+    x y z w : A
+    p : x ≡ y
+    q : y ≡ z
+    r : z ≡ w
+```
+
++ #[
+  ```
+  lemma2-1-4-i1 : p ≡ p ∙ refl
+  lemma2-1-4-i1 {A} {x} {y} {p} j i = hfill (λ where
+      _ (i = i0) → x
+      _ (i = i1) → y
+    ) (inS (p i)) j
+
+  -- lemma2-1-4-i2 : p ≡ refl ∙ p
+  -- lemma2-1-4-i2 {A} {x} {y} {p} j i = hfill (λ where
+  --     _ (i = i0) → x
+  --     _ (i = i1) → y
+  --  ) (inS (p i)) {! i1 !}
+
+  postulate
+    lemma2-1-4-ii1 : (sym p) ∙ p ≡ refl
+    lemma2-1-4-ii2 : p ∙ (sym p) ≡ refl
+    lemma2-1-4-iii : sym (sym p) ≡ refl
+
+  lemma2-1-4-iv : p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+  lemma2-1-4-iv i j = {!   !}
+  ```
+]
\ No newline at end of file