Polymorphic Universes¶
 Author
Matthieu Sozeau
General Presentation¶
Warning
The status of Universe Polymorphism is experimental.
This section describes the universe polymorphic extension of Coq. Universe polymorphism makes it possible to write generic definitions making use of universes and reuse them at different and sometimes incompatible universe levels.
A standard example of the difference between universe polymorphic and monomorphic definitions is given by the identity function:
 Definition identity {A : Type} (a : A) := a.
 identity is defined
By default, constant declarations are monomorphic, hence the identity
function declares a global universe (automatically named identity.u0
) for its domain.
Subsequently, if we try to selfapply the identity, we will get an
error:
 Fail Definition selfid := identity (@identity).
 The command has indeed failed with message: The term "@identity" has type "forall A : Type, A > A" while it is expected to have type "?A" (unable to find a welltyped instantiation for "?A": cannot ensure that "Type@{identity.u0+1}" is a subtype of "Type@{identity.u0}").
Indeed, the global level identity.u0
would have to be strictly smaller than
itself for this selfapplication to type check, as the type of
(@identity)
is forall (A : Type@{identity.u0}), A > A
whose type is itself
Type@{identity.u0+1}
.
A universe polymorphic identity function binds its domain universe level at the definition level instead of making it global.
 Polymorphic Definition pidentity {A : Type} (a : A) := a.
 pidentity is defined
 About pidentity.
 pidentity@{u} : forall {A : Type}, A > A pidentity is universe polymorphic Arguments pidentity {A}%type_scope a pidentity is transparent Expands to: Constant Top.pidentity
It is then possible to reuse the constant at different levels, like so:
 Polymorphic Definition selfpid := pidentity (@pidentity).
 selfpid is defined
Of course, the two instances of pidentity
in this definition are
different. This can be seen when the Printing Universes
flag is on:
 Set Printing Universes.
 Print selfpid.
 selfpid@{u u0} = pidentity@{u} (@pidentity@{u0}) : forall A : Type@{u0}, A > A (* u u0 = u0 < u *) Arguments selfpid A%type_scope a
Now pidentity
is used at two different levels: at the head of the
application it is instantiated at u
while in the argument position
it is instantiated at u0
. This definition is only valid as long as
u0
is strictly smaller than u
, as shown by the constraints.
Note that if we made selfpid
universe monomorphic, the two
universes (in this case u
and u0
) would be declared in the
global universe graph with names selfpid.u0
and selfpid.u1
.
Since the constraints would be global, Print selfpid.
will
not show them, however they will be shown by Print Universes
.
When printing pidentity
, we can see the universes it binds in
the annotation @{u}
. Additionally, when
Printing Universes
is on we print the "universe context" of
pidentity
consisting of the bound universes and the
constraints they must verify (for pidentity
there are no constraints).
Inductive types can also be declared universe polymorphic on universes appearing in their parameters or fields. A typical example is given by monoids. We first put ourselves in a mode where every declaration is universepolymorphic:
 Set Universe Polymorphism.
 Record Monoid := { mon_car :> Type; mon_unit : mon_car; mon_op : mon_car > mon_car > mon_car }.
 Monoid is defined mon_car is defined mon_unit is defined mon_op is defined
A monoid is here defined by a carrier type, a unit in this type and a binary operation.
 Print Monoid.
 Record Monoid@{u} : Type@{u+1} := Build_Monoid { mon_car : Type@{u}; mon_unit : mon_car; mon_op : mon_car > mon_car > mon_car }. (* u = *) Arguments Build_Monoid mon_car%type_scope mon_unit mon_op%function_scope Arguments mon_car m Arguments mon_unit m Arguments mon_op m _ _
The Monoid's carrier universe is polymorphic, hence it is possible to
instantiate it for example with Monoid
itself. First we build the
trivial unit monoid in any universe i >= Set
:
 Definition unit_monoid@{i} : Monoid@{i} := { mon_car := unit; mon_unit := tt; mon_op x y := tt }.
 unit_monoid is defined
Here we are using the fact that unit : Set
and by cumulativity,
any polymorphic universe is greater or equal to Set
.
From this we can build a definition for the monoid of monoids, where multiplication is given by the product of monoids. To do so, we first need to define a universepolymorphic variant of pairs:
 Record pprod@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{max(i,j)} := ppair { pfst : A; psnd : B }.
 pprod is defined pfst is defined psnd is defined
 Arguments ppair {A} {B}.
 Infix "**" := pprod (at level 40, left associativity) : type_scope.
 Notation "( x ; y ; .. ; z )" := (ppair .. (ppair x y) .. z) (at level 0) : core_scope.
The monoid of monoids uses the cartesian product of monoids as its operation:
 Definition monoid_op@{i} (m m' : Monoid@{i}) (x y : mon_car m ** mon_car m') : mon_car m ** mon_car m' := let (l, r) := x in let (l', r') := y in (mon_op m l l'; mon_op m' r r').
 monoid_op is defined
 Definition prod_monoid@{i} (m m' : Monoid@{i}): Monoid@{i} := { mon_car := (m ** m')%type; mon_unit := (mon_unit m; mon_unit m'); mon_op := (monoid_op m m') }.
 prod_monoid is defined
 Definition monoids_monoid@{i j  i < j} : Monoid@{j} := { mon_car := Monoid@{i}; mon_unit := unit_monoid@{i}; mon_op := prod_monoid@{i} }.
 monoids_monoid is defined
 Print monoids_monoid.
 monoids_monoid@{i j} = { mon_car := Monoid@{i}; mon_unit := unit_monoid@{i}; mon_op := prod_monoid@{i} } : Monoid@{j} (* i j = i < j *)
As one can see from the constraints, this monoid is “large”, it lives
in a universe strictly higher than its objects, monoids in the universes i
.
Polymorphic, Monomorphic¶
 Attribute universes(polymorphic= yesno?)¶
This boolean attribute can be used to control whether universe polymorphism is enabled in the definition of an inductive type. There is also a legacy syntax using the
Polymorphic
prefix (seelegacy_attr
) which, as shown in the examples, is more commonly used.When
universes(polymorphic=no)
is used, global universe constraints are produced, even when theUniverse Polymorphism
flag is on. There is also a legacy syntax using theMonomorphic
prefix (seelegacy_attr
).
 Flag Universe Polymorphism¶
This flag is off by default. When it is on, new declarations are polymorphic unless the
universes(polymorphic=no)
attribute is used to override the default.
Many other commands can be used to declare universe polymorphic or
monomorphic constants depending on whether the Universe
Polymorphism
flag is on or the universes(polymorphic)
attribute is used:
Lemma
,Axiom
, etc. can be used to declare universe polymorphic constants.Using the
universes(polymorphic)
attribute with theSection
command will locally set the polymorphism flag inside the section.Variable
,Context
,Universe
andConstraint
in a section support polymorphism. See Universe polymorphism and sections for more details.Using the
universes(polymorphic)
attribute with theHint Resolve
orHint Rewrite
commands will makeauto
/rewrite
use the hint polymorphically, not at a single instance.
Cumulative, NonCumulative¶
 Attribute universes(cumulative= yesno?)¶
Polymorphic inductive types, coinductive types, variants and records can be declared cumulative using this boolean attribute or the legacy
Cumulative
prefix (seelegacy_attr
) which, as shown in the examples, is more commonly used.This means that two instances of the same inductive type (family) are convertible based on the universe variances; they do not need to be equal.
When the attribtue is off, the inductive type is noncumulative even if the
Polymorphic Inductive Cumulativity
flag is on. There is also a legacy syntax using theNonCumulative
prefix (seelegacy_attr
).This means that two instances of the same inductive type (family) are convertible only if all the universes are equal.
 Error The cumulative attribute can only be used in a polymorphic context.¶
Using this attribute requires being in a polymorphic context, i.e. either having the
Universe Polymorphism
flag on, or having used theuniverses(polymorphic)
attribute as well.
Note
#[ universes(polymorphic= yes?), universes(cumulative= yesno?) ]
can be abbreviated into#[ universes(polymorphic= yes?, cumulative= yesno?) ]
.
 Flag Polymorphic Inductive Cumulativity¶
When this flag is on (it is off by default), it makes all subsequent polymorphic inductive definitions cumulative, unless the
universes(cumulative=no)
attribute is used to override the default. It has no effect on monomorphic inductive definitions.
Consider the examples below.
 Polymorphic Cumulative Inductive list {A : Type} :=  nil : list  cons : A > list > list.
 list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
 Set Printing Universes.
 Print list.
 Inductive list@{u} (A : Type@{u}) : Type@{max(Set,u)} := nil : list@{u}  cons : A > list@{u} > list@{u}. (* *u = *) Arguments list {A}%type_scope Arguments nil {A}%type_scope Arguments cons {A}%type_scope _ _
When printing list
, the universe context indicates the subtyping
constraints by prefixing the level names with symbols.
Because inductive subtypings are only produced by comparing inductives
to themselves with universes changed, they amount to variance
information: each universe is either invariant, covariant or
irrelevant (there are no contravariant subtypings in Coq),
respectively represented by the symbols =
, +
and *
.
Here we see that list
binds an irrelevant universe, so any two
instances of list
are convertible: \(E[Γ] ⊢ \mathsf{list}@\{i\}~A
=_{βδιζη} \mathsf{list}@\{j\}~B\) whenever \(E[Γ] ⊢ A =_{βδιζη} B\) and
this applies also to their corresponding constructors, when
they are comparable at the same type.
See Conversion rules for more details on convertibility and subtyping. The following is an example of a record with nontrivial subtyping relation:
 Polymorphic Cumulative Record packType := {pk : Type}.
 packType is defined pk is defined
 About packType.
 packType@{u} : Type@{u+1} (* +u = *) packType is universe polymorphic Expands to: Inductive Top.packType
packType
binds a covariant universe, i.e.
Looking back at the example of monoids, we can see that they are naturally covariant for cumulativity:
 Set Universe Polymorphism.
 Cumulative Record Monoid := { mon_car :> Type; mon_unit : mon_car; mon_op : mon_car > mon_car > mon_car }.
 Monoid is defined mon_car is defined mon_unit is defined mon_op is defined
 Set Printing Universes.
 Print Monoid.
 Record Monoid@{u} : Type@{u+1} := Build_Monoid { mon_car : Type@{u}; mon_unit : mon_car; mon_op : mon_car > mon_car > mon_car }. (* +u = *) Arguments Build_Monoid mon_car%type_scope mon_unit mon_op%function_scope Arguments mon_car m Arguments mon_unit m Arguments mon_op m _ _
This means that a monoid in a lower universe (like the unit monoid in set), can be seen as a monoid in any higher universe, without introducing explicit lifting.
 Definition unit_monoid : Monoid@{Set} := { mon_car := unit; mon_unit := tt; mon_op x y := tt }.
 unit_monoid is defined
 Monomorphic Universe i.
 Check unit_monoid : Monoid@{i}.
 unit_monoid : Monoid@{i} : Monoid@{i}
Finally, invariant universes appear when there is no possible subtyping relation between different instances of the inductive. Consider:
 Polymorphic Cumulative Record monad@{i} := { m : Type@{i} > Type@{i}; unit : forall (A : Type@{i}), A > m A }.
 monad is defined m is defined unit is defined
 Set Printing Universes.
 Print monad.
 Record monad@{i} : Type@{i+1} := Build_monad { m : Type@{i} > Type@{i}; unit : forall A : Type@{i}, A > m A }. (* =i = *) Arguments Build_monad (m unit)%function_scope Arguments m m _%type_scope Arguments unit m A%type_scope _
The universe of monad
is invariant due to its use on the left side of an arrow in
the m
field: one cannot lift or lower the level of the type constructor to build a
monad in a higher or lower universe.
Specifying cumulativity¶
The variance of the universe parameters for a cumulative inductive may be specified by the user.
For the following type, universe a
has its variance automatically
inferred (it is irrelevant), b
is required to be irrelevant,
c
is covariant and d
is invariant. With these annotations
c
and d
have less general variances than would be inferred.
 Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy.
 Dummy is defined Dummy_rect is defined Dummy_ind is defined Dummy_rec is defined Dummy_sind is defined
 About Dummy.
 Dummy@{a b c d} : Prop (* *a *b +c =d = *) Dummy is universe polymorphic Expands to: Inductive Top.Dummy
Insufficiently restrictive variance annotations lead to errors:
 Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}.
 The command has indeed failed with message: Incorrect variance for universe Top.81: expected * but cannot be less restrictive than +.
Example: Demonstration of universe variances
 Set Printing Universes.
 Set Universe Polymorphism.
 Set Polymorphic Inductive Cumulativity.
 Inductive Invariant @{=u} : Type@{u}.
 Invariant is defined Invariant_rect is defined Invariant_ind is defined Invariant_rec is defined Invariant_sind is defined
 Inductive Covariant @{+u} : Type@{u}.
 Covariant is defined Covariant_rect is defined Covariant_ind is defined Covariant_rec is defined Covariant_sind is defined
 Inductive Irrelevant@{*u} : Type@{u}.
 Irrelevant is defined Irrelevant_rect is defined Irrelevant_ind is defined Irrelevant_rec is defined Irrelevant_sind is defined
 Section Universes.
 Universe low high.
 Constraint low < high.
 (* An invariant universe blocks cumulativity from upper or lower levels. *)
 Axiom inv_low : Invariant@{low}.
 inv_low is declared
 Axiom inv_high : Invariant@{high}.
 inv_high is declared
 Fail Check (inv_low : Invariant@{high}).
 The command has indeed failed with message: The term "inv_low" has type "Invariant@{low}" while it is expected to have type "Invariant@{high}".
 Fail Check (inv_high : Invariant@{low}).
 The command has indeed failed with message: The term "inv_high" has type "Invariant@{high}" while it is expected to have type "Invariant@{low}".
 (* A covariant universe allows cumulativity from a lower level. *)
 Axiom co_low : Covariant@{low}.
 co_low is declared
 Axiom co_high : Covariant@{high}.
 co_high is declared
 Check (co_low : Covariant@{high}).
 co_low : Covariant@{high} : Covariant@{high} (* {} = low <= high *)
 Fail Check (co_high : Covariant@{low}).
 The command has indeed failed with message: The term "co_high" has type "Covariant@{high}" while it is expected to have type "Covariant@{low}".
 (* An irrelevant universe allows cumulativity from any level *)
 Axiom irr_low : Irrelevant@{low}.
 irr_low is declared
 Axiom irr_high : Irrelevant@{high}.
 irr_high is declared
 Check (irr_low : Irrelevant@{high}).
 irr_low : Irrelevant@{high} : Irrelevant@{high}
 Check (irr_high : Irrelevant@{low}).
 irr_high : Irrelevant@{low} : Irrelevant@{low}
 End Universes.
Example: A proof using cumulativity
 Set Universe Polymorphism.
 Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 Inductive eq@{i} {A : Type@{i}} (x : A) : A > Type@{i} := eq_refl : eq x x.
 eq is defined eq_rect is defined eq_ind is defined eq_rec is defined eq_sind is defined
 Print eq.
 Inductive eq@{i} (A : Type@{i}) (x : A) : A > Type@{i} := eq_refl : eq@{i} x x. (* *i = *) Arguments eq {A}%type_scope x _ Arguments eq_refl {A}%type_scope x
The universe of eq
is irrelevant here, hence proofs of equalities can
inhabit any universe. The universe must be big enough to fit A
.
 Definition funext_type@{a b e} (A : Type@{a}) (B : A > Type@{b}) := forall f g : (forall a, B a), (forall x, eq@{e} (f x) (g x)) > eq@{e} f g.
 funext_type is defined
 Section down.
 Universes a b e e'.
 Constraint e' < e.
 Lemma funext_down {A B} (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B.
 1 goal A : Type@{Top.125} B : A > Type@{Top.126} H : funext_type@{a b e} A B ============================ funext_type@{a b e'} A B
 Proof.
 exact H.
 No more goals.
 Defined.
 End down.
Cumulativity Weak Constraints¶
 Flag Cumulativity Weak Constraints¶
When set, which is the default, this flag causes "weak" constraints to be produced when comparing universes in an irrelevant position. Processing weak constraints is delayed until minimization time. A weak constraint between
u
andv
when neither is smaller than the other and one is flexible causes them to be unified. Otherwise the constraint is silently discarded.This heuristic is experimental and may change in future versions. Disabling weak constraints is more predictable but may produce arbitrary numbers of universes.
Global and local universes¶
Each universe is declared in a global or local context before it
can be used. To ensure compatibility, every global universe is set
to be strictly greater than Set
when it is introduced, while every
local (i.e. polymorphically quantified) universe is introduced as
greater or equal to Set
.
Conversion and unification¶
The semantics of conversion and unification have to be modified a little to account for the new universe instance arguments to polymorphic references. The semantics respect the fact that definitions are transparent, so indistinguishable from their bodies during conversion.
This is accomplished by changing one rule of unification, the first order approximation rule, which applies when two applicative terms with the same head are compared. It tries to shortcut unfolding by comparing the arguments directly. In case the constant is universe polymorphic, we allow this rule to fire only when unifying the universes results in instantiating a socalled flexible universe variables (not given by the user). Similarly for conversion, if such an equation of applicative terms fail due to a universe comparison not being satisfied, the terms are unfolded. This change implies that conversion and unification can have different unfolding behaviors on the same development with universe polymorphism switched on or off.
Minimization¶
Universe polymorphism with cumulativity tends to generate many useless
inclusion constraints in general. Typically at each application of a
polymorphic constant f
, if an argument has expected type Type@{i}
and is given a term of type Type@{j}
, a \(j ≤ i\) constraint will be
generated. It is however often the case that an equation \(j = i\) would
be more appropriate, when f
's universes are fresh for example.
Consider the following example:
 Polymorphic Definition pidentity {A : Type} (a : A) := a.
 pidentity is defined
 Definition id0 := @pidentity nat 0.
 id0 is defined
 Set Printing Universes.
 Print id0.
 id0@{} = pidentity@{Set} 0 : nat
This definition is elaborated by minimizing the universe of id0
to
level Set
while the more general definition would keep the fresh level
i
generated at the application of id
and a constraint that Set
\(≤ i\).
This minimization process is applied only to fresh universe variables.
It simply adds an equation between the variable and its lower bound if
it is an atomic universe (i.e. not an algebraic max() universe).
Explicit Universes¶
universe_name::=
qualid

Set

Prop
univ_annot::=
@{ univ_level_or_quality*  univ_level_or_quality*? }
univ_level_or_quality::=
Set

SProp

Prop

Type

_

qualid
univ_decl::=
@{ ident* ? ident* +?  univ_constraint*, +?? }
cumul_univ_decl::=
@{ ident* ? +=*? ident* +?  univ_constraint*, +?? }
univ_constraint::=
universe_name <=<= universe_name
The syntax has been extended to allow users to explicitly bind names to universes and explicitly instantiate polymorphic definitions.
 Command Universe ident+¶
 Command Universes ident+¶
In the monomorphic case, declares new global universes with the given names. Global universe names live in a separate namespace. The command supports the
universes(polymorphic)
attribute (or thePolymorphic
legacy attribute) only in sections, meaning the universe quantification will be discharged for each section definition independently. Error Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead.¶
 Command Constraint univ_constraint+,¶
Declares new constraints between named universes.
If consistent, the constraints are then enforced in the global environment. Like
Universe
, it can be used with theuniverses(polymorphic)
attribute (or thePolymorphic
legacy attribute) in sections only to declare constraints discharged at section closing time. One cannot declare a global constraint on polymorphic universes. Error Universe inconsistency.¶
 Error Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead¶
Printing universes¶
 Flag Printing Universes¶
Turn this flag on to activate the display of the actual level of each occurrence of
Type
. See Sorts for details. This wizard flag, in combination withPrinting All
can help to diagnose failures to unify terms apparently identical but internally different in the Calculus of Inductive Constructions.
 Command Print Sorted? Universes Subgraph ( qualid* )? string?¶
This command can be used to print the constraints on the internal level of the occurrences of \(\Type\) (see Sorts).
The
Subgraph
clause limits the printed graph to the requested names (adjusting constraints to preserve the implied transitive constraints between kept universes).The
Sorted
clause makes each universe equivalent to a numbered label reflecting its level (with a linear ordering) in the universe hierarchy.string
is an optional output filename. Ifstring
ends in.dot
or.gv
, the constraints are printed in the DOT language, and can be processed by Graphviz tools. The format is unspecified ifstring
doesn’t end in.dot
or.gv
. Ifstring
is a relative filename, it refers to the directory specified by the command line optionoutputdirectory
, if set (see Command line options) and otherwise, the current directory. UsePwd
to display the current directory.
Polymorphic definitions¶
For polymorphic definitions, the declaration of (all) universe levels introduced by a definition uses the following syntax:
 Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A.
 le is defined
 Print le.
 le@{i j} = fun A : Type@{i} => A : Type@{i} > Type@{j} (* i j = i <= j *) Arguments le A%type_scope
During refinement we find that j
must be larger or equal than i
, as we
are using A : Type@{i} <= Type@{j}
, hence the generated constraint. At the
end of a definition or proof, we check that the only remaining
universes are the ones declared. In the term and in general in proof
mode, introduced universe names can be referred to in terms. Note that
local universe names shadow global universe names. During a proof, one
can use Show Universes
to display the current context of universes.
It is possible to provide only some universe levels and let Coq infer the others
by adding a +
in the list of bound universe levels:
 Fail Definition foobar@{u} : Type@{u} := Type.
 The command has indeed failed with message: Universe Top.132 (Toplevel input, characters 38443848) is unbound.
 Definition foobar@{u +} : Type@{u} := Type.
 foobar is defined
 Set Printing Universes.
 Print foobar.
 foobar@{u u0} = Type@{u0} : Type@{u} (* u u0 = u0 < u *)
This can be used to find which universes need to be explicitly bound in a given definition.
Definitions can also be instantiated explicitly, giving their full instance:
 Check (pidentity@{Set}).
 pidentity@{Set} : ?A > ?A where ?A : [  Set]
 Monomorphic Universes k l.
 Check (le@{k l}).
 le@{k l} : Type@{k} > Type@{l} (* {} = k <= l *)
Usernamed universes and the anonymous universe implicitly attached to
an explicit Type
are considered rigid for unification and are never
minimized. Flexible anonymous universes can be produced with an
underscore or by omitting the annotation to a polymorphic definition.
 Check (fun x => x) : Type > Type.
 (fun x : Type@{Top.137} => x) : Type@{Top.137} > Type@{Top.138} : Type@{Top.137} > Type@{Top.138} (* {Top.138 Top.137} = Top.137 <= Top.138 *)
 Check (fun x => x) : Type > Type@{_}.
 (fun x : Type@{Top.139} => x) : Type@{Top.139} > Type@{Top.139} : Type@{Top.139} > Type@{Top.139} (* {Top.139} = *)
 Check le@{k _}.
 le@{k k} : Type@{k} > Type@{k}
 Check le.
 le@{Top.142 Top.142} : Type@{Top.142} > Type@{Top.142} (* {Top.142} = *)
 Flag Strict Universe Declaration¶
Turning this flag off allows one to freely use identifiers for universes without declaring them first, with the semantics that the first use declares it. In this mode, the universe names are not associated with the definition or proof once it has been defined. This is meant mainly for debugging purposes.
 Flag Private Polymorphic Universes¶
This flag, on by default, removes universes which appear only in the body of an opaque polymorphic definition from the definition's universe arguments. As such, no value needs to be provided for these universes when instantiating the definition. Universe constraints are automatically adjusted.
Consider the following definition:
 Lemma foo@{i} : Type@{i}.
 1 goal ============================ Type@{i}
 Proof. exact Type. Qed.
 No more goals.
 Print foo.
 foo@{i} = Type@{Top.145} : Type@{i} (* Public universes: i = Set < i Private universes: {Top.145} = Top.145 < i *)
The universe
Top.xxx
for theType
in the body cannot be accessed, we only care that one exists for any instantiation of the universes appearing in the type offoo
. This is guaranteed when the transitive constraintSet <= Top.xxx < i
is verified. Then when using the constant we don't need to put a value for the inner universe: Check foo@{_}.
 foo@{Top.146} : Type@{Top.146} (* {Top.146} = Set < Top.146 *)
and when not looking at the body we don't mention the private universe:
 About foo.
 foo@{i} : Type@{i} (* i = Set < i *) foo is universe polymorphic foo is opaque Expands to: Constant Top.foo
To recover the same behavior with regard to universes as
Defined
, thePrivate Polymorphic Universes
flag may be unset: Unset Private Polymorphic Universes.
 Lemma bar : Type. Proof. exact Type. Qed.
 1 goal ============================ Type@{Top.147} No more goals.
 About bar.
 bar@{u u0} : Type@{u} (* u u0 = u0 < u *) bar is universe polymorphic bar is opaque Expands to: Constant Top.bar
 Fail Check bar@{_}.
 The command has indeed failed with message: Universe instance length is 1 but should be 2.
 Check bar@{_ _}.
 bar@{Top.150 Top.151} : Type@{Top.150} (* {Top.151 Top.150} = Top.151 < Top.150 *)
Note that named universes are always public.
 Set Private Polymorphic Universes.
 Unset Strict Universe Declaration.
 Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed.
 1 goal ============================ Type@{outer} No more goals.
 About baz.
 baz@{outer inner} : Type@{outer} (* outer inner = inner < outer *) baz is universe polymorphic baz is opaque Expands to: Constant Top.baz
Sort polymorphism¶
Quantifying over universes does not allow instantiation with Prop
or SProp
. For instance
 Polymorphic Definition type@{u} := Type@{u}.
 type is defined
 Fail Check type@{Prop}.
 The command has indeed failed with message: Universe instances cannot contain nonSet small levels, polymorphic universe instances must be greater or equal to Set.
To be able to instantiate a sort with Prop
or SProp
, we must
quantify over sort qualities. Definitions which quantify over
sort qualities are called sort polymorphic.
All sort quality variables must be explicitly bound.
 Polymorphic Definition sort@{s  u } := Type@{su}.
 sort is defined
To help the parser, both 
in the univ_decl
are required.
Sort quality variables of a sort polymorphic definition may be
instantiated by the concrete values SProp
, Prop
and Type
or by a
bound variable.
Instantiating s
in Type@{su}
with the impredicative Prop
or
SProp
produces Prop
or SProp
respectively regardless of the
instantiation fof u
.
 Eval cbv in sort@{PropSet}.
 = Prop : Type
 Eval cbv in sort@{TypeSet}.
 = Set : Type
When no explicit instantiation is provided or _
is used, a temporary
variable is generated. Temporary sort variables are instantiated with
Type
if not unified with another quality when universe minimization
runs (typically at the end of a definition).
Check
and Eval
run minimization so we cannot use them to
witness these temporary variables.
 Goal True.
 1 goal ============================ True
 Set Printing Universes.
 let c := constr:(sort) in idtac c.
 sort@{α13  Top.156}
Note
We recommend you do not name explicitly quantified sort variables
α
followed by a number as printing will not distinguish between
your bound variables and temporary variables.
Sort polymorphic inductives may be declared when every instantiation is valid.
Elimination at a given universe instance requires that elimination is
allowed at every ground instantiation of the sort variables in the
instance. Additionally if the output sort at the given universe
instance is sort polymorphic, the return type of the elimination must
be at the same quality. These restrictions ignore Definitional
UIP
.
For instance
 Set Universe Polymorphism.
 Inductive Squash@{su} (A:Type@{su}) : Prop := squash (_:A).
 Squash is defined Squash_ind is defined Squash_sind is defined
Elimination to Prop
and SProp
is always allowed, so Squash_ind
and Squash_sind
are automatically defined.
Elimination to Type
is not allowed with variable s
, because the
instantiation s := Type
does not allow elimination to Type
.
However elimination to Type
or to a polymorphic sort with s := Prop
is allowed:
 Definition Squash_Prop_rect A (P:Squash@{Prop_} A > Type) (H:forall x, P (squash _ x)) : forall s, P s := fun s => match s with squash _ x => H x end.
 Squash_Prop_rect is defined
 Definition Squash_Prop_srect@{su +} A (P:Squash@{Prop_} A > Type@{su}) (H:forall x, P (squash _ x)) : forall s, P s := fun s => match s with squash _ x => H x end.
 Squash_Prop_srect is defined
Note
Since inductive types with sort polymorphic output may only be polymorphically eliminated to the same sort quality, containers such as sigma types may be better defined as primitive records (which do not have this restriction) when possible.
 Set Primitive Projections.
 Record sigma@{su v} (A:Type@{su}) (B:A > Type@{sv}) : Type@{smax(u,v)} := pair { pr1 : A; pr2 : B pr1 }.
 sigma is defined pr1 is defined pr2 is defined
Universe polymorphism and sections¶
Variables
, Context
, Universe
and
Constraint
in a section support polymorphism. This means that
the universe variables and their associated constraints are discharged
polymorphically over definitions that use them. In other words, two
definitions in the section sharing a common variable will both get
parameterized by the universes produced by the variable declaration.
This is in contrast to a “mononorphic” variable which introduces
global universes and constraints, making the two definitions depend on
the same global universes associated with the variable.
It is possible to mix universe polymorphism and monomorphism in sections, except in the following ways:
no monomorphic constraint may refer to a polymorphic universe:
 Section Foo.
 Polymorphic Universe i.
 Fail Constraint i = i.
 The command has indeed failed with message: Cannot add monomorphic constraints which refer to section polymorphic universes.
This includes constraints implicitly declared by commands such as
Variable
, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): Fail Variable A : (Type@{i} : Type).
 The command has indeed failed with message: Cannot add monomorphic constraints which refer to section polymorphic universes.
 Polymorphic Variable A : (Type@{i} : Type).
 A is declared
(in the above example the anonymous
Type
constrains polymorphic universei
to be strictly smaller.)no monomorphic constant or inductive may be declared if polymorphic universes or universe constraints are present.
These restrictions are required in order to produce a sensible result when closing the section (the requirement on constants and inductive types is stricter than the one on constraints, because constants and inductives are abstracted by all the section's polymorphic universes and constraints).