The universal property of the empty type

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-07.
Last modified on 2024-02-06.

module foundation.universal-property-empty-type where
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types


There is a unique map from the empty type into any type. Similarly, for any type family over an empty type, there is a unique dependent function taking values in this family.


module _
  {l1 : Level} (A : UU l1)

  dependent-universal-property-empty : (l : Level)  UU (l1  lsuc l)
  dependent-universal-property-empty l =
    (P : A  UU l)  is-contr ((x : A)  P x)

  universal-property-empty : (l : Level)  UU (l1  lsuc l)
  universal-property-empty l = (X : UU l)  is-contr (A  X)

  universal-property-dependent-universal-property-empty :
    ({l : Level}  dependent-universal-property-empty l) 
    ({l : Level}  universal-property-empty l)
  universal-property-dependent-universal-property-empty dup-empty {l} X =
    dup-empty {l}  a  X)

  is-empty-universal-property-empty :
    ({l : Level}  universal-property-empty l)  is-empty A
  is-empty-universal-property-empty up-empty = center (up-empty empty)

  dependent-universal-property-empty-is-empty :
    {l : Level} (H : is-empty A)  dependent-universal-property-empty l
  pr1 (dependent-universal-property-empty-is-empty {l} H P) x = ex-falso (H x)
  pr2 (dependent-universal-property-empty-is-empty {l} H P) f =
    eq-htpy  x  ex-falso (H x))

  universal-property-empty-is-empty :
    {l : Level} (H : is-empty A)  universal-property-empty l
  universal-property-empty-is-empty {l} H =
      ( dependent-universal-property-empty-is-empty H)

  dependent-universal-property-empty' :
    {l : Level} (P : empty  UU l)  is-contr ((x : empty)  P x)
  pr1 (dependent-universal-property-empty' P) = ind-empty {P = P}
  pr2 (dependent-universal-property-empty' P) f = eq-htpy ind-empty

  universal-property-empty' :
    {l : Level} (X : UU l)  is-contr (empty  X)
  universal-property-empty' X =
    dependent-universal-property-empty'  t  X)

  uniqueness-empty :
    {l : Level} (Y : UU l) 
    ({l' : Level} (X : UU l')  is-contr (Y  X)) 
    is-equiv (ind-empty {P = λ t  Y})
  uniqueness-empty Y H =
    is-equiv-is-equiv-precomp ind-empty
      ( λ X 
          ( λ g  g  ind-empty)
          ( H X)
          ( universal-property-empty' X))

  universal-property-empty-is-equiv-ind-empty :
    {l : Level} (X : UU l)  is-equiv (ind-empty {P = λ t  X}) 
    ((l' : Level) (Y : UU l')  is-contr (X  Y))
  universal-property-empty-is-equiv-ind-empty X is-equiv-ind-empty l' Y =
      ( empty  Y)
      ( λ f  f  ind-empty)
      ( is-equiv-precomp-is-equiv ind-empty is-equiv-ind-empty Y)
      ( universal-property-empty' Y)

Recent changes