Unit Type Properties
Table of Contents
1 Unit properties
module Lib.Prop.Unit where
This file defines some useful results of the Unit datatype.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.Data.Unit
1.2 Unicity of unit
By Unit-induction, it suffices to show that Path Unit star star is inhabited. The constant path suffices.
Unit/uniqueness (x : Unit) : Path Unit star x = ind-Unit (λx'. Path Unit star x') (refl Unit star) x Unit/uniqueness' (x : Unit) : Path Unit x star = inv Unit star x (Unit/uniqueness x)
1.3 Unit is a proposition
Any x, y : Unit are thus equal.
Unit/all-elements-equal (x : Unit) (y : Unit) : Path Unit x y = comp Unit x star (Unit/uniqueness' x) y (Unit/uniqueness y)
That is, Unit is a proposition.
Unit/is-prop : is-prop Unit = Unit/all-elements-equal Unit/Prop : Prop = ( Unit, Unit/is-prop)
1.4 Unit is contractible
This also shows that Unit is contractible.
Unit/is-contr : is-contr Unit = (star, Unit/uniqueness)
1.5 Unit is set
And that it is a set.
Unit/is-set : is-set Unit = is-contr→is-set Unit Unit/is-contr
1.6 The identity types of Unit are contractible
Unit/id-is-contr (x y : Unit) : is-contr (Path Unit x y) = (Unit/is-prop x y, λq. Unit/is-set x y (Unit/is-prop x y) q)