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

Typing rules¶

The underlying formal language of Coq is a Calculus of Inductive Constructions (CIC) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related work are provided in a separate chapter; see Early history of Coq.

The terms¶

The expressions of the CIC are terms and all terms have a type. There are types for functions (or programs), there are atomic types (especially datatypes)... but also types for proofs and types for the types themselves. Especially, any object handled in the formalism must belong to a type. For instance, universal quantification is relative to a type and takes the form “for all x of type $T$, $P$”. The expression “$x$ of type $T$” is written “$x:T$”. Informally, “$x:T$” can be thought as “$x$ belongs to $T$”.

Terms are built from sorts, variables, constants, abstractions, applications, local definitions, and products. From a syntactic point of view, types cannot be distinguished from terms, except that they cannot start by an abstraction or a constructor. More precisely the language of the Calculus of Inductive Constructions is built from the following rules.

the sorts $\SProp$, $\Prop$, $\Set$, $\Type(i)$ are terms.
variables, hereafter ranged over by letters $x$, $y$, etc., are terms
constants, hereafter ranged over by letters $c$, $d$, etc., are terms.
if $x$ is a variable and $T$, $U$ are terms then $∀ x:T,~U$ (forall x:T, U in Coq concrete syntax) is a term. If $x$ occurs in $U$, $∀ x:T,~U$ reads as “for all $x$ of type $T$, $U$”. As $U$ depends on $x$, one says that $∀ x:T,~U$ is a dependent product. If $x$ does not occur in $U$ then $∀ x:T,~U$ reads as “if $T$ then $U$”. A non dependent product can be written: $T \rightarrow U$.
if $x$ is a variable and $T$, $u$ are terms then $λ x:T .~u$ (fun x:T => u in Coq concrete syntax) is a term. This is a notation for the λ-abstraction of λ-calculus [Bar81]. The term $λ x:T .~u$ is a function which maps elements of $T$ to the expression $u$.
if $t$ and $u$ are terms then $(t~u)$ is a term (t u in Coq concrete syntax). The term $(t~u)$ reads as “$t$ applied to $u$”.
if $x$ is a variable, and $t$, $T$ and $u$ are terms then $\letin{x}{t:T}{u}$ is a term which denotes the term $u$ where the variable $x$ is locally bound to $t$ of type $T$. This stands for the common “let-in” construction of functional programs such as ML or Scheme.

Free variables. The notion of free variables is defined as usual. In the expressions $λx:T.~U$ and $∀ x:T,~U$ the occurrences of $x$ in $U$ are bound.

Substitution. The notion of substituting a term $t$ to free occurrences of a variable $x$ in a term $u$ is defined as usual. The resulting term is written $\subst{u}{x}{t}$.

The logical vs programming readings. The constructions of the CIC can be used to express both logical and programming notions, accordingly to the Curry-Howard correspondence between proofs and programs, and between propositions and types [CFC58][How80][dB72].

For instance, let us assume that $\nat$ is the type of natural numbers with zero element written $0$ and that True is the always true proposition. Then $→$ is used both to denote $\nat→\nat$ which is the type of functions from $\nat$ to $\nat$, to denote True→True which is an implicative proposition, to denote $\nat →\Prop$ which is the type of unary predicates over the natural numbers, etc.

Let us assume that mult is a function of type $\nat→\nat→\nat$ and eqnat a predicate of type $\nat→\nat→ \Prop$. The λ-abstraction can serve to build “ordinary” functions as in $λ x:\nat.~(\kw{mult}~x~x)$ (i.e. fun x:nat => mult x x in Coq notation) but may build also predicates over the natural numbers. For instance $λ x:\nat.~(\kw{eqnat}~x~0)$ (i.e. fun x:nat => eqnat x 0 in Coq notation) will represent the predicate of one variable $x$ which asserts the equality of $x$ with $0$. This predicate has type $\nat → \Prop$ and it can be applied to any expression of type $\nat$, say $t$, to give an object $P~t$ of type $\Prop$, namely a proposition.

Furthermore forall x:nat, P x will represent the type of functions which associate with each natural number $n$ an object of type $(P~n)$ and consequently represent the type of proofs of the formula “$∀ x.~P(x)$”.

Typing rules¶

As objects of type theory, terms are subjected to type discipline. The well typing of a term depends on a local context and a global environment.

Local context. A local context is an ordered list of declarations of variables. The declaration of a variable $x$ is either an assumption, written $x:T$ (where $T$ is a type) or a definition, written $x:=t:T$. Local contexts are written in brackets, for example $[x:T;~y:=u:U;~z:V]$. The variables declared in a local context must be distinct. If $Γ$ is a local context that declares $x$, we write $x ∈ Γ$. Writing $(x:T) ∈ Γ$ means there is an assumption or a definition giving the type $T$ to $x$ in $Γ$. If $Γ$ defines $x:=t:T$, we also write $(x:=t:T) ∈ Γ$. For the rest of the chapter, $Γ::(y:T)$ denotes the local context $Γ$ enriched with the local assumption $y:T$. Similarly, $Γ::(y:=t:T)$ denotes the local context $Γ$ enriched with the local definition $(y:=t:T)$. The notation $[]$ denotes the empty local context. Writing $Γ_1 ; Γ_2$ means concatenation of the local context $Γ_1$ and the local context $Γ_2$.

Global environment. A global environment is an ordered list of declarations. Global declarations are either assumptions, definitions or declarations of inductive objects. Inductive objects declare both constructors and inductive or coinductive types (see Section Theory of inductive definitions).

In the global environment, assumptions are written as $(c:T)$, indicating that $c$ is of the type $T$. Definitions are written as $c:=t:T$, indicating that $c$ has the value $t$ and type $T$. We shall call such names constants. For the rest of the chapter, the $E;~c:T$ denotes the global environment $E$ enriched with the assumption $c:T$. Similarly, $E;~c:=t:T$ denotes the global environment $E$ enriched with the definition $(c:=t:T)$.

The rules for inductive definitions (see Section Theory of inductive definitions) have to be considered as assumption rules in which the following definitions apply: if the name $c$ is declared in $E$, we write $c ∈ E$ and if $c:T$ or $c:=t:T$ is declared in $E$, we write $(c : T) ∈ E$.

Typing rules. In the following, we define simultaneously two judgments. The first one $\WTEG{t}{T}$ means the term $t$ is well-typed and has type $T$ in the global environment $E$ and local context $Γ$. The second judgment $\WFE{Γ}$ means that the global environment $E$ is well-formed and the local context $Γ$ is a valid local context in this global environment.

A term $t$ is well typed in a global environment $E$ iff there exists a local context $\Gamma$ and a term $T$ such that the judgment $\WTEG{t}{T}$ can be derived from the following rules.

W-Empty: \[\frac{% % }{% \WF{[]}{}% }\]

W-Local-Assum: \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% x \not\in \Gamma % \cup E% }{% \WFE{\Gamma::(x:T)}% }\]

W-Local-Def: \[\frac{% \WTEG{t}{T}% \hspace{3em}% x \not\in \Gamma % \cup E% }{% \WFE{\Gamma::(x:=t:T)}% }\]

W-Global-Assum: \[\frac{% \WTE{}{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% c \notin E% }{% \WF{E;~c:T}{}% }\]

W-Global-Def: \[\frac{% \WTE{}{t}{T}% \hspace{3em}% c \notin E% }{% \WF{E;~c:=t:T}{}% }\]

Ax-SProp: \[\frac{% \WFE{\Gamma}% }{% \WTEG{\SProp}{\Type(1)}% }\]

Ax-Prop: \[\frac{% \WFE{\Gamma}% }{% \WTEG{\Prop}{\Type(1)}% }\]

Ax-Set: \[\frac{% \WFE{\Gamma}% }{% \WTEG{\Set}{\Type(1)}% }\]

Ax-Type: \[\frac{% \WFE{\Gamma}% }{% \WTEG{\Type(i)}{\Type(i+1)}% }\]

Var: \[\frac{% \WFE{\Gamma}% \hspace{3em}% (x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}% }{% \WTEG{x}{T}% }\]

Const: \[\frac{% \WFE{\Gamma}% \hspace{3em}% (c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$}% }{% \WTEG{c}{T}% }\]

Prod-SProp: \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in {\Sort}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\SProp}% }{% \WTEG{\forall~x:T,U}{\SProp}% }\]

Prod-Prop: \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Prop}% }{% \WTEG{∀ x:T,~U}{\Prop}% }\]

Prod-Set: \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \{\SProp, \Prop, \Set\}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Set}% }{% \WTEG{∀ x:T,~U}{\Set}% }\]

Prod-Type: \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \{\SProp, \Type(i)\}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Type(i)}% }{% \WTEG{∀ x:T,~U}{\Type(i)}% }\]

Lam: \[\frac{% \WTEG{∀ x:T,~U}{s}% \hspace{3em}% \WTE{\Gamma::(x:T)}{t}{U}% }{% \WTEG{λ x:T\mto t}{∀ x:T,~U}% }\]

App: \[\frac{% \WTEG{t}{∀ x:U,~T}% \hspace{3em}% \WTEG{u}{U}% }{% \WTEG{(t\ u)}{\subst{T}{x}{u}}% }\]

Let: \[\frac{% \WTEG{t}{T}% \hspace{3em}% \WTE{\Gamma::(x:=t:T)}{u}{U}% }{% \WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}% }\]

Note

Prod-Prop and Prod-Set typing-rules make sense if we consider the semantic difference between $\Prop$ and $\Set$:

All values of a type that has a sort $\Set$ are extractable.
No values of a type that has a sort $\Prop$ are extractable.

Note

We may have $\letin{x}{t:T}{u}$ well-typed without having $((λ x:T.~u)~t)$ well-typed (where $T$ is a type of $t$). This is because the value $t$ associated with $x$ may be used in a conversion rule (see Section Conversion rules).

Subtyping rules¶

At the moment, we did not take into account one rule between universes which says that any term in a universe of index $i$ is also a term in the universe of index $i+1$ (this is the cumulativity rule of CIC). This property extends the equivalence relation of convertibility into a subtyping relation inductively defined by:

if $E[Γ] ⊢ t =_{βδιζη} u$ then $E[Γ] ⊢ t ≤_{βδιζη} u$,
if $i ≤ j$ then $E[Γ] ⊢ \Type(i) ≤_{βδιζη} \Type(j)$,
for any $i$, $E[Γ] ⊢ \Set ≤_{βδιζη} \Type(i)$,
$E[Γ] ⊢ \Prop ≤_{βδιζη} \Set$, hence, by transitivity, $E[Γ] ⊢ \Prop ≤_{βδιζη} \Type(i)$, for any $i$ (note: $\SProp$ is not related by cumulativity to any other term)
if $E[Γ] ⊢ T =_{βδιζη} U$ and $E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'$ then $E[Γ] ⊢ ∀x:T,~T′ ≤_{βδιζη} ∀ x:U,~U′$.
if $\ind{p}{Γ_I}{Γ_C}$ is a universe polymorphic and cumulative (see Chapter Polymorphic Universes) inductive type (see below) and $(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S)∈Γ_I$ and $(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', S')∈Γ_I$ are two different instances of the same inductive type (differing only in universe levels) with constructors

\[[c_1 : ∀Γ_P ,∀ T_{1,1} … T_{1,n_1} ,~t~v_{1,1} … v_{1,m} ;~…;~ c_k : ∀Γ_P ,∀ T_{k,1} … T_{k,n_k} ,~t~v_{k,1} … v_{k,m} ]\]

and

\[[c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ]\]

respectively then

\[E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m'\]

(notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type) if

\[E[Γ] ⊢ w_i =_{βδιζη} w_i'\]

for $1 ≤ i ≤ m$ and we have

\[E[Γ] ⊢ T_{i,j} ≤_{βδιζη} T_{i,j}'\]

and

\[E[Γ] ⊢ A_i ≤_{βδιζη} A_i'\]

where $Γ_{\mathit{Arr}(t)} = [a_1 : A_1 ;~ … ;~a_l : A_l ]$ and $Γ_{\mathit{Arr}(t)}' = [a_1 : A_1';~ … ;~a_l : A_l']$.

The conversion rule up to subtyping is now exactly:

Conv: \[\frac{% E[Γ] ⊢ U : s% \hspace{3em}% E[Γ] ⊢ t : T% \hspace{3em}% E[Γ] ⊢ T ≤_{βδιζη} U% }{% E[Γ] ⊢ t : U% }\]

Normal form. A term which cannot be any more reduced is said to be in normal form. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the head reduction which will play an important role (see Chapter Tactics). Any term $t$ can be written as $λ x_1 :T_1 .~… λ x_k :T_k .~(t_0~t_1 … t_n )$ where $t_0$ is not an application. We say then that $t_0$ is the head of $t$. If we assume that $t_0$ is $λ x:T.~u_0$ then one step of β-head reduction of $t$ is:

\[λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~ λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n )\]

Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the β-head normal form of $t$:

\[t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m )\]

where $v$ is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some $u_i$ can be reducible. Similar notions of head-normal forms involving δ, ι and ζ reductions or any combination of those can also be defined.

Admissible rules for global environments¶

From the original rules of the type system, one can show the admissibility of rules which change the local context of definition of objects in the global environment. We show here the admissible rules that are used in the discharge mechanism at the end of a section.

Abstraction. One can modify a global declaration by generalizing it over a previously assumed constant $c$. For doing that, we need to modify the reference to the global declaration in the subsequent global environment and local context by explicitly applying this constant to the constant $c$.

Below, if $Γ$ is a context of the form $[y_1 :A_1 ;~…;~y_n :A_n]$, we write $∀x:U,~\subst{Γ}{c}{x}$ to mean $[y_1 :∀ x:U,~\subst{A_1}{c}{x};~…;~y_n :∀ x:U,~\subst{A_n}{c}{x}]$ and $\subst{E}{|Γ|}{|Γ|c}$ to mean the parallel substitution $E\{y_1 /(y_1~c)\}…\{y_n/(y_n~c)\}$.

First abstracting property:

\[\frac{\WF{E;~c:U;~E′;~c′:=t:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} {\subst{Γ}{c′}{(c′~c)}}}\]

\[\frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}}\]

\[\frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ \subst{E″}{|Γ_I ;Γ_C |}{|Γ_I ;Γ_C | c}} {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}}\]

One can similarly modify a global declaration by generalizing it over a previously defined constant $c$. Below, if $Γ$ is a context of the form $[y_1 :A_1 ;~…;~y_n :A_n]$, we write $\subst{Γ}{c}{u}$ to mean $[y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]$.

Second abstracting property:

\[\frac{\WF{E;~c:=u:U;~E′;~c′:=t:T;~E″}{Γ}} {\WF{E;~c:=u:U;~E′;~c′:=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};~E″}{Γ}}\]

\[\frac{\WF{E;~c:=u:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:=u:U;~E′;~c′:\subst{T}{c}{u};~E″}{Γ}}\]

\[\frac{\WF{E;~c:=u:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WF{E;~c:=u:U;~E′;~\ind{p}{\subst{Γ_I}{c}{u}}{\subst{Γ_C}{c}{u}};~E″}{Γ}}\]

Pruning the local context. If one abstracts or substitutes constants with the above rules then it may happen that some declared or defined constant does not occur any more in the subsequent global environment and in the local context. One can consequently derive the following property.

First pruning property:: \[\frac{% \WF{E;~c:U;~E′}{Γ}% \hspace{3em}% c~\kw{does not occur in}~E′~\kw{and}~Γ% }{% \WF{E;E′}{Γ}% }\]

Second pruning property:: \[\frac{% \WF{E;~c:=u:U;~E′}{Γ}% \hspace{3em}% c~\kw{does not occur in}~E′~\kw{and}~Γ% }{% \WF{E;E′}{Γ}% }\]

The Calculus of Inductive Constructions with impredicative Set¶

Coq can be used as a type checker for the Calculus of Inductive Constructions with an impredicative sort $\Set$ by using the compiler option -impredicative-set. For example, using the ordinary coqtop command, the following is rejected,

Example

Fail Definition id: Set := forall X:Set,X->X.: The command has indeed failed with message: The term "forall X : Set, X -> X" has type "Type" while it is expected to have type "Set" (universe inconsistency: Cannot enforce Set+1 <= Set).

while it will type check, if one uses instead the coqtop -impredicative-set option..

The major change in the theory concerns the rule for product formation in the sort $\Set$, which is extended to a domain in any sort:

ProdImp: \[\frac{% E[Γ] ⊢ T : s% \hspace{3em}% s ∈ \Sort% \hspace{3em}% E[Γ::(x:T)] ⊢ U : \Set% }{% E[Γ] ⊢ ∀ x:T,~U : \Set% }\]

This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called large inductive definitions like the example of second-order existential quantifier (exSet).

There should be restrictions on the eliminations which can be performed on such definitions. The elimination rules in the impredicative system for sort $\Set$ become:

Set1: \[\frac{% s ∈ \{\Prop, \Set\}% }{% [I:\Set|I→ s]% }\]

Set2: \[\frac{% I~\kw{is a small inductive definition}% \hspace{3em}% s ∈ \{\Type(i)\}% }{% [I:\Set|I→ s]% }\]