11.9. The Unit Type

The unit type is the least informative type. It is used when a value is needed, but no further information is relevant. There are two varieties of the unit type:

If in doubt, use Unit until universe errors occur.

🔗def
Unit : Type

The unit type, the canonical type with one element, named unit or (). In other words, it describes only a single value, which consists of said constructor applied to no arguments whatsoever. The Unit type is similar to void in languages derived from C.

Unit is actually defined as PUnit.{1} where PUnit is the universe polymorphic version. The Unit should be preferred over PUnit where possible to avoid unnecessary universe parameters.

In functional programming, Unit is the return type of things that "return nothing", since a type with one element conveys no additional information. When programming with monads, the type m Unit represents an action that has some side effects but does not return a value, while m α would be an action that has side effects and returns a value of type α.

🔗def
Unit.unit : Unit

Unit.unit : Unit is the canonical element of the unit type. It can also be written as ().

🔗inductive type
PUnit.{u} : Sort u

The unit type, the canonical type with one element, named unit or (). This is the universe-polymorphic version of Unit; it is preferred to use Unit instead where applicable. For more information about universe levels: Types as objects

Constructors

  • unit.{u} : PUnit

    PUnit.unit : PUnit is the canonical element of the unit type.

11.9.1. Definitional Equality

Unit-like types are inductive types that have a single constructor which takes no non-proof parameters. PUnit is one such type. All elements of unit-like types are definitionally equal to all other elements.

Definitional Equality of Unit

Every term with type Unit is definitionally equal to every other term with type Unit:

example (e1 e2 : Unit) : e1 = e2 := rfl
Definitional Equality of Unit-Like Types

Both CustomUnit and AlsoUnit are unit-like types, with a single constructor that takes no parameters. Every pair of terms with either type is definitionally equal.

inductive CustomUnit where | customUnit example (e1 e2 : CustomUnit) : e1 = e2 := rfl structure AlsoUnit where example (e1 e2 : AlsoUnit) : e1 = e2 := rfl

Types with parameters, such as WithParam, are also unit-like if they have a single constructor that does not take parameters.

inductive WithParam (n : Nat) where | mk example (x y : WithParam 3) : x = y := rfl

Constructors with non-proof parameters are not unit-like, even if the parameters are all unit-like types.

inductive NotUnitLike where | mk (u : Unit) example (e1 e2 : NotUnitLike) : e1 = e2 := type mismatch rfl has type ?m.13 = ?m.13 : Prop but is expected to have type e1 = e2 : Proprfl 
type mismatch
  rfl
has type
  ?m.13 = ?m.13 : Prop
but is expected to have type
  e1 = e2 : Prop

Constructors of unit-like types may take parameters that are proofs.

inductive ProofUnitLike where | mk : 2 = 2 → ProofUnitLike example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl