6.4.2

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)