\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \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}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \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{\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}\]

Sorts¶

sort

::=

Set

|

Prop

|

SProp

|

Type

|

Type @{ _ }

|

Type @{ universe }

universe

::=

max ( universe_expr+, )

|

universe_expr

::=

universe_name + natural?

The types of types are called sorts.

All sorts have a type and there is an infinite well-founded typing hierarchy of sorts whose base sorts are $\SProp$, $\Prop$ and $\Set$.

The sort $\Prop$ intends to be the type of logical propositions. If $M$ is a logical proposition then it denotes the class of terms representing proofs of $M$. An object $m$ belonging to $M$ witnesses the fact that $M$ is provable. An object of type $\Prop$ is called a proposition. We denote propositions by form. This constitutes a semantic subclass of the syntactic class term.

The sort $\SProp$ is like $\Prop$ but the propositions in $\SProp$ are known to have irrelevant proofs (all proofs are equal). Objects of type $\SProp$ are called strict propositions. See SProp (proof irrelevant propositions) for information about using $\SProp$, and [GCST19] for meta theoretical considerations.

The sort $\Set$ intends to be the type of small sets. This includes data types such as booleans and naturals, but also products, subsets, and function types over these data types. We denote specifications (program types) by specif. This constitutes a semantic subclass of the syntactic class term.

$\SProp$, $\Prop$ and $\Set$ themselves can be manipulated as ordinary terms. Consequently they also have a type. Because assuming simply that $\Set$ has type $\Set$ leads to an inconsistent theory [Coq86], the language of CIC has infinitely many sorts. There are, in addition to the base sorts, a hierarchy of universes $\Type(i)$ for any integer $i ≥ 1$.

Like $\Set$, all of the sorts $\Type(i)$ contain small sets such as booleans, natural numbers, as well as products, subsets and function types over small sets. But, unlike $\Set$, they also contain large sets, namely the sorts $\Set$ and $\Type(j)$ for $j<i$, and all products, subsets and function types over these sorts.

Formally, we call $\Sort$ the set of sorts which is defined by:

\[\Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\}\]

Their properties, such as $\Prop:\Type(1)$, $\Set:\Type(1)$, and $\Type(i):\Type(i+1)$, are described in Subtyping rules.

The user does not have to mention explicitly the index $i$ when referring to the universe $\Type(i)$. One only writes Type. The system itself generates for each instance of Type a new index for the universe and checks that the constraints between these indexes can be solved. From the user point of view we consequently have $\Type:\Type$. We shall make precise in the typing rules the constraints between the indices.

Implementation issues In practice, the Type hierarchy is implemented using algebraic universes. An algebraic universe $u$ is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $\max(u_1 ,...,u_n )$), or the base universe (the expression $0$) which corresponds, in the arity of template polymorphic inductive types (see Section Well-formed inductive definitions), to the predicative sort $\Set$. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the acyclicity of the graph of constraints results in a Universe inconsistency error.