← Docs

Universe polymorphism

Universes can be declared once and reused in the module.

Declarations

Declare one or more universe variables at the top of a file with \universe. Subsequent definitions in the file can use them wherever a universe is expected.

\universe 𝓤 𝓥

Using universe variables

Once declared, a definition that mentions 𝓤, 𝓥 becomed polymorphic, i.e. below definition id works as has a type {𝓤 : Universe} -> {A : 𝓤} -> (x : A) -> A:

\universe 𝓤

\let id {A : 𝓤} (x : A) : A => x

See also

• Inductive types