prove 6.4.1

src/CubicalHott/Lemma6-4-1.agda

@@ -2,9 +2,25 @@
 
 module CubicalHott.Lemma6-4-1 where
 
+open import Agda.Primitive
 open import Cubical.Foundations.Prelude
 open import Cubical.Relation.Nullary
+open import Cubical.Data.Empty
 open import Cubical.HITs.S1
+open import CubicalHott.Example3-1-9 renaming (lemma to lemma3-1-9)
 
 loop≢refl : ¬ (loop ≡ refl)
-loop≢refl p = {!   !}
+loop≢refl loop≡refl = false where
+  f : ∀ {l} → (A : Type l) → (x : A) → (p : x ≡ x) → S¹ → A
+  f A x p base = x
+  f A x p (loop i) = p i
+
+  p-refl : ∀ {l} → (A : Type l) → (x : A) → (p : x ≡ x) → p ≡ refl
+  p-refl A x p i j = f A x p (loop≡refl i j)
+
+  oops : ∀ {l} → (A : Type l) → isSet A
+  oops {l} A x y p q =
+    J (λ y' p' → (q' : x ≡ y') → p' ≡ q') (λ q' → sym (p-refl A x q')) p q
+
+  false : ⊥
+  false = lemma3-1-9 (oops Type)