type-theory/src/Lemma641.agda

{-# 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; equivProof; 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

-- record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
--   no-eta-equality
--   field
--     equiv-proof : (y : B) → isContr (fiber f y)

--  isEquiv bool-id
--    A = Bool
--    B = Bool
--    f : Bool → Bool
--  equiv-proof : (y : B = Bool) → isContr (fiber f y)

--  fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ')
--  fiber {A = A} f y = Σ A \ x → f x ≡ y
--  fiber f y
--    f : Bool → Bool
--    A = Bool
--    B = Bool
--    y : Bool = y
--  fiber f y = Σ Bool \ x → f x ≡ y

--  isContr : ∀ {ℓ} → Set ℓ → Set ℓ
--  isContr A = Σ A \ x → (∀ y → x ≡ y)
--  isContr (Σ Bool \ x → f x ≡ y)
--    = Σ (Σ Bool \ x → f x ≡ y) \ x → (∀ y → x ≡ y)
--
--    .fst = (x , f x ≡ y)
--    .snd = (∀ y → .fst ≡ y)

bool-id-is-equiv : isEquiv bool-id
bool-id-is-equiv .equiv-proof y = ?
-- First is an element of bool-id ≡ bool
-- bool-id-is-equiv .equiv-proof y .fst = ( y , bool-id≡bool y )
-- -- Second is a proof that any other inhabitant of bool-id ≡ bool is the same as the above
-- bool-id-is-equiv .equiv-proof y .snd = ?

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)