ch2

flake.nix

@@ -0,0 +1 @@
+

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)

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