initial

.gitignore

@@ -0,0 +1,2 @@
+_build
+*.pdf

.vscode/settings.json

@@ -0,0 +1,6 @@
+{
+	"agdaMode.connection.commandLineOptions": "--safe --cubical --without-K",
+	"files.associations": {
+		"*.lagda.typ": "agda"
+	}
+}

cubical-hott.agda-lib

@@ -0,0 +1,2 @@
+include: src
+depend: cubical

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 = {!   !}
+  ```
+]