\[\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}\]

Sorts¶

sort::=Set|Prop|SProp|Type|Type @{ _ }|Type @{ qualid |? universe }universe::=max ( universe_expr+, )|_|universe_expruniverse_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.

Algebraic universes In practice, the Type hierarchy is implemented using algebraic universes, which appear in the syntax Type@{universe}. An algebraic universe $u$ is either a variable, a successor of an algebraic universe (an expression $u+1$), an upper bound of algebraic universes (an expression $\max(u_1 ,...,u_n )$), or the base universe $\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.

The user does not have to mention explicitly the universe $u$ when referring to the universe Type@{u}. One only writes Type. The system itself generates for each instance of Type a new variable 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.

The syntax Type@{qualid | universe} is used with Polymorphic Universes when quantifying over all sorts including $\Prop$ and $\SProp$.