Definition. Unit Type [hca/H003.lagda] The unit type is the type with only one element ★ : 𝟙 data 𝟙 : Type where ★ : 𝟙