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
Imports
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
Idea
The unit type is inductively generated by one 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
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
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 = 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 abstract 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
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
Recent changes
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-13. Fredrik Bakke. Remove unused imports and fix some unaddressed comments (#621).
- 2023-05-03. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).