18.9. The Unit Type

The unit type is the canonical type with exactly one element, named unit and represented by the empty tuple (). It describes only a single value, which consists of said constructor applied to no arguments whatsoever.

Unit is analogous to void in languages derived from C: even though void has no elements that can be named, it represents the return of control flow from a function with no additional information. In functional programming, Unit is the return type of things that "return nothing". Mathematically, this is represented by a single completely uninformative value, as opposed to an empty type such as Empty, which represents unreachable code.

When programming with monads, Unit is especially useful. For any type α, m α represents an action that has side effects and returns a value of type α. The type m Unit represents an action that has some side effects but does not return a value.

There are two variants of the unit type:

Unit is a Type that exists in the smallest non-propositional universe.
PUnit is universe polymorphic and can be used in any non-propositional universe.

Behind the scenes, Unit is actually defined as PUnit.{1}. Unit should be preferred over PUnit when possible to avoid unnecessary universe parameters. If in doubt, use Unit until universe errors occur.

def

Unit : Type
Unit : Type

The canonical type with one element. This element is written ().

Unit has a number of uses:

It can be used to model control flow that returns from a function call without providing other information.
Monadic actions that return Unit have side effects without computing values.
In polymorphic types, it can be used to indicate that no data is to be stored in a particular field.

def

Unit.unit : Unit
Unit.unit : Unit

The only element of the unit type.

It can be written as an empty tuple: ().

inductive type

PUnit.{u} : Sort u
PUnit.{u} : Sort u

The canonical universe-polymorphic type with just one element.

It should be used in contexts that require a type to be universe polymorphic, thus disallowing Unit.

Constructors

unit.{u} : PUnit

The only element of the universe-polymorphic unit type.

18.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