{-# OPTIONS --cubical #-}

module Lemma641 where

open import Level
open import Cubical.Foundations.Prelude 
  using (_≡_; refl; _∙_; _≡⟨⟩_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
open import Cubical.Data.Empty as ⊥
open import Cubical.Foundations.Equiv using (isEquiv; equiv-proof)
open import Relation.Nullary using (¬_)
open import Relation.Binary.Core using (Rel)

_≢_ : {ℓ : Level} {A : Set ℓ} → Rel A ℓ
x ≢ y = ¬ x ≡ y

data S¹ : Set where
  base : S¹
  loop : base ≡ base

data Bool : Set where
  true : Bool
  false : Bool

bool-id : Bool → Bool
bool-id true = true
bool-id false = false

bool-id≡bool : (b : Bool) → bool-id b ≡ b
bool-id≡bool true _ = true
bool-id≡bool false _ = false

bool-id-is-equiv : isEquiv bool-id
bool-id-is-equiv .equiv-proof y .fst = ( y , bool-id≡bool y )
bool-id-is-equiv .equiv-proof y .snd (y′ , p) i = let b = p (~ i) in (? , bool-id≡bool y)

bool-flip : Bool → Bool
bool-flip true = false
bool-flip false = true

f : {A : Set} (x : A) → (p : x ≡ x) → S¹ → A
f x p base = x
f x p (loop i) = p i

refl-base : base ≡ base
refl-base = refl

refl-x : {A : Set} → (x : A) → x ≡ x
refl-x _ = refl

-- p : x ≡ x
-- p : PathP (λ _ → A) x x
-- p : I → A

-- f : S¹ → A
-- loop : I → S¹
-- λ i → f (loop i) : I → A

-- f : S¹ → A
-- refl-base : base ≡ base
-- refl-base : I → S¹
-- λ i → f (refl-base i) : I → A

-- refl-x : x ≡ x
-- refl-x : I → A

-- p ≡ refl : I → (I → A)

types-arent-sets : {A : Set} (x : A) → (p : x ≡ x) → p ≡ refl → ⊥
types-arent-sets x p p≡refl = ?

-- This is the consequence of loop ≡ refl, which says that for any p : x ≡ x, it
-- also equals refl. It is then used with a proof that p ≡ refl → ⊥
consequence : {A : Set} (x : A) → (p : x ≡ x) → loop ≡ refl → p ≡ refl
consequence x p loop≡refl = p
  ≡⟨ refl ⟩
    (λ i → f x p (loop i))
  ≡⟨ cong (λ l i → f x p (l i)) loop≡refl ⟩
    (λ i → f x p (refl-base i))
  ≡⟨ refl ⟩
    refl-x x
  ∎

lemma641 : loop ≢ refl
lemma641 x = ?

-- https://serokell.io/blog/playing-with-negation

-- f : {A : Set} (x : A) → (p : x ≡ x) → (S¹ → A)