Created
July 23, 2021 16:13
-
-
Save dorchard/0714eccc4f21fdc50b20ea90d2b2975f to your computer and use it in GitHub Desktop.
Some facts about empty types
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Empty where | |
open import Data.Empty | |
open import Relation.Binary.PropositionalEquality | |
open import Relation.Nullary | |
open import Function.Inverse | |
-- Empty type has only unequal elements | |
uneq : (x y : ⊥) -> x ≢ y | |
uneq () y prf | |
-- Empty type has only equal elements | |
eq : (x y : ⊥) -> x ≡ y | |
eq () y | |
-- Type whose elements are always unequal is isomorphic to empty type | |
isEmpty : (A : Set) -> ((x y : A) -> x ≢ y) -> A ↔ ⊥ | |
isEmpty A prop = record { | |
to = record { _⟨$⟩_ = left ; cong = cong left } | |
; from = record { _⟨$⟩_ = right ; cong = cong right } | |
; inverse-of = record { | |
left-inverse-of = leftRight | |
; right-inverse-of = rightLeft | |
} | |
} | |
where | |
left : A -> ⊥ | |
left x = prop x x refl | |
right : ⊥ -> A | |
right () | |
leftRight : (x : A) → right (left x) ≡ x | |
leftRight x with left x | |
... | () | |
rightLeft : (x : ⊥) -> left (right x) ≡ x | |
rightLeft () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment