119 lines
3.2 KiB
Agda
119 lines
3.2 KiB
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)
|