# The unit type

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

Created on 2022-01-27.

module foundation.unit-type where

Imports
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.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
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


## Properties

### The unit type is contractible

abstract
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}
where

abstract
is-equiv-terminal-map-is-contr :
is-contr A → is-equiv (terminal-map 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

equiv-unit-is-contr : is-contr A → A ≃ unit
pr1 (equiv-unit-is-contr H) = terminal-map A
pr2 (equiv-unit-is-contr H) = is-equiv-terminal-map-is-contr H

abstract
is-contr-is-equiv-const : is-equiv (terminal-map 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

abstract
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

abstract
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

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

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
pr1 (raise-unit-Prop l1) = raise-unit l1
pr2 (raise-unit-Prop l1) = is-prop-raise-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 : Set lzero
pr1 raise-unit-Set = unit
pr2 raise-unit-Set = is-set-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