{-# OPTIONS --cubical --no-import-sorts --safe #-} module Cubical.Data.Empty.Properties where open import Cubical.Core.Everything open import Cubical.Foundations.Prelude open import Cubical.Foundations.Isomorphism open import Cubical.Data.Empty.Base isProp⊥ : isProp ⊥ isProp⊥ () isContr⊥→A : ∀ {ℓ} {A : Type ℓ} → isContr (⊥ → A) fst isContr⊥→A () snd isContr⊥→A f i () uninhabEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → ⊥) → (B → ⊥) → A ≃ B uninhabEquiv ¬a ¬b = isoToEquiv isom where open Iso isom : Iso _ _ isom .fun a = rec (¬a a) isom .inv b = rec (¬b b) isom .rightInv b = rec (¬b b) isom .leftInv a = rec (¬a a)