The unit type

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

Created on 2022-01-27.
Last modified on 2023-06-15.

module foundation.unit-type where
open import foundation.dependent-pair-types
open import foundation.raising-universe-levels
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.truncated-types
open import foundation-core.truncation-levels


The unit type is inductively generated by one point.


The unit type

record unit : UU lzero where
  instance constructor star

{-# BUILTIN UNIT unit #-}

The induction principle of the unit type

ind-unit : {l : Level} {P : unit  UU l}  P star  ((x : unit)  P x)
ind-unit p star = p

The terminal map out of a type

terminal-map : {l : Level} {A : UU l}  A  unit
terminal-map = const _ unit star

Points as maps out of the unit type

point : {l : Level} {A : UU l}  A  (unit  A)
point a = const unit _ a

Raising the universe level of the unit type

raise-unit : (l : Level)  UU l
raise-unit l = raise l unit

raise-star : {l : Level}  raise l unit
raise-star = map-raise star

compute-raise-unit : (l : Level)  unit  raise-unit l
compute-raise-unit l = compute-raise l unit


The unit type is contractible

  is-contr-unit : is-contr unit
  pr1 is-contr-unit = star
  pr2 is-contr-unit star = refl

Any contractible type is equivalent to the unit type

module _
  {l : Level} {A : UU l}

    is-equiv-terminal-map-is-contr :
      is-contr A  is-equiv (terminal-map {A = A})
    pr1 (pr1 (is-equiv-terminal-map-is-contr H)) = ind-unit (center H)
    pr2 (pr1 (is-equiv-terminal-map-is-contr H)) = ind-unit refl
    pr1 (pr2 (is-equiv-terminal-map-is-contr H)) x = center H
    pr2 (pr2 (is-equiv-terminal-map-is-contr H)) = contraction H

    is-contr-is-equiv-const : is-equiv (terminal-map {A = A})  is-contr A
    pr1 (is-contr-is-equiv-const ((g , G) , (h , H))) = h star
    pr2 (is-contr-is-equiv-const ((g , G) , (h , H))) = H

The unit type is a proposition

  is-prop-unit : is-prop unit
  is-prop-unit = is-prop-is-contr is-contr-unit

unit-Prop : Prop lzero
pr1 unit-Prop = unit
pr2 unit-Prop = is-prop-unit

The unit type is a set

  is-set-unit : is-set unit
  is-set-unit = is-trunc-succ-is-trunc neg-one-𝕋 is-prop-unit

unit-Set : Set lzero
pr1 unit-Set = unit
pr2 unit-Set = is-set-unit
  is-contr-raise-unit :
    {l1 : Level}  is-contr (raise-unit l1)
  is-contr-raise-unit {l1} =
    is-contr-equiv' unit (compute-raise l1 unit) is-contr-unit

  is-prop-raise-unit :
    {l1 : Level}  is-prop (raise-unit l1)
  is-prop-raise-unit {l1} =
    is-prop-equiv' (compute-raise l1 unit) is-prop-unit

raise-unit-Prop :
  (l1 : Level)  Prop l1
pr1 (raise-unit-Prop l1) = raise-unit l1
pr2 (raise-unit-Prop l1) = is-prop-raise-unit

  is-set-raise-unit :
    {l1 : Level}  is-set (raise-unit l1)
  is-set-raise-unit = is-trunc-succ-is-trunc neg-one-𝕋 is-prop-raise-unit

raise-unit-Set : Set lzero
pr1 raise-unit-Set = unit
pr2 raise-unit-Set = is-set-unit

Recent changes