The unit type

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

Created on 2022-01-27.
Last modified on 2025-02-14.

module foundation.unit-type where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.diagonal-maps-of-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.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.retractions
open import foundation-core.sets
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

Idea

The unit type is a type inductively generated by a single point.

Definition

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

module _
  {l : Level} (A : UU l)
  where

  terminal-map : A → unit
  terminal-map = const A star

Points as maps out of the unit type

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

  point : A → (unit → A)
  point = diagonal-exponential A unit

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

raise-terminal-map : {l1 l2 : Level} (A : UU l1) → A → raise-unit l2
raise-terminal-map {l2 = l2} A = const A raise-star

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

inv-compute-raise-unit : (l : Level) → raise-unit l ≃ unit
inv-compute-raise-unit l = inv-compute-raise l unit

Properties

The unit type is contractible

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

abstract
  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

Any contractible type is equivalent to the unit type

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

  is-equiv-terminal-map-is-contr : is-contr A → is-equiv (terminal-map A)
  is-equiv-terminal-map-is-contr H =
    is-equiv-is-invertible (λ _ → center H) (λ _ → refl) (contraction H)

  equiv-unit-is-contr : is-contr A → A ≃ unit
  equiv-unit-is-contr H = terminal-map A , is-equiv-terminal-map-is-contr H

  is-contr-retraction-terminal-map : retraction (terminal-map A) → is-contr A
  is-contr-retraction-terminal-map (h , H) = h star , H

  is-contr-is-equiv-terminal-map : is-equiv (terminal-map A) → is-contr A
  is-contr-is-equiv-terminal-map H =
    is-contr-retraction-terminal-map (retraction-is-equiv H)

  is-contr-equiv-unit : A ≃ unit → is-contr A
  is-contr-equiv-unit e = (map-inv-equiv e star , is-retraction-map-inv-equiv e)

  is-contr-equiv-unit' : unit ≃ A → is-contr A
  is-contr-equiv-unit' e = (map-equiv e star , is-section-map-inv-equiv e)

Any contractible type is equivalent to the raised unit type

module _
  {l1 l2 : Level} {A : UU l1}
  where

  is-equiv-raise-terminal-map-is-contr :
    is-contr A → is-equiv (raise-terminal-map {l2 = l2} A)
  is-equiv-raise-terminal-map-is-contr H =
    is-equiv-is-invertible
      ( λ _ → center H)
      ( λ where (map-raise x) → refl)
      ( contraction H)

  equiv-raise-unit-is-contr : is-contr A → A ≃ raise-unit l2
  equiv-raise-unit-is-contr H =
    raise-terminal-map A , is-equiv-raise-terminal-map-is-contr H

  is-contr-retraction-raise-terminal-map :
    retraction (raise-terminal-map {l2 = l2} A) → is-contr A
  is-contr-retraction-raise-terminal-map (h , H) = h raise-star , H

  is-contr-is-equiv-raise-terminal-map :
    is-equiv (raise-terminal-map {l2 = l2} A) → is-contr A
  is-contr-is-equiv-raise-terminal-map H =
    is-contr-retraction-raise-terminal-map (retraction-is-equiv H)

  is-contr-equiv-raise-unit : A ≃ raise-unit l2 → is-contr A
  is-contr-equiv-raise-unit e =
    ( map-inv-equiv e raise-star) ,
    ( λ x →
      ap (map-inv-equiv e) (eq-is-contr is-contr-raise-unit) ∙
      is-retraction-map-inv-equiv e x)

The unit type is a proposition

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

unit-Prop : Prop lzero
unit-Prop = unit , is-prop-unit

abstract
  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
raise-unit-Prop l1 = raise-unit l1 , is-prop-raise-unit

The unit type is a set

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

unit-Set : Set lzero
unit-Set = unit , is-set-unit

abstract
  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 : (l1 : Level) → Set l1
raise-unit-Set l1 = raise-unit l1 , is-set-raise-unit

All parallel maps into unit are equal

module _
  {l : Level} {A : UU l} {f g : A → unit}
  where

  eq-map-into-unit : f ＝ g
  eq-map-into-unit = refl

The map point x is injective for every x

module _
  {l : Level} {A : UU l} (x : A)
  where

  is-injective-point : is-injective (point x)
  is-injective-point _ = refl

  point-injection : injection unit A
  pr1 point-injection = point x
  pr2 point-injection = is-injective-point

The map point x has a retraction for every x

module _
  {l : Level} {A : UU l} (x : A)
  where

  retraction-point : retraction (point x)
  retraction-point = terminal-map A , refl-htpy

Recent changes