From 4f2c25cf44a86eabc2b0c858d2615f9cb9bda9eb Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 24 Sep 2024 23:59:10 -0500
Subject: [PATCH] 6.4.2

---
 src/CubicalHott/Lemma6-4-2.agda | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 src/CubicalHott/Lemma6-4-2.agda

diff --git a/src/CubicalHott/Lemma6-4-2.agda b/src/CubicalHott/Lemma6-4-2.agda
new file mode 100644
index 0000000..dd97079
--- /dev/null
+++ b/src/CubicalHott/Lemma6-4-2.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-4-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.S1
+open import Cubical.Relation.Nullary
+open import CubicalHott.Lemma6-4-1
+
+lemma : Σ ((x : S¹) → x ≡ x) (λ f → ¬ (f ≡ λ x _ → x))
+lemma = f , p where
+  f : (x : S¹) → x ≡ x
+  f base = loop 
+  f (loop i) j =
+    let u = λ k → λ where
+      (i = i0) → loop (j ∨ ~ k)
+      (i = i1) → loop (j ∧ k)
+      (j = i0) → loop (i ∨ ~ k)
+      (j = i1) → loop (i ∧ k)
+    in hcomp u base
+
+  p : ¬ f ≡ (λ x _ → x)
+  p q = loop≢refl (funExt⁻ q base)
\ No newline at end of file