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.
Last modified on 2024-09-06.
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-terminal-map : is-equiv (terminal-map A) → is-contr A pr1 (is-contr-is-equiv-terminal-map ((g , G) , (h , H))) = h star pr2 (is-contr-is-equiv-terminal-map ((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 : (l1 : Level) → Set l1 pr1 (raise-unit-Set l1) = raise-unit l1 pr2 (raise-unit-Set 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
Recent changes
- 2024-09-06. Fredrik Bakke. Colocal types (#1089).
- 2024-08-29. Fernando Chu, Fredrik Bakke and Egbert Rijke. Cones, limits and reduced coslices of precats (#1161).
- 2024-04-11. Fredrik Bakke. Refactor diagonals (#1096).
- 2024-03-02. Fredrik Bakke. Factor out standard pullbacks (#1042).
- 2024-01-10. Fredrik Bakke. Use
point x
instead ofconst unit X x
(#994).