Unit

Theory

A unit type is a type with only one term. We use \(\mathbb{1}\) to denote a unit type.