\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Polymorphic Universes

Author:

  Matthieu Sozeau

## General Presentation

Warning

The status of Universe Polymorphism is experimental.

This section describes the universe polymorphic extension of Rocq. 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 self-apply 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 well-typed 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 self-application 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 Declared in toplevel input, characters 168-177

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 universe-polymorphic:

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 universe-polymorphic 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= yes​no?)

  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 (see `legacy_attr`) which, as shown in the examples, is more commonly used.

  When `universes(polymorphic=no)` is used, global universe constraints are produced, even when the `Universe Polymorphism` flag is on. There is also a legacy syntax using the `Monomorphic` prefix (see `legacy_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 the `Section` command will locally set the polymorphism flag inside the section.

- `Variable`, `Context`, `Universe` and `Constraint` in a section support polymorphism. See Universe polymorphism and sections for more details.

- Using the `universes(polymorphic)` attribute with the `Hint Resolve` or `Hint Rewrite` commands will make `auto` / `rewrite` use the hint polymorphically, not at a single instance.

## Cumulative, NonCumulative

Attribute universes(cumulative= yes​no?)

  Polymorphic inductive types, coinductive types, variants and records can be declared cumulative using this boolean attribute or the legacy `Cumulative` prefix (see `legacy_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 non-cumulative even if the `Polymorphic Inductive Cumulativity` flag is on. There is also a legacy syntax using the `NonCumulative` prefix (see `legacy_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 the `universes(polymorphic)` attribute as well.

  Note

  `#[ universes(polymorphic= yes?), universes(cumulative= yes​no?) ]` can be abbreviated into `#[ universes(polymorphic= yes?, cumulative= yes​no?) ]`.

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 Rocq), 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 non-trivial 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 Declared in toplevel input, characters 1606-1614

`packType` binds a covariant universe, i.e.

\[E[Γ] ⊢ \mathsf{packType}@\{i\} ≤_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j\]

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 Declared in toplevel input, characters 2172-2177

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.99: 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}" (universe inconsistency: Cannot enforce low = high because low < 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}" (universe inconsistency: Cannot enforce high = low because low < high).

(* 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}" (universe inconsistency: Cannot enforce high <= low because low < high).

(* 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.139} B : A -> Type@{Top.140} 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` and `v` 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 short-cut 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 so-called 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).

Flag Universe Minimization ToSet

  Turning this flag off (it is on by default) disallows minimization to the sort `Set` and only collapses floating universes between themselves.

## Explicit Universes

universe_name`::=`qualid`````|`Set`````|`Prop``univ_annot`::=`@{ univ_level_or_quality* |​; univ_level_or_quality*? }``univ_level_or_quality`::=`0`````|`Set`````|`SProp`````|`Prop`````|`Type`````|`_`````|`qualid``sort_quality_var`::=`Prop`````|`SProp`````|`Type`````|`qualid``univ_decl`::=`@{ ident* |​;? ident* +? | sort_constraint*, +?? }``cumul_univ_decl`::=`@{ ident* |​;? +​=​*? ident* +? | sort_constraint*, +?? }``sort_constraint`::=`universe_name <​=​<= universe_name`````|`sort_quality_var -> sort_quality_var``

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 the `Polymorphic` 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 sort_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 the `universes(polymorphic)` attribute (or the `Polymorphic` legacy attribute) in sections only to declare constraints discharged at section closing time. One cannot declare a global constraint on polymorphic universes.

  Error Undeclared universe ident.
  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 with `Printing 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 ( debug_univ_name* )? With​Without Constraint Sources? string?
  debug_univ_name`::=`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). `debug_univ_name` is `qualid` for named universes (e.g. `eq.u0`), and `string` for raw universe expressions (e.g. `"Stdlib.Init.Logic.1"`).

  By default when printing a subgraph `Print Universes` attempts to find and print the source of the constraints. This can be controlled by providing `With Constraint Sources` or `Without Constraint Sources`.

  Monomorphic Universes a b c.
  Monomorphic Definition make_a_le_b (F:Type@{b} -> Prop) (X:Type@{a}) := F X.
    make_a_le_b is defined
  Monomorphic Definition make_b_le_c (F:Type@{c} -> Prop) (X:Type@{b}) := F X.
    make_b_le_c is defined
  Monomorphic Definition make_c_le_a (F:Type@{a} -> Prop) (X:Type@{c}) := F X.
    make_c_le_a is defined
  Print Universes Subgraph (a c).
    Set < a < c c = a (because c <=(from make_c_le_a) a <=(from make_a_le_b) b <=(from make_b_le_c) c)

  Note

  The integer in raw universe expressions is extremely unstable, so raw universe expressions should not be used outside debugging sessions.

  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. If `string` ends in `.dot` or `.gv`, the constraints are printed in the DOT language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in `.dot` or `.gv`. If `string` is a relative filename, it refers to the directory specified by the command line option `-output-directory`, if set (see Command line options) and otherwise, the current directory. Use `Pwd` 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 Rocq 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.149 (Toplevel input, characters 4348-4352) 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 *)

User-named 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.154} => x) : Type@{Top.154} -> Type@{Top.155} : Type@{Top.154} -> Type@{Top.155} (* {Top.155 Top.154} |= Top.154 <= Top.155 *)
Check (fun x => x) : Type -> Type@{_}.
  (fun x : Type@{Top.156} => x) : Type@{Top.156} -> Type@{Top.156} : Type@{Top.156} -> Type@{Top.156} (* {Top.156} |= *)
Check le@{k _}.
  le@{k k} : Type@{k} -> Type@{k}
Check le.
  le@{Top.159 Top.159} : Type@{Top.159} -> Type@{Top.159} (* {Top.159} |= *)

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. 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.162} : Type@{i} (* Public universes: i |= Set < i Private universes: {Top.162} |= Top.162 < i *)

  The universe `Top.xxx` for the `Type` in the body cannot be accessed, we only care that one exists for any instantiation of the universes appearing in the type of `foo`. This is guaranteed when the transitive constraint `Set <= 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.163} : Type@{Top.163} (* {Top.163} |= Set < Top.163 *)

  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 Declared in toplevel input, characters 4612-4615

  To recover the same behavior with regard to universes as `Defined`, the `Private Polymorphic Universes` flag may be unset:

  Unset Private Polymorphic Universes.
  Lemma bar : Type. Proof. exact Type. Qed.
    1 goal ============================ Type@{Top.164} 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 Declared in toplevel input, characters 4736-4739
  Fail Check bar@{_}.
    The command has indeed failed with message: Universe instance length for bar is 1 but should be 2.
  Check bar@{_ _}.
    bar@{Top.167 Top.168} : Type@{Top.167} (* {Top.168 Top.167} |= Top.168 < Top.167 *)

  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 Declared in toplevel input, characters 4896-4899

## 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 non-Set 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@{s;u}.
  sort is defined

Note

The following deprecated syntax is equivalent:

Polymorphic Definition sort'@{s | u |} := Type@{s|u}.
  Toplevel input, characters 32-33: > Polymorphic Definition sort'@{s | u |} > ^ Warning: Separating sorts from universes with "|" is deprecated. Use ";" instead. [deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default] Toplevel input, characters 49-50: > Polymorphic Definition sort'@{s | u |} := Type@{s|u}. > ^ Warning: Separating sorts from universes with "|" is deprecated. Use ";" instead. [deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default] 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@{s;u}` with the impredicative `Prop` or `SProp` produces `Prop` or `SProp` respectively regardless of the instantiation of `u`.

Eval cbv in sort@{Prop;Set}.
  = Prop : Type
Eval cbv in sort@{Type;Set}.
  = 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@{α14 ; Top.174}

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 of Sort-Polymorphic Inductives

Sort-polymorphic inductives follow rules for their elimination, both when the target sort is polymorphic or not. We illustrate the first case on the following example:

Set Universe Polymorphism.
Inductive Squash@{s;u} (A:Type@{s;u}) : Prop := squash (_:A).
  Squash is defined Squash_ind is defined Squash_sind is defined

Here, 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@{s;u +} A (P:Squash@{Prop;_} A -> Type@{s;u}) (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

In fact, for a given universe instance, elimination is allowed if:

- it is allowed for every ground instantiation of the sort variables in the instance, or

- the output sort at the given universe instance is sort polymorphic and the return type of the elimination is at the same quality.

For instance, for the following inductive, elimination is not allowed unless the target sort of the inductive matches the sort it is eliminated to.

Inductive sum@{sl sr s;ul ur} (A:Type@{sl;ul}) (B:Type@{sr;ur}) : Type@{s;max(ul,ur)} := | inl (_:A) | inr (_:B).
  sum is defined

Arguments inl {_ _} _.
Arguments inr {_ _} _.

Fail Definition sum_elim@{sl sr s s';ul ur u'|} (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'}) (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y)) (v : sum@{sl sr s;ul ur} A B) : P v := match v with | inl x => fl x | inr y => fr y end.
  The command has indeed failed with message: Elimination constraints are not implied by the ones declared: s -> s'

As this greatly inhibits the possibilities of sort polymorphism, we have introduced elimination constraints to manage these cases. Here, the annotation `s -> s'` can be added to tell Rocq that the definition is allowed for every sorts `s`, `s'` such that `s` eliminates into `s'`.

Definition sum_elim@{sl sr s s';ul ur u'|s -> s'} (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'}) (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y)) (v : sum@{sl sr s;ul ur} A B) : P v := match v with | inl x => fl x | inr y => fr y end.
  sum_elim is defined

It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and `Prop` or `Prop` and `SProp`, but cannot be instantiated to e.g., `Prop` and `Type` or `SProp` and `Prop`.

Check sum_elim@{_ _ Type Prop;_ _ _}.
  sum_elim : forall (A B : Type) (P : sum A B -> Prop), (forall x : A, P (inl x)) -> (forall y : B, P (inr y)) -> forall v : sum A B, P v
Check sum_elim@{_ _ Prop SProp;_ _ _}.
  sum_elim : forall (A B : Type) (P : sum A B -> SProp), (forall x : A, P (inl x)) -> (forall y : B, P (inr y)) -> forall v : sum A B, P v
Fail Check sum_elim@{_ _ Prop Type;_ _ _}.
  The command has indeed failed with message: The quality constraints are inconsistent: cannot enforce Prop -> Type because it would identify Type and Prop which is inconsistent. This is introduced by the constraints Prop -> Type
Fail Check sum_elim@{_ _ SProp Prop;_ _ _}.
  The command has indeed failed with message: The quality constraints are inconsistent: cannot enforce SProp -> Prop because it would identify Prop and SProp which is inconsistent. This is introduced by the constraints SProp -> Prop

Note

As with universe level constraints, elimination constraints can be elaborated automatically if the constraints are denoted extensible with `+` or if they are totally omitted. For instance, the two following definitions are legal.

Definition sum_elim_ext@{sl sr s s';ul ur u'|+} (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'}) (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y)) (v : sum@{sl sr s;ul ur} A B) : P v := match v with | inl x => fl x | inr y => fr y end.
  sum_elim_ext is defined
Definition sum_elim_elab@{sl sr s s';ul ur u'} (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'}) (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y)) (v : sum@{sl sr s;ul ur} A B) : P v := match v with | inl x => fl x | inr y => fr y end.
  sum_elim_elab is defined

Note

These restrictions ignore `Definitional UIP`.

Flag Printing Sort Qualities

  By default when `Printing Universes` is on, sorts at floating sort qualities will print their quality. Turning this flag off will instead print them as though the quality was `Type` (which it will become at the end of the definition unless it is unified with another rigid quality).

## Explicit Sorts

Similar to universes, fresh global sorts can be declared with the `Sort`, and elimination constraint on global sorts can be declared with the `Constraint`.

Command Sort ident+
Command Sorts ident+

  > In the monomorphic case, declares new global sort qualities with the given names. Global quality names live in their own namespace. Inside sections, the command respects the `Universe Polymorphism` flag, either set globally or locally through the `universes(polymorphic)` attribute (or the `Polymorphic` legacy attribute), meaning the sort quantification will be discharged for each section definition independently. Polymorphic sort qualities are forbidden outside sections.

  Error Polymorphic sorts can only be declared inside sections, use #[universe(polymorphic=no)] Sort in order to declare a global sort.

    Generated when a `Sort` command is issued outside a section with universe polymorphism set. Either scope the `Sort` with an enclosing `Section` or be explicit about creating a global sort by turning universe polymorphism off.

  Error Cannot declare global sort qualities inside module types.

    The `Sort` command is not supported inside module types.

Command Print Sorts

  > Print the list of global named sorts in the current global environment. Use `Show Universes` to print sort variables local to a proof context.

  Set Universe Polymorphism.
  (* A global sort named g. *) #[universes(polymorphic=no)] Sort g.
  Print Sorts.
    g
  (* Universe of g-sorted type. *) Definition G@{l|} : Type@{l+1} := Type@{g;l}.
    G is defined
  Section LocalSorts.
  Sort u v w.
  Definition arr2@{l|} (A : Type@{u;l}) (B : Type@{v;l}) (C : Type@{w;l}) : Type@{w;l} := A -> B -> C.
    arr2 is defined
  Print Sorts.
    g u v w
  Sort x y.
  Definition arr1@{l|} (X : Type@{x;l}) (Y : Type@{y;l}) : Type@{y;l} := X -> Y.
    arr1 is defined
  Print Sorts.
    g u v w x y
  End LocalSorts.
  (* The sorts u, v, w, x and y are no longer present. *) Print Sorts.
    g
  (* Equivalent definition of arr2 outside the section LocalSorts. *) Definition arr2'@{u v w ; l |} (A : Type@{u;l}) (B : Type@{v;l}) (C : Type@{w;l}) : Type@{w;l} := A -> B -> C.
    arr2' is defined
  (* All sort declarations of the section are bound, even the unused one. *) About arr1.
    arr1@{u v w x y ; l} : Type@{x ; _} -> Type@{y ; _} -> Type@{y ; _} arr1 is universe polymorphic Arguments arr1 (X Y)%_type_scope arr1 is transparent Expands to: Constant Top.arr1 Declared in toplevel input, characters 7826-7830

## Template polymorphism

Template polymorphism is a variant of universe polymorphism for inductive types (and inductive families) whose shape allows inferring the universe instance from the parameters. Template polymorphic inductives appear in terms without an explicit universe instance (for instance if `prod` is template polymorphic then `prod nat nat` is a fully explicit term, if it is universe polymorphic it would be `prod@{Set Set} nat nat`).

Additionally template polymorphism implements sort polymorphism restricted to the sorts `Prop` and `Type` (for instance `prod True True : Prop`).

### Template polymorphic inductive declarations

A template polymorphic inductive is polymorphic over some specific universe levels and sort variables which are introduced by the inductive's declaration. These levels are called "template (polymorphic) levels" and sorts.

A type of the shape `Type@{s;u}` or `forall ..., Type@{s;u}` (i.e. a type of types or type families) is called an "arity". `Type@{s;u}` is the "conclusion" of the arity. The type of an inductive is always an arity, and for short we say "the inductive's conclusion" instead of "the inductive's type's conclusion". Template polymorphism also involves parameters of the inductive whose types are arities.

An inductive may be template polymorphic when

- it is the only inductive of its block (the combination of template polymorphism and mutual inductives is not supported).

- the template levels appear linearly in the conclusions of parameters which are arities. Such conclusions must have only that level as its universe (i.e. `Type@{s;u}` where `u` is a template level, not `Type@{s;max(u,v)}` or `Type@{u+1}`). Each template level is said to be "bound" by the parameter in whose type it appears.

- the template levels may also appear in the inductive's conclusion, and appear nowhere else (not in non-arity parameters, not in the domains of arity parameters, not in the indices, and not in the constructor arguments and return types).

- template levels which appear in the inductive's conclusion do not appear with an increment (i.e. if `u` is a template level it does not appear as `u+1`).

  This restriction prevents generating increments higher than 1 by applying template inductives to themselves, i.e. if `I : Type@{u} -> Type@{u + 1}` was template polymorphic and `X:Type@{i}` then `I (I X) : Type@{i + 2}`. It is necessary as the current universe checking cannot handle such increments properly, but this restriction may be removed in the future.

- the template sorts appear in the conclusions of parameters (not necessarily linearly), may appear in the inductive's conclusion, and appear nowhere else.

- for each template universe `u`, there are no constraints of the form `v <= u` ("no constraints from below").

These requirements are more than sufficient to ensure that if the inductive was declared universe polymorphic and cumulative then all template levels would be irrelevant. The "no constraints from below" requirement is needed for subject reduction (preservation of typing by reduction) in terms involving partially applied template polymorphic inductives. Linearity of template universes and not supporting mutual inductives make implementation of template polymorphism easier.

Warning

The restriction that universes are introduced by the inductive declaration prevents inductive types declared in sections from being template-polymorphic on universes introduced previously in the section: they cannot parameterize over the universes introduced with section variables that become parameters at section closing time, as these may be shared with other definitions from the same section which can impose constraints on them.

Note

Currently user syntax does not support explicit sort polymorphism annotations (`@{s;...}`) in template polymorphic declarations. The sorts must be left implicit and will be automatically inferred.

Example

Inductive option (A:Type) : Type := | None : option A | Some : A -> option A.
  option is defined option_rect is defined option_ind is defined option_rec is defined option_sind is defined
Inductive prod A B := pair : A -> B -> prod A B.
  prod is defined prod_rect is defined prod_ind is defined prod_rec is defined prod_sind is defined

Set Printing Universes.
About option.
  option : Type@{option.u0} -> Type@{max(Set,option.u0)} option is template universe polymorphic on option.u0 (cannot be instantiated to Prop) Arguments option A%_type_scope Expands to: Inductive Top.option Declared in toplevel input, characters 8343-8349
About prod.
  prod : Type@{prod.u0} -> Type@{prod.u1} -> Type@{max(prod.u0,prod.u1)} prod is template universe polymorphic on prod.u1 prod.u0 (can be instantiated to Prop) Arguments prod (A B)%_type_scope Expands to: Inductive Top.prod Declared in toplevel input, characters 8421-8425

Since the sort polymorphism of template inductives cannot be specified in the user syntax, it is instead described by the "can/cannot be instantiated to `Prop`" mention in `About`'s output. Since `option` has 2 constructors, it cannot be instantiated to `Prop` i.e. it is not sort polymorphic.

### Using template polymorphic inductives

For each template universe `u` bound by parameter `A` of an inductive `I`, when `I` is applied such that `A` is instantiated with a term of type `forall ..., Type@{q;i}` (where `i` may be an algebraic universe), `u` is instantiated by `i` in the inductive's conclusion and in the constraints (which must be of the form `u <= x` where `x` is a global universe due to the "no constraints from below" requirement).

Each template sort `s` is instantiated by the supremum of the `q` appearing in the conclusions of the types of arguments provided for parameters binding `s`. This is well-defined because template sorts may only be instantiated by `Prop` and `Type` and variable sorts restricted to these 2 ground sorts.

If the inductive is partially applied, leftover parameters act as though they were given an argument at a default global universe and at sort `Type`.

Warning

Partially applied template polymorphic inductives lead to constraints between global universes, which can cause complex universe inconsistencies.

Example

As mentioned previously, `option` is not sort polymorphic:

Check fun A:Prop => option A.
  fun A : Prop => option A : Prop -> Set

but it is universe polymorphic:

Check fun A:Set => option A.
  fun A : Set => option A : Set -> Set
Check option Set.
  option Set : Type@{Set+1}

Example

`prod` is sort polymorphic, but restricted to `Prop` and `Type`:

Check fun A:Prop => prod A A.
  fun A : Prop => prod A A : Prop -> Prop
Fail Check fun A:SProp => prod A A.
  The command has indeed failed with message: In environment A : SProp The term "A" has type "SProp" while it is expected to have type "Type@{α101 ; Top.273}" (universe inconsistency: Cannot enforce SProp <= Type@{α101 | Top.273}).

When only one of the arguments is `Prop`, the supremum of the sorts is `Type`:

Check prod True nat.
  prod True nat : Set

This is also the case when partially applied to a `Prop`, and we can see the use of the default universe `prod.u1` for the second parameter:

Check prod True.
  prod True : Type@{prod.u1} -> Type@{max(Set,prod.u1)}

### Controlling template polymorphism

Flag Auto Template Polymorphism

  This flag, enabled by default, makes every inductive type declared at level `Type` (without an explicit universe instance or hiding it behind a definition) template polymorphic if possible.

  This can be prevented using the `universes(template=no)` attribute.

  Template polymorphism and full universe polymorphism (see Chapter Polymorphic Universes) are incompatible, so if the latter is enabled (through the `Universe Polymorphism` flag or the `universes(polymorphic)` attribute) it will prevail over automatic template polymorphism.

Warning Automatically declaring ident as template polymorphic.

  Warning `auto-template` can be used (it is off by default) to find which types are implicitly declared template polymorphic by `Auto Template Polymorphism`.

  An inductive type can be forced to be template polymorphic using the `universes(template)` attribute: in this case, the warning is not emitted.

Attribute universes(template= yes​no?)

  This boolean attribute can be used to explicitly declare an inductive type as template polymorphic, whether the `Auto Template Polymorphism` flag is on or off.

  Error Template-polymorphism and universe polymorphism are not compatible

    This attribute cannot be used in a full universe polymorphic context, i.e. if the `Universe Polymorphism` flag is on or if the `universes(polymorphic)` attribute is used.

  Warning This inductive type has no template universes

    The attribute was used but the inductive definition does not satisfy the criterion to be template polymorphic.

  When `universes(template=no)` is used, it will prevent an inductive type from being template polymorphic, even if the `Auto Template Polymorphism` flag is on.

## 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 universe `i` 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).

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF