From 73a58bd2c285159dd162eedcf9efda97121f4e1c Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 23 Aug 2024 20:18:40 -0500
Subject: [PATCH] ch2

---
 flake.nix                     |  1 +
 src/CubicalHott/Chapter2.agda | 20 ++++++++++++++++++++
 src/CubicalHott/Chapter8.agda |  2 +-
 3 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 flake.nix

diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1 @@
+
diff --git a/src/CubicalHott/Chapter2.agda b/src/CubicalHott/Chapter2.agda
index a905d23..31fe5ef 100644
--- a/src/CubicalHott/Chapter2.agda
+++ b/src/CubicalHott/Chapter2.agda
@@ -11,6 +11,26 @@ private
   variable
     l l2 : Level
 
+module lemma211 where
+  lemma : {A : Type l} → {x y : A} → (x ≡ y) → (y ≡ x)
+  lemma p i = p (~ i)
+
+module lemma212 where
+  lemma : {A : Type l} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+  lemma {x = x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
+
+module lemma214 where
+  private
+    variable
+      A : Type l
+      x y z w : A
+      p : x ≡ y
+      q : y ≡ z
+      r : z ≡ w
+
+  lemma-i : p ≡ p ∙ refl
+  lemma-i = hfill {!   !} {!   !} {!   !}
+  
 module lemma2310 where
   lemma : {A B : Type l}
     → (P : B → Type l2)
diff --git a/src/CubicalHott/Chapter8.agda b/src/CubicalHott/Chapter8.agda
index fab4ae1..abdc84e 100644
--- a/src/CubicalHott/Chapter8.agda
+++ b/src/CubicalHott/Chapter8.agda
@@ -64,7 +64,7 @@ module section81 where
     -- 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 !}
+  decode (loop i) c j = {!   !}
 
   -- Lemma 8.1.7
   postulate