Some facts about empty types

Empty.agda

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 ()