# Some axioms for mathematics

Frédéric Blanqui  Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria,
France<EMAIL_ADDRESS>,  Gilles Dowek  Université Paris-Saclay,
ENS Paris-Saclay, LMF, CNRS, Inria, France<EMAIL_ADDRESS>,
Emilie Grienenberger  Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS,
Inria, France<EMAIL_ADDRESS>,  Gabriel Hondet
Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria, France
<EMAIL_ADDRESS>and  François Thiré  Nomadic Labs, France
<EMAIL_ADDRESS>
###### Abstract.

The $\lambda\Pi$-calculus modulo theory is a logical framework in which many
logical systems can be expressed as theories. We present such a theory, the
theory ${\mathcal{U}}$, where proofs of several logical systems can be
expressed. Moreover, we identify a sub-theory of ${\mathcal{U}}$ corresponding
to each of these systems, and prove that, when a proof in ${\mathcal{U}}$ uses
only symbols of a sub-theory, then it is a proof in that sub-theory.

##  1\. Introduction

The $\lambda\Pi\text{-calculus modulo theory}$ ($\lambda\Pi/\\!\equiv$)
[CD07], implemented in the system Dedukti [ABC+16, HB20], is a logical
framework, that is a framework to define theories. It generalizes some
previously proposed frameworks: Predicate logic [HA28],
$\lambda\text{-Prolog}$ [NM88], Isabelle [Pau93], the Edinburgh logical
framework [HHP93], also called the $\lambda\Pi\text{-calculus}$, Deduction
modulo theory [DHK03, DW03], Pure type systems [Ber88, Ter89], and Ecumenical
logic [Pra15, Dow15, PR17, Gri19]. It is thus an extension of Predicate logic
that provides the possibility for all symbols to bind variables, a syntax for
proof-terms, a notion of computation, a notion of proof reduction for
axiomatic theories, and the possibility to express both constructive and
classical proofs.

$\lambda\Pi/\\!\equiv$ enables to express all theories that can be expressed
in Predicate logic, such as geometry, arithmetic, and set theory, but also
Simple type theory [Chu40] and the Calculus of constructions [CH88], that are
less easy to define in Predicate logic.

We present a theory in $\lambda\Pi/\\!\equiv$, the theory ${\mathcal{U}}$,
where all proofs of Minimal, Constructive, and Ecumenical predicate logic;
Minimal, Constructive, and Ecumenical simple type theory; Simple type theory
with predicate subtyping, prenex predicative polymorphism, or both; the
Calculus of constructions, and the Calculus of constructions with prenex
predicative polymorphism can be expressed. This theory is therefore a
candidate for a universal theory, where proofs developed in implementations of
Classical predicate logic (such as automated theorem proving systems, SMT
solvers, etc.), Classical simple type theory (such as HOL 4, Isabelle/HOL, HOL
Light, etc.), the Calculus of constructions (such as Coq, Matita, Lean, etc.),
and Simple type theory with predicate subtyping and prenex polymorphism (such
as PVS), can be expressed.

Moreover, the proofs of the theory ${\mathcal{U}}$ can be classified as proofs
in Minimal predicate logic, Constructive Predicate logic, etc. just by
identifying the axioms they use, akin to proofs in geometry that can be
classified as proofs in Euclidean, hyperbolic, elliptic, neutral, etc.
geometries. More precisely, we identify sub-theories of the theory
${\mathcal{U}}$ that correspond to each of these theories, and we prove that
when a proof in ${\mathcal{U}}$ uses only symbols of a sub-theory, then it is
a proof in that sub-theory.

In Section 2, we recall the definition of $\lambda\Pi/\\!\equiv$ and of a
theory. In Section 3, we introduce the theory ${\mathcal{U}}$ step by step. In
Section 4, we provide a general theorem on sub-theories in
$\lambda\Pi/\\!\equiv$, and prove that every fragment of ${\mathcal{U}}$,
including ${\mathcal{U}}$ itself, is indeed a theory, that is, it is defined
by a confluent and type-preserving rewriting systems. Finally, in Section 5,
we detail the sub-theories of ${\mathcal{U}}$ that correspond to the above
mentioned systems.

##  2\. The $\lambda\Pi\text{-calculus modulo theory}$

$\lambda\Pi/\\!\equiv$ is an extension of the Edinburgh logical framework
[HHP93] with a primitive notion of computation defined with rewriting rules
[DJ90, TeR03].

The terms are those of the Edinburgh logical framework

$t,u=c~{}|~{}x~{}|~{}\mbox{\tt TYPE}~{}|~{}\mbox{\tt
KIND}~{}|~{}\Pi{x}\,{:}\,{t},u~{}|~{}\lambda{x}\,{:}\,{t},{u}~{}|~{}t~{}u$

where $c$ belongs to a finite or infinite set of constants ${\mathcal{C}}$ and
$x$ to an infinite set ${\mathcal{V}}$ of variables. The terms TYPE and KIND
are called sorts. The term $\Pi{x}\,{:}\,{t},u$ is called a product. It is
dependent if the variable $x$ occurs free in $u$. Otherwise, it is simply
written $t\rightarrow u$. Terms are also often written $A$, $B$, etc. The set
of constants of a term $t$ is written ${\mbox{\it const}}(t)$.

A rewriting rule is a pair of terms $\ell\hookrightarrow r$, such that
$\ell=c~{}\ell_{1}~{}\ldots~{}\ell_{n}$, where $c$ is a constant. If
${\mathcal{R}}$ is a set of rewriting rules, we write
$\hookrightarrow_{\mathcal{R}}$ for the smallest relation closed by term
constructors and substitution containing ${\mathcal{R}}$,
$\hookrightarrow_{\beta}$ for the usual $\beta$-reduction,
${\hookrightarrow_{\beta{\mathcal{R}}}}$ for
${{\hookrightarrow_{\beta}}\cup{\hookrightarrow_{\mathcal{R}}}}$, and
$\equiv_{\beta{\mathcal{R}}}$ for the smallest equivalence relation containing
${\hookrightarrow_{\beta{\mathcal{R}}}}$.

A relation $\hookrightarrow$ is confluent on a set of terms if, for all terms
$t,u,v$ in this set such that $t\hookrightarrow^{*}u$ and
$t\hookrightarrow^{*}v$, there exists a term $w$ in this set such that
$u\hookrightarrow^{*}w$ and $v\hookrightarrow^{*}w$. Confluence implies that
every term has at most one irreducible form.

$\vdash_{\Sigma,{\mathcal{R}}}[~{}]~{}\mbox{well-formed}$

$\vdash_{\Sigma,{\mathcal{R}}}\Gamma,x:A~{}\mbox{well-
formed}\Gamma\vdash_{\Sigma,{\mathcal{R}}}A:s$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}\mbox{\tt TYPE}:\mbox{\tt
KIND}\vdash_{\Sigma,{\mathcal{R}}}\Gamma~{}\mbox{well-formed}$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}c:A\vdash_{\Sigma,{\mathcal{R}}}\Gamma~{}\mbox{well-
formed}~{}~{}~{}\vdash_{\Sigma,{\mathcal{R}}}A:s$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}x:A\vdash_{\Sigma,{\mathcal{R}}}\Gamma~{}\mbox{well-
formed}$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}\Pi{x}\,{:}\,{A},B:s\lx@proof@logical@and\Gamma\vdash_{\Sigma,{\mathcal{R}}}A:\mbox{\tt
TYPE}\Gamma,x:A\vdash_{\Sigma,{\mathcal{R}}}B:s$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}\lambda{x}\,{:}\,{A},{t}:\Pi{x}\,{:}\,{A},B\lx@proof@logical@and\Gamma\vdash_{\Sigma,{\mathcal{R}}}A:\mbox{\tt
TYPE}\Gamma,x:A\vdash_{\Sigma,{\mathcal{R}}}B:s\Gamma,x:A\vdash_{\Sigma,{\mathcal{R}}}t:B$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}t~{}u:(u/x)B\lx@proof@logical@and\Gamma\vdash_{\Sigma,{\mathcal{R}}}t:\Pi{x}\,{:}\,{A},B\Gamma\vdash_{\Sigma,{\mathcal{R}}}u:A$

$\Gamma\vdash_{\Sigma,{\mathcal{R}}}t:B\lx@proof@logical@and\Gamma\vdash_{\Sigma,{\mathcal{R}}}t:A\Gamma\vdash_{\Sigma,{\mathcal{R}}}B:s$

Figure 1. Typing rules of $\lambda\Pi/\\!\equiv$ with signature $\Sigma$ and
rewriting rules $\mathcal{R}$

The typing rules of $\lambda\Pi/\\!\equiv$ are given in Figure 1. The
difference with the rules of the Edinburgh logical framework is that, in the
rule (conv), types are identified modulo $\equiv_{\beta{\mathcal{R}}}$ instead
of just $\equiv_{\beta}$. In a typing judgement
$\Gamma\vdash_{\Sigma,{\mathcal{R}}}t:A$, the term $t$ is given the type $A$
with respect to three parameters: a signature $\Sigma$ that assigns a type to
the constants of $t$, a context $\Gamma$ that assigns a type to the free
variables of $t$, and a set of rewriting rules ${\mathcal{R}}$. A context
$\Gamma$ is a list of declarations $x_{1}:B_{1},\ldots,x_{m}:B_{m}$ formed
with a variable and a term. A signature $\Sigma$ is a list of declarations
$c_{1}:A_{1},\ldots,c_{n}:A_{n}$ formed with a constant and a closed term,
that is a term term with no free variables. This is why the rule (const)
requires no context for typing $A$. We write $|\Sigma|$ for the set
$\\{c_{1},\ldots,c_{n}\\}$, and $\Lambda(\Sigma)$ for the set of terms $t$
such that ${\mbox{\it const}}(t)\subseteq|\Sigma|$. We say that a rewriting
rule $\ell\hookrightarrow r$ is in $\Lambda(\Sigma)$ if $\ell$ and $r$ are,
and a context $x_{1}:B_{1},\ldots,x_{m}:B_{m}$ is in $\Lambda(\Sigma)$ if
$B_{1},\ldots,B_{m}$ are. It is often convenient to group constant
declarations and rules into small clusters, called “axioms”.

A relation $\hookrightarrow$ preserves typing in $\Sigma,{\mathcal{R}}$ if,
for all contexts $\Gamma$ and terms $t$, $u$ and $A$ of $\Lambda(\Sigma)$, if
$\Gamma\vdash_{\Sigma,{\mathcal{R}}}t:A$ and $t\hookrightarrow u$, then
$\Gamma\vdash_{\Sigma,{\mathcal{R}}}u:A$. The relation
$\hookrightarrow_{\beta}$ preserves typing as soon as
$\hookrightarrow_{\beta{\mathcal{R}}}$ is confluent (see for instance [Bla01])
for, in this case, the product is injective modulo
$\equiv_{\beta{\mathcal{R}}}$:
$\Pi{x}\,{:}\,{A},B\equiv_{\beta{\mathcal{R}}}\Pi{x}\,{:}\,{A^{\prime}},B^{\prime}$
iff $A\equiv_{\beta{\mathcal{R}}}A^{\prime}$ and
$B\equiv_{\beta{\mathcal{R}}}B^{\prime}$. The relation
$\hookrightarrow_{\mathcal{R}}$ preserves typing if every rewriting rule
$\ell\hookrightarrow r$ preserves typing, that is: for all contexts $\Gamma$,
substitutions $\theta$ and terms $A$ of $\Lambda(\Sigma)$, if
$\Gamma\vdash_{\Sigma,{\mathcal{R}}}\theta l:A$ then
$\Gamma\vdash_{\Sigma,{\mathcal{R}}}\theta r:A$.

Although typing is defined with arbitrary signatures $\Sigma$ and sets of
rewriting rules ${\mathcal{R}}$, we are only interested in sets
${\mathcal{R}}$ verifying some confluence and type-preservation properties.

[System, theory] A system is a pair $\Sigma,{\mathcal{R}}$ such that each rule
of ${\mathcal{R}}$ is in $\Lambda(\Sigma)$. It is a theory if
$\hookrightarrow_{\beta{\mathcal{R}}}$ is confluent on $\Lambda(\Sigma)$, and
every rule of ${\mathcal{R}}$ preserves typing in $\Sigma,{\mathcal{R}}$.

Therefore, in a theory, $\hookrightarrow_{\beta{\mathcal{R}}}$ preserves
typing since $\hookrightarrow_{\beta}$ preserves typing (for
$\hookrightarrow_{\beta{\mathcal{R}}}$ is confluent) and
$\hookrightarrow_{\mathcal{R}}$ preserves typing (for every rule preserves
typing). We recall two other basic properties of $\lambda\Pi/\\!\equiv$ we
will use in Theorem 13:

######  Lemma 1.

If $\Gamma\vdash_{\Sigma,{\mathcal{R}}}t:A$, then either $A=\mbox{\tt KIND}$
or $\Gamma\vdash_{\Sigma,{\mathcal{R}}}A:s$ for some sort $s$.

If $\Gamma\vdash_{\Sigma,{\mathcal{R}}}\Pi{x}\,{:}\,{A},B:s$, then
$\Gamma\vdash_{\Sigma,{\mathcal{R}}}A:\mbox{\tt TYPE}$.

##  3\. The theory ${\mathcal{U}}$

Let us now present the theory ${\mathcal{U}}$ which is formed with axioms
expressed in $\lambda\Pi/\\!\equiv$.

###  3.1. Object-terms

The notions of term, proposition, and proof are not primitive in
$\lambda\Pi/\\!\equiv$. The first axioms of the theory ${\mathcal{U}}$
introduce these notions. We first define a notion analogous to the Predicate
logic notion of term, to express the objects the theory speaks about, such as
the natural numbers. As all expressions in $\lambda\Pi/\\!\equiv$ are called
“terms”, we shall call these expressions “object-terms”, to distinguish them
from the other terms.

To build the notion of object-term in $\lambda\Pi/\\!\equiv$ we declare a
constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ of type
TYPE

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}:\mbox{\tt
TYPE}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$-decl)

and constants of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow...\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
for the function symbols, for instance a constant $0$ of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ and a
constant succ of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$.
The object-terms, for instance $(\mbox{{succ}}~{}(\mbox{{succ}}~{}0))$ and
$(\mbox{{succ}}~{}x)$, are then just $\lambda\Pi/\\!\equiv$ terms of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ and, in
an object-term, the variables are $\lambda\Pi/\\!\equiv$ variables of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$. If we
wanted to have object-terms of several sorts, like in Many-sorted predicate
logic, we could just declare several constants $I_{1}$, $I_{2}$, …, $I_{n}$ of
type TYPE.

###  3.2. Propositions

Just like $\lambda\Pi/\\!\equiv$ does not contain a primitive notion of
object-term, it does not contain a primitive notion of proposition, but tools
to define this notion. To do so, in the theory ${\mathcal{U}}$, we declare a
constant Prop of type TYPE

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}:\mbox{\tt TYPE}$ (Prop-decl)

and predicate symbols, that is constants of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow...\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$, for instance a constant positive of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$. Propositions are then $\lambda\Pi/\\!\equiv$ terms, such as
$(\mbox{{positive}}~{}(\mbox{{succ}}~{}(\mbox{{succ}}~{}0)))$, of type Prop.

###  3.3. Implication

In the theory ${\mathcal{U}}$, we then declare a constant for implication

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$-decl)

and we can then construct the term $(\mbox{\it
positive}~{}({\textit{succ}}~{}({\textit{succ}}~{}0)))\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}(\mbox{\it
positive}~{}({\textit{succ}}~{}({\textit{succ}}~{}0)))$ of type Prop.

###  3.4. Proofs

Predicate logic defines a language for terms and propositions, but proofs have
to be defined in a second step, for instance as derivations in natural
deduction, sequent calculus, etc. These derivations, like object-terms and
propositions, are trees. Therefore, they can be represented as
$\lambda\Pi/\\!\equiv$ terms.

Using the Brouwer-Heyting-Kolmogorov interpretation, a proof of the
proposition
$A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}B$
should be a $\lambda\Pi/\\!\equiv$ term expressing a function mapping proofs
of $A$ to proofs of $B$. Then, using the Curry-de Bruijn-Howard
correspondence, the type of this term should be the proposition
$A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}B$
itself. But, this is not possible in the theory ${\mathcal{U}}$ yet, as the
proposition
$A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}B$
has the type Prop, and not the type TYPE.

A strict view on the Curry-de Bruijn-Howard correspondence leads to identify
Prop and TYPE, yielding the conclusion that all types, including
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$, and
Prop itself, are propositions. A more moderate view leads to introduce an
embedding Prf of propositions into types, mapping each proposition $A$ to the
type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$ of its proofs. This view is moderate in two respects. First, the
propositions themselves are not the types of their proofs: if $t$ is a proof
of $A$, then it does not have the type $A$, but the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$. Second, this embedding is not surjective. So not all types are
types of proofs, in particular
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ and
Prop are not.

So, in the theory ${\mathcal{U}}$, we declare a constant Prf

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow\mbox{\tt TYPE}$ (Prf-decl)

When assigning the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow\mbox{\tt TYPE}$ to the constant Prf, we use the fact that
$\lambda\Pi/\\!\equiv$ supports dependent types, that is the possibility to
build a family of types
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x$ parameterized with a variable $x$ of type Prop, where Prop is
itself of type TYPE.

According to the Brouwer-Heyting-Kolmogorov interpretation, a proof of
$A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}A$
is a $\lambda\Pi/\\!\equiv$ term expressing a function mapping proofs of $A$
to proofs of $A$. In particular, the identity function
$\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A},{x}$ mapping each proof of $A$ to itself is a proof of
$A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}A$.
According to the Curry-de Bruijn-Howard correspondence, this term should have
the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}A)$,
but it has the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$. So, the types
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}A)$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$ must be identified. To do so, we use the fact that
$\lambda\Pi/\\!\equiv$ allows the declaration of rewriting rules, so that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(A\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}A)$
rewrites to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}y)~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$-red)

This rule expresses the meaning of the constant
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$.
It is, in $\lambda\Pi/\\!\equiv$, the expression of the Brouwer-Heyting-
Kolmogorov interpretation of proofs for implication: a proof of
$x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}y$
is a function mapping proofs of $x$ to proofs of $y$. So, in the theory
${\mathcal{U}}$, the Brouwer-Heyting-Kolmogorov interpretation of proofs for
implication is made explicit: it is the rule
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$-red).

###  3.5. Universal quantification

Unlike implication, the universal quantifier binds a variable. Thus, we
express the proposition $\forall z~{}A$ as the proposition
$\forall~{}(\lambda{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{A})$
[Chu40, NM88, Pau93, HHP93], yielding the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ for the argument of $\forall$, hence the type
$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ for the constant $\forall$ itself.

But, in the theory ${\mathcal{U}}$, we allow quantification, not only over the
variables of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$, but
over variables of any type of object-terms. We could introduce a different
quantifier for each type of object-terms, for instance two quantifiers of type
$(I_{1}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ and
$(I_{2}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ if we had two types $I_{1}$ and $I_{2}$ of object-terms. But, as in
some cases, we will have an infinite number of types of object-terms, this
would require to introduce a infinite number of constants.

Thus, we rather want to have a single generic quantifier. But we cannot give
the type $\Pi{X}\,{:}\,{\mbox{\tt
TYPE}},(X\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ to this quantifier, first because in $\lambda\Pi/\\!\equiv$ there is
no way to quantifiy over a variable of type TYPE, but also bcause this would
introduce the possibility to quantify over Prop and all the types of the form
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$, while we do not always we want to consider these types as types of
object-terms.

Therefore, in the theory ${\mathcal{U}}$, we declare a constant Set of type
TYPE for the types of object-terms

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}:\mbox{\tt TYPE}$ (Set-decl)

a constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$ of
type Set

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$-decl)

a constant El to embed the terms of type Set into terms of type TYPE

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow\mbox{\tt TYPE}$ (El-decl)

and a rule that reduces the term
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$
to ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$-red)

The types of object-terms then have the form
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}A$ and are distinguished among the other terms of type TYPE.

We can now give the type
$\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ to the generic universal quantifier

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}:\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$-decl)

and write
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}(\lambda{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{A})$
for the proposition $\forall z~{}A$.

Just like for the implication, we declare a rewriting rule expressing that the
type of the proofs of the proposition
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}~{}x~{}p$
is the type of functions mapping each $z$ of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x$ to a proof of $p~{}z$

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}~{}x~{}p)~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(p~{}z)$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$-red)

Again, the Brouwer-Heyting-Kolmogorov interpretation of proofs for the
universal quantifier is made explicit: it is this rule
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$-red).

###  3.6. Other constructive connectives and quantifiers

We define the other connectives and quantifiers, à la Russell, for instance
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x$ as
$\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$. In this definition, we do not use the quantifier
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$
of the theory ${\mathcal{U}}$ (so far, in the theory ${\mathcal{U}}$, we can
quantify over the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$, but
not over the type Prop), but the quantifier $\Pi$ of the logical framework
$\lambda\Pi/\\!\equiv$ itself.

Remark that, per se, the quantification on the variable $z$ of type Prop is
predicative, as the term
$\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$ has type TYPE and not Prop. But, the rule rewriting
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x$ to
$\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$ introduces some impredicativity, as $x$ of type Prop is “defined”
as the inverse image, for the embedding Prf, of the type
$\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$, that contains a quantification on a variable of type Prop

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$-red)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}$-red)

$\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
($\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}x)~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$
($\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}$-red)

(written infix) (-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x$ (-red)

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}y)~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}$-red)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists}:\Pi{a}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists}~{}a~{}p)~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},(\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(p~{}x)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}z$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists}$-red)

###  3.7. Infinity

Now that we have the symbols
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$ and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}$, we
can express that the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ is
infinite, that is, that there exists a non-surjective injection from this type
to itself. We call this non-surjective injection succ. To express its
injectivity, we introduce its left inverse pred. To express its non-
surjectivity, we introduce an element
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$, that
is not in its image positive [DW05]. This choice of notation enables the
definition of natural numbers as some elements of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
succ}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
(succ-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pred}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
(pred-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pred}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$
(pred-red1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pred}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
succ}}~{}x)~{}\hookrightarrow~{}x$ (pred-red2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (positive-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}$
(positive-red1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
succ}}~{}x)~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$
(positive-red2)

###  3.8. Classical connectives and quantifiers

The disjunction in constructive logic and in classical logic are governed by
different deduction rules. As the deduction rules express the meaning of the
connectives and quantifiers, we can conclude that the disjunction in
constructive logic and in classical logic have different meanings. If these
disjunctions have different meanings, they should be expressed with different
symbols, for instance $\vee$ for the constructive disjunction and $\vee_{c}$
for the classical one, just like, in classical logic, we use two different
symbols for the inclusive disjunction and the exclusive one.

The constructive and the classical disjunction need not belong to different
languages, but they can coexist in the same. Ecumenical logics [Pra15, Dow15,
PR17, Gri19] are logics where the constructive and classical connectives and
quantifiers coexist. A proposition whose connectors and quantifiers are all
constructive, is said to be “purely constructive”, and one whose connectors
and quantifiers are all classical, is said to be “purely classical”. The
others are said to be “mixed propositions”. Any deductive system, where a
purely constructive proposition is provable if and only if it is provable in
Constructive predicate logic, and where a purely classical proposition is
provable if and only if it is provable in Classical predicate logic, is
Ecumenical. Ecumenical logics may of course differ on mixed propositions.

Many Ecumenical logics consider the constructive connectives and quantifiers
as primitive and attempt to define the classical ones from them, using the
negative translation as a definition. There are several options: the classical
disjunction, for instance, can either be defined as

  1. (1)

$A\vee_{c}B=\neg\neg(A\vee B)$

  2. (2)

$A\vee_{c}B=(\neg\neg A)\vee(\neg\neg B)$

  3. (3)

$A\vee_{c}B=\neg\neg((\neg\neg A)\vee(\neg\neg B))$

and similarly for the other connectives and quantifiers.

Using these definitions, the proposition $(P\wedge_{c}Q)\Rightarrow_{c}P$ is
then

  1. (1)

$\neg\neg((\neg\neg(P\wedge Q))\Rightarrow P)$

  2. (2)

$(\neg\neg((\neg\neg P)\wedge(\neg\neg Q)))\Rightarrow(\neg\neg P)$

  3. (3)

$\neg\neg((\neg\neg\neg\neg((\neg\neg P)\wedge(\neg\neg
Q)))\Rightarrow(\neg\neg P))$

None of them is exactly the negative translation of $(P\wedge Q)\Rightarrow P$
that is

$\neg\neg((\neg\neg((\neg\neg P)\wedge(\neg\neg Q)))\Rightarrow(\neg\neg P))$

With Definition (1.), the double negations on atomic propositions are missing.
This can be repaired in two ways: by duplicating each predicate symbol of the
language [Pra15] into a constructive one and a classical one, the latter being
the double negation of the former, or by modifying the syntax of Predicate
logic [Gil18], defining first terms, then atoms, of the form
$P(t_{1},...,t_{n})$ where $P$ is a predicate symbol and $t_{1}$, …, $t_{n}$
terms, and finally propositions, a proposition being either an atom, the
conjunction of two propositions, etc. but making the embedding of atoms into
propositions explicit, with a symbol $\rhd$, this symbol having also a
classical version defined as the double negation of the constructive one. This
way, the proposition above is now written
$(\rhd_{c}P\wedge_{c}~{}\rhd_{c}Q)\Rightarrow_{c}\rhd_{c}P$, which is, by
definition, equal to $\neg\neg((\neg\neg((\neg\neg\rhd P)\wedge(\neg\neg\rhd
Q)))\Rightarrow(\neg\neg\rhd P))$.

With Definition (2.) [AH14], the double negation at the root of the
proposition is missing. This again can be repaired [Gri19] by modifying the
syntax of Predicate logic, defining first terms, then pre-propositions, that
are defined like the propositions in Predicate logic and then propositions, a
proposition being obtained by applying a symbol $\circ$ to a pre-proposition.
Again, this symbol has also a classical version defined as the double negation
of the constructive one. This way, the proposition above is written
$\circ_{c}((P\wedge_{c}Q)\Rightarrow_{c}P)$ and this proposition is, by
definition, equal to $\circ\neg\neg((\neg\neg((\neg\neg P)\wedge(\neg\neg
Q)))\Rightarrow(\neg\neg P))$.

Definition (3.) [Dow15] is closer to the negative translation except that, in
some places, the two negations are replaced with four. But, as $\neg\neg\neg
A$ is equivalent to $\neg A$, these extra negations can be removed. Yet, a
classical atomic proposition $P$ is the same as its constructive version,
while its negative translation is $\neg\neg P$, and in (1.) $P_{c}$ or
$\rhd_{c}P$ is equal $\neg\neg P$, as well as $\circ_{c}P$ in (2.). As atomic
propositions are not provable anyway, this does not affect provability. But it
affects hypothetical provability, leading to duplicate the notion of
entailment.

In the theory ${\mathcal{U}}$, we use Definition (2.). Indeed, as we already
have a distinction between the proposition $A$ and the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}A$ of its proofs, we can just include the symbol $\circ_{c}$ into the
constant Prf introducing a classical version
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}}$ of this constant

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow\mbox{\tt TYPE}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}}~{}\hookrightarrow~{}\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}x)}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}}$-red)

We can then define the classical connectives and quantifiers as follows

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{c}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{c}}$-decl)

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{c}}~{}\hookrightarrow~{}\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\lambda{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}x)\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}y)}}$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{c}}$-red)

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\wedge_{c}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\wedge_{c}}$-decl)

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\wedge_{c}}~{}\hookrightarrow~{}\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\lambda{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}x)\conj(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}y)}}$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\wedge_{c}}$-red)

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee_{c}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee_{c}}$-decl)

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee_{c}}~{}\hookrightarrow~{}\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\lambda{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}x)\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}(\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}y)}}$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee_{c}}$-red)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall_{c}}:\Pi{a}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall_{c}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall_{c}}~{}\hookrightarrow~{}\lambda{a}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{\lambda{p}\,{:}\,{({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}~{}a~{}(\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a},{\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}(p~{}x))}}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall_{c}}$-red)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists_{c}}:\Pi{a}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists_{c}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists_{c}}~{}\hookrightarrow~{}\lambda{a}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{\lambda{p}\,{:}\,{({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists}~{}a~{}(\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}a},{\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}(p~{}x))}}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists_{c}}$-red)

Note that $\top_{c}$ and $\bot_{c}$ are $\top$ and $\bot$, by definition. Note
also that $\neg\neg\neg A$ is equivalent to $\neg A$, so we do not need to
duplicate negation either.

###  3.9. Propositions as objects

So far, we have mainly reconstructed the Predicate logic notions of object-
term, proposition, and proof. We can now turn to two notions coming from
Simple type theory: propositions as objects and functionality.

Simple type theory is often presented as an independent system, but it can be
expressed in several logical frameworks, such as Predicate logic, Isabelle,
Deduction modulo theory, Pure type systems, and also $\lambda\Pi/\\!\equiv$.
Yet, the relation between Predicate logic and Simple type theory is complex
because

  * •

Simple type theory can be expressed in Predicate logic

  * •

and Predicate logic is a restriction of Simple type theory, allowing
quantification on variables of type $\iota$ only.

So, in Predicate logic, we can express Simple type theory, that contains, as a
restriction, Predicate logic, in which we can express Simple type theory, that
contains, as a restriction, Predicate logic, in which we can express Simple
type theory, that contains, etc. Stacking encodings in this way leads to
nonsensical expressions of Simple type theory. But this remark shows that,
after having reconstructed Predicate logic in $\lambda\Pi/\\!\equiv$, we have
a choice: we can either express Simple type theory in Predicate logic, that is
itself expressed in $\lambda\Pi/\\!\equiv$, or express Simple type theory
directly in $\lambda\Pi/\\!\equiv$, letting Predicate logic be, a posteriori,
a restriction of it, that is, build Simple type theory, not in Predicate
logic, but as an extension of Predicate logic.

In the theory ${\mathcal{U}}$, we choose the second option that leads to a
simpler expression of Simple type theory, avoiding the stacking of two
encodings. Simple type theory is thus expressed by adding two axioms on top of
Predicate logic: one for propositions as objects and one for functionality.

Let us start with propositions as objects. So far, the term
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$ is
the only closed term of type Set. So, we can only quantify over the variables
of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$,
that is
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$. In
particular, we cannot quantify over propositions. To do so, we just need to
declare a constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$ of type
Set

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$-decl)

and a rule identifying
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$
and Prop

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$-red)

Note that just like there are no terms of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$,
but terms, such as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$, which
have type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$,
that is
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$, there
are no terms of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$, but
terms, such as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$,
which have type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$,
that is Prop.

Applying the constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$
to the constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$, we
obtain a term of type
$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$, that is
$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$, and we can express the proposition $\forall p~{}(p\Rightarrow p)$ as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}~{}(\lambda{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{p\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}p})$.
The type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}~{}(\lambda{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{p\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}p}))$
of the proofs of this proposition rewrites to
$\Pi{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}p\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}p$. So, the term
$\lambda{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}p},{x}}$ is a proof of this proposition.

###  3.10. Functionality

Besides
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$ and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$, we
introduce more types in the theory, for functions and sets. To do so, we
declare a constant

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$-decl)

and a rewriting rule

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}y)~{}\hookrightarrow~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x)\rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}y)$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$-red)

For instance, these rules enable the construction of the
$\lambda\Pi/\\!\equiv$ term
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$
of type Set that expresses the simple type $\iota\rightarrow\iota$. The
$\lambda\Pi/\\!\equiv$ term
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})$
of type TYPE rewrites to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$.
The simply typed term $\lambda{x}\,{:}\,{\iota},{x}$ of type
$\iota\rightarrow\iota$ is then expressed as the term
$\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{x}$
of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
that is
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})$.

###  3.11. Dependent arrow

The axiom
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$)
enables us to give simple types to the object-terms expressing functions. We
can also give them dependent types, with the dependent versions of this axiom

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}:\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}y)~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(y~{}z)$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$-red)

Note that, if we apply the constant
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$
to a term $t$ and a term
$\lambda{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t},{u}$, where the variable $z$ does not occur in $u$, then
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(t\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}\lambda{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t},{u})$ rewrites to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}u$, just like
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(t\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}u)$.
Thus, the constant
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$
is useful only if we can build a term
$\lambda{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t},{u}$ where the variable $z$ occurs in $u$. With the symbols we have
introduced so far, this is not possible. The only constants that can be used
to build a term of type Set are
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$,
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$,
and
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$,
and the variable $z$ cannot occur free in a term built from these four
constants and a variable $z$ of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t$.

Just like we have a constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$ of
type Set, we could add a constant array of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ such that $\mbox{{array}}~{}n$ is the type of arrays of length $n$. We
could then construct the term
$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}\lambda{n}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{\mbox{{array}}~{}n})$
of type Set. Then, the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}\lambda{n}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{\mbox{{array}}~{}n})$
that rewrites to
$\Pi{n}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(\mbox{{array}}~{}n)$, would be the type of functions mapping a natural
number $n$ to an array of length $n$.

So, this symbol
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$
becomes useful, only if we add such a constant array, object-level dependent
types, or the symbols
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}$ or
psub below.

###  3.12. Dependent implication

In the same way, we can add a dependent implication, where, in the proposition
$A\Rightarrow B$, the proof of $A$ may occur in $B$

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}:\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (written infix)
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}y)~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(y~{}z)$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}$-red)

###  3.13. Proofs in object-terms

To construct an object-term, we sometimes want to apply a function symbol to
other object-terms and also to proofs. For instance, we may want to apply the
Euclidean division div to two numbers $t$ and $u$ and to a proof that $u$ is
positive.

We would like the type of div to be something like

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}\lambda{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{~{}}{({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})})$

But the term
$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})$
is not well typed, as the constant
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$
expects, as a first argument, a term of type Set and not of type Prop, that
is, a type of object-terms and not of proofs.

Thus, we must declare another constant

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$

and a rewriting rule

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}~{}x~{}y)~{}\hookrightarrow~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x)\rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}y)$

Just like for the constant
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$
and
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$,
we can also have a dependent version of this constant. In fact, in the theory
${\mathcal{U}}$, we only have this dependent version

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}:\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}~{}x~{}y)~{}\hookrightarrow~{}\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}(y~{}z)$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}$-red)

This way, we can give, to the constant div, the type

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}\lambda{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{\pi~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y)~{}(\lambda{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y)},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}})})$

that is

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow\Pi{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$

In the same way, if we add a symbol $=$ of type
$\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}\rightarrow{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$, we can express the proposition

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}\lambda{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y)},{(=~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}(\mbox{{div}}~{}x~{}y~{}p)~{}(\mbox{{div}}~{}x~{}y~{}p))}$

enlightening the meaning of the proposition usually written

$y>0\Rightarrow x/y=x/y$

The proposition $x/y=x/y$ is well-formed, but it contains, besides $x$ and
$y$, an implicit free variable $p$, for a proof of $y>0$. This variable is
bound by the implication, that needs therefore to be a dependent implication.
Hence, the only free variables in $y>0\Rightarrow x/y=x/y$ are $x$ and $y$.

###  3.14. Proof irrelevance

If $p$ and $q$ are two non convertible proofs of the proposition
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}2$, the terms $\mbox{{div}}~{}7~{}2~{}p$ and
$\mbox{{div}}~{}7~{}2~{}q$ are not convertible. As a consequence, the
proposition

$=~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}(\mbox{{div}}~{}7~{}2~{}p)~{}(\mbox{{div}}~{}7~{}2~{}q)$

would not be provable.

To make these terms convertible, we embed the theory into an extended one,
that contains another constant

$\mbox{{div}}^{\dagger}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})$

and a rule

$\mbox{{div}}~{}x~{}y~{}p~{}\hookrightarrow~{}\mbox{{div}}^{\dagger}~{}x~{}y$

and we define convertibility in this extended theory. This way, the terms
$\mbox{{div}}~{}7~{}2~{}p$ and $\mbox{{div}}~{}7~{}2~{}q$ are convertible, as
they both reduce to $\mbox{{div}}^{\dagger}~{}7~{}2$.

Note that, in the extended theory, the constant $\mbox{{div}}^{\dagger}$
enables the construction of the erroneous term
$\mbox{{div}}^{\dagger}~{}1~{}0$. But the extended theory is only used to
define the convertibility in the restricted one and this term is not a term of
the restricted theory. It is not even the reduct of a term of the form
$\mbox{{div}}~{}1~{}0~{}r$ [FT19, BH21].

###  3.15. Dependent pairs and predicate subtyping

Instead of declaring a constant div that takes three arguments: a number $t$,
a number $u$, and a proof $p$ that $u$ is positive, we can declare a constant
that takes two arguments: a number $t$ and a pair
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}u~{}p$ formed with a number $u$ and a proof $p$ that $u$ is
positive.

The type of the pair
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}u~{}p$ whose first element is a number and the second a proof
that this number is positive is written
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}$, or informally
$\\{x:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}x\\}$. It can be called “the type of positive numbers”,
especially if the pair is proof-irrelevant in its second argument. It is a
subtype of the type of natural numbers defined with the predicate positive.
Therefore, the symbol psub introduces predicate subtyping.

We thus declare a constant psub and a constant pair

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}:\Pi{t}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ (psub-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}}:\Pi{t}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},\Pi{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},\Pi{m}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(p~{}m)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)$ (pair-decl)

This way, instead of giving the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}\lambda{y}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}y)},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}})$
to the constant div, we can give it the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})$.

To avoid introducing a new positive number
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}3~{}p$ with each proof $p$ that $3$ is positive, we make this
symbol pair proof irrelevant by introducing a symbol
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}$ and a rewriting rule that discards the proof

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}:\Pi{t}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},\Pi{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}}~{}t~{}p~{}m~{}h~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}~{}t~{}p~{}m$ (pair-red)

This declaration and this rewriting rule are not part of the theory
${\mathcal{U}}$ but of the theory ${\mathcal{U}}^{\dagger}$ used to define the
conversion on the terms of ${\mathcal{U}}$.

Finally, we declare the projections fst and snd together with an associated
rewriting rule

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}}:\Pi{t}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},\Pi{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t$ (fst-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}}~{}t~{}p~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}~{}t^{\prime}~{}p^{\prime}~{}m)~{}\hookrightarrow~{}m$ (fst-
red)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
snd}}:\Pi{t}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},\Pi{p}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}},\Pi{m}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(p~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}}~{}t~{}p~{}m))$ (snd-decl)

Note that the left hand side of the rule (fst-red) is not well-typed, but it
can match a well-typed term
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}}~{}A~{}B~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}~{}A~{}B~{}m)$. Yet, we prefer this rule to the non linear one
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}}~{}t~{}p~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}~{}t~{}p~{}m)~{}\hookrightarrow~{}m$ that would make
confluence proofs more difficult.

Note that there is no rewriting rule for the second projection as the second
element of pairs is discarded during rewriting.

###  3.16. Dependent types

When we have the axioms (El),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$),
and
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$),
the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
of the term succ is equivalent to the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota})$.
Hence, this type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
is in the image of the embedding El. The symbol array introduced in Section
3.11 has the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ and similarly if we have a predicate symbol
$\leq:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o})$,
the term
$\lambda{n}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}~{}(\lambda{m}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{m\leq
n})}$ also has the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$. Unlike the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
the type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ is not in the image of any embedding. It is well-formed in the
framework but not in the theory itself.

To make this type an element of the image of an embedding we can introduce
dependent types at the level of objects-terms. To do so, we introduce a
constant Set1 of type TYPE and a constant set of type Set1

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set1}}:\mbox{\tt TYPE}$ (Set1-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
set}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set1}}\hfill$ (set-decl)

a new arrow

$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}:\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set1}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set1}}$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}$-decl)

and an embedding of Set1 into TYPE, similar to the embeddings Prf and El

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Ty}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set1}}\rightarrow\mbox{\tt TYPE}$ (Ty-decl)

and we identify Ty set with Set—like
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$
is identified with Prop—and the dependent arrow
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}$
with a product type

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Ty}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
set}}\hookrightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$ (set-red)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Ty}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}y)\hookrightarrow\Pi{z}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Ty}}~{}(y~{}z)$
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}$-red)

The type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$, is now equivalent to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Ty}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}(\lambda{n}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
set}}}))$ and is thus in the image of the embedding Ty.

###  3.17. Prenex predicative type quantification in types

Using the symbols of the theory ${\mathcal{U}}$ introduced so far, the symbol
for equality $=$ has the type
$\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}\rightarrow{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ which is not a type of object terms. This motivates the introduction
of object-level polymorphism [Gir72, Rey74]. However extending Simple type
theory with object-level polymorphism makes it inconsistent [Hur95, Coq86],
and similarly it makes the theory ${\mathcal{U}}$ inconsistent. So, object-
level polymorphism in ${\mathcal{U}}$ is restricted to prenex polymorphism.

To do so, we introduce a new constant Scheme of type TYPE

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Scheme}}:\mbox{\tt TYPE}$ (Scheme-decl)

a constant Els to embed the terms of type Scheme into terms of type TYPE

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Scheme}}\rightarrow\mbox{\tt TYPE}$ (Els-decl)

a constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}$
to embed the terms of type Set into terms of type Scheme and a rule connecting
these embeddings

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Scheme}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}$-decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}~{}x)~{}\hookrightarrow~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}$-red)

We then introduce a quantifier for the variables of type Set in the terms of
type Scheme and the associated rewriting rule

${\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}
A}}}:({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Scheme}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Scheme}}$ (  A -decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}}~{}({\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}
A}}}~{}p)~{}\hookrightarrow~{}\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}}~{}(p~{}x)$ (  A -red)

This way, the type of the identity function is
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}}}~{}{\left({{\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}
A}}}}~{}{\left(\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}}~{}{\left(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}x\right)}}\right)}\right)}$.
It reduces to
$\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x$. Therefore, it is inhabited by the term
$\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{\lambda{y}\,{:}\,{{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}},{y}}$. In a similar way, the symbol $=$ can then be given the
type
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}}}~{}{\left({{\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}
A}}}}~{}{\left(\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}}~{}{\left(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}\right)}}\right)}\right)}$
that reduces to
$\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}\rightarrow{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$.

###  3.18. Prenex predicative type quantification in propositions

When we express the reflexivity of the polymorphic equality, we need also to
quantify over a type variable, but now in a proposition. To be able to do so,
we introduce another quantifier and its associated rewriting rule

${\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}$\mathcal{A}$}}}:({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}$ (  $\mathcal{A}$ -decl)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}({\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}$\mathcal{A}$}}}~{}p)~{}\hookrightarrow~{}\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(p~{}x)$ (  $\mathcal{A}$ -red)

This way, the reflexivity of equality can be expressed as
$\left({{\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}$\mathcal{A}$}}}}~{}{\left(\lambda{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},{{{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}}~{}{x}}~{}{\left(\lambda{y}\,{:}\,{{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}}~{}{x}},{{{{=}~{}{x}}~{}{y}}~{}{y}}\right)}}\right)}\right)$.

###  3.19. The theory ${\mathcal{U}}$: putting everything together

The theory ${\mathcal{U}}$ is formed with the 43 axioms with a black bar at
the beginning of the line:
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$),
(Set), (El),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$),
(Prop), (Prf),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot}$),
($\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}}$),
(),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{c}}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\wedge_{c}}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee_{c}}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall_{c}}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists_{c}}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}$),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$),
(succ), (pred), (positive), (psub), (pair),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}$), (fst), (snd), (Set1), (set),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}$),
(Ty), (Scheme), (Els),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}$),
(  A ), (  $\mathcal{A}$ ).

Note that, strictly speaking, the declaration
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}$-decl) and the rule (pair-red) are not part of the theory
${\mathcal{U}}$, but of its extension ${\mathcal{U}}^{\dagger}$ used to define
the conversion on the terms of ${\mathcal{U}}$.

Among these axioms, 14 only have a constant declaration, 27 have a constant
declaration and one rewriting rule, and 2 have a constant declaration and two
rewriting rules. So $\Sigma_{{\mathcal{U}}}$ contains 43 declarations and
${\mathcal{R}}_{\mathcal{U}}$ 31 rules.

This large number of axioms is explained by the fact that
$\lambda\Pi/\\!\equiv$ is a weaker framework than Predicate logic. The 20
first axioms are needed just to construct notions that are primitive in
Predicate logic: terms, propositions, with their 13 constructive and classical
connectives and quantifiers, and proofs. So the theory ${\mathcal{U}}$ is just
23 axioms on top of the definition of Predicate logic.

It is also explained by the fact that axioms are more atomic than in Predicate
logic, for instance 4 axioms:
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$),
(succ), (pred), and (positive) are needed to express “the” axiom of infinity,
5 (psub), (pair),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}$), (fst), and (snd) to express predicate subtyping, 4
(Set1),(set),($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}$),(Ty)
to express dependent types and 5 (Scheme), (Els),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow}$),
(  A ), and (  $\mathcal{A}$ ) to express prenex polymorphism. The 5 remaining
axioms express propositions as objects
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$),
various forms of functionality
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$),
and
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}$),
and dependent implication
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}$).

##  4\. Sub-theories

Not all proofs require all these axioms. Many proofs can be expressed in sub-
theories built by bringing together some of the axioms of ${\mathcal{U}}$, but
not all.

Given subsets $\Sigma_{\mathcal{S}}$ of $\Sigma_{\mathcal{U}}$ and
${\mathcal{R}}_{\mathcal{S}}$ of ${\mathcal{R}}_{\mathcal{U}}$, we would like
to be sure that a proof in ${\mathcal{U}}$, using only constants in
$\Sigma_{\mathcal{S}}$, is a proof in
$\Sigma_{\mathcal{S}},{\mathcal{R}}_{\mathcal{S}}$. Such a result is trivial
in Predicate logic: for instance, a proof in ZFC which does not use the axiom
of choice is a proof in ZF, but it is less straightforward in
$\lambda\Pi/\\!\equiv$, because
$\Sigma_{\mathcal{S}},{\mathcal{R}}_{\mathcal{S}}$ might not be a theory. So
we should not consider any pair
$\Sigma_{\mathcal{S}},{\mathcal{R}}_{\mathcal{S}}$. For instance, as Set
occurs in the type of El, if we want El in $\Sigma_{\mathcal{S}}$, we must
take Set as well. In the same way, as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
succ}}~{}x)$ rewrites to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$, if
we want (positive) and (succ) in $\Sigma_{\mathcal{S}}$, we must include
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$ in
$\Sigma_{\mathcal{S}}$ and the rule rewriting
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
positive}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
succ}}~{}x)$ to
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top}$ in
${\mathcal{R}}_{\mathcal{S}}$.

This leads to a definition of a notion of sub-theory and to prove that, if
$\Sigma_{1},{\mathcal{R}}_{1}$ is a sub-theory of a theory
$\Sigma_{0},{\mathcal{R}}_{0}$, $\Gamma$, $t$ and $A$ are in
$\Lambda(\Sigma_{1})$, and $\Gamma\vdash_{\Sigma_{0},{\mathcal{R}}_{0}}t:A$,
then $\Gamma\vdash_{\Sigma_{1},{\mathcal{R}}_{1}}t:A$.

This property implies that, if $\pi$ is a proof of $A$ in ${\mathcal{U}}$ and
both $A$ and $\pi$ are in $\Lambda(\Sigma_{1})$, then $\pi$ is a proof of $A$
in $\Sigma_{1},{\mathcal{R}}_{1}$, but it does not imply that if $A$ is in
$\Lambda(\Sigma_{1})$ and $A$ has a proof in ${\mathcal{U}}$, then it has a
proof in $\Sigma_{1},{\mathcal{R}}_{1}$.

###  4.1. Fragments

[Fragment] A signature $\Sigma_{1}$ is included in a signature $\Sigma_{0}$,
$\Sigma_{1}\subseteq\Sigma_{0}$, if each declaration $c:A$ of $\Sigma_{1}$ is
a declaration of $\Sigma_{0}$.

A system $\Sigma_{1},{\mathcal{R}}_{1}$ is a fragment of a system
$\Sigma_{0},{\mathcal{R}}_{0}$, if the following conditions are satisfied:

  * •

$\Sigma_{1}\subseteq\Sigma_{0}$ and
${\mathcal{R}}_{1}\subseteq{\mathcal{R}}_{0}$;

  * •

for all $(c:A)\in\Sigma_{1}$, ${\mbox{\it const}}(A)\subseteq|\Sigma_{1}|$;

  * •

for all $\ell\hookrightarrow r\in{\mathcal{R}}_{0}$, if ${\mbox{\it
const}}(\ell)\subseteq|\Sigma_{1}|$, then ${\mbox{\it
const}}(r)\subseteq|\Sigma_{1}|$ and $\ell\hookrightarrow
r\in{\mathcal{R}}_{1}$.

We write $\vdash_{i}$ for $\vdash_{\Sigma_{i},{\mathcal{R}}_{i}}$,
$\hookrightarrow_{i}$ for $\hookrightarrow_{\beta{\mathcal{R}}_{i}}$, and
$\equiv_{i}$ for $\equiv_{\beta{\mathcal{R}}_{i}}$.

######  Lemma 11 (Preservation of reduction).

If $\Sigma_{1},{\mathcal{R}}_{1}$ is a fragment of
$\Sigma_{0},{\mathcal{R}}_{0}$, $t\in\Lambda(\Sigma_{1})$ and
$t\hookrightarrow_{0}u$, then $t\hookrightarrow_{1}u$ and
$u\in\Lambda(\Sigma_{1})$.

######  Proof 4.1.

By induction on the position where the rule is applied. We only detail the
case of a top reduction, the other cases easily following by induction
hypothesis.

So, let $\ell\hookrightarrow r$ be the rule used to rewrite $t$ in $u$ and
$\theta$ such that $t=\theta\ell$ and $u=\theta r$. As
$t\in\Lambda(\Sigma_{1})$, we have $\ell\in\Lambda(\Sigma_{1})$ and, for all
$x$ free in $\ell$, $\theta x\in\Lambda(\Sigma_{1})$. Thus, as
$\Sigma_{1},{\mathcal{R}}_{1}$ is a fragment of
$\Sigma_{0},{\mathcal{R}}_{0}$, $r\in\Lambda(\Sigma_{1})$ and
$\ell\hookrightarrow r\in{\mathcal{R}}_{1}$. Therefore $t\hookrightarrow_{1}u$
and $u=\theta r\in\Lambda(\Sigma_{1})$.

######  Lemma 12 (Preservation of confluence).

Every fragment of a confluent system is confluent.

######  Proof 4.2.

Let $\Sigma_{1},{\mathcal{R}}_{1}$ be a fragment of a confluent system
$\Sigma_{0},{\mathcal{R}}_{0}$. We prove that $\hookrightarrow_{1}$ is
confluent on $\Lambda(\Sigma_{1})$. Assume that $t,u,v\in\Lambda(\Sigma_{1})$,
$t\hookrightarrow_{1}^{*}u$ and $t\hookrightarrow_{1}^{*}v$. Since
$|\Sigma_{1}|\subseteq|\Sigma_{0}|$, we have $t,u,v\in\Lambda(\Sigma_{0})$.
Since ${\mathcal{R}}_{1}\subseteq{\mathcal{R}}_{0}$, we have
$t\hookrightarrow_{0}^{*}u$ and $t\hookrightarrow_{0}^{*}v$. By confluence of
$\hookrightarrow_{0}$ on $\Lambda(\Sigma_{0})$, there exists a $w$ in
$\Lambda(\Sigma_{0})$ such that $u\hookrightarrow_{0}^{*}w$ and
$v\hookrightarrow_{0}^{*}w$. Since $u,v\in\Lambda(\Sigma_{1})$, by Lemma 11,
$w\in\Lambda(\Sigma_{1})$, $u\hookrightarrow_{1}^{*}w$ and
$v\hookrightarrow_{1}^{*}w$.

[Sub-theory] A system $\Sigma_{1},{\mathcal{R}}_{1}$ is a sub-theory of a
theory $\Sigma_{0},{\mathcal{R}}_{0}$, if $\Sigma_{1},{\mathcal{R}}_{1}$ is a
fragment of $\Sigma_{0},{\mathcal{R}}_{0}$ and it is a theory. As we already
know that ${\mathcal{R}}_{1}$ is confluent, this amounts to say that each rule
of ${\mathcal{R}}_{1}$ preserves typing in $\Sigma_{1},{\mathcal{R}}_{1}$.

###  4.2. The fragment theorem

######  Theorem 13.

Let $\Sigma_{0},{\mathcal{R}}_{0}$ be a confluent system and
$\Sigma_{1},{\mathcal{R}}_{1}$ be a fragment of $\Sigma_{0},{\mathcal{R}}_{0}$
that preserves typing.

  * •

If the judgement $\Gamma\vdash_{0}t:D$ is derivable,
$\Gamma\in\Lambda(\Sigma_{1})$ and $t\in\Lambda(\Sigma_{1})$, then there
exists $D^{\prime}\in\Lambda(\Sigma_{1})$ such that
$D\hookrightarrow_{0}^{*}D^{\prime}$ and the judgement
$\Gamma\vdash_{1}t:D^{\prime}$ is derivable.

  * •

If the judgement $\vdash_{0}\Gamma~{}\mbox{well-formed}$ is derivable and
$\Gamma\in\Lambda(\Sigma_{1})$, then the judgement
$\vdash_{1}\Gamma~{}\mbox{well-formed}$ is derivable.

######  Proof 4.3.

By induction on the derivation. The important cases are (abs), (app), and
(conv). The other cases are a simple application of the induction hypothesis.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}\lambda{x}\,{:}\,{A},{t}:\Pi{x}\,{:}\,{A},B\lx@proof@logical@and\Gamma\vdash_{0}A:\mbox{\tt
TYPE}\Gamma,x:A\vdash_{0}B:s\Gamma,x:A\vdash_{0}t:B$

as $\Gamma$, $A$, and $t$ are in $\Lambda(\Sigma_{1})$, by induction
hypothesis, there exists $A^{\prime}$ in $\Lambda(\Sigma_{1})$ such that
$\mbox{\tt TYPE}\hookrightarrow^{*}_{0}A^{\prime}$ and
$\Gamma\vdash_{1}A:A^{\prime}$ is derivable, and there exists $B^{\prime}$ in
$\Lambda(\Sigma_{1})$ such that $B\hookrightarrow_{0}^{*}B^{\prime}$ and
$\Gamma,x:A\vdash_{1}t:B^{\prime}$ is derivable. As TYPE is a sort,
$A^{\prime}=\mbox{\tt TYPE}$. Therefore, $\Gamma\vdash_{1}A:\mbox{\tt TYPE}$
is derivable.

As $B$ is typable and every subterm of a typable term is typable, KIND does
not occur in $B$. As $B\hookrightarrow_{0}^{*}B^{\prime}$ and no rule contains
KIND, KIND does not occur in $B^{\prime}$ as well. Hence,
$B^{\prime}\neq\mbox{\tt KIND}$. By Lemma 1, as
$\Gamma,x:A\vdash_{1}t:B^{\prime}$ is derivable and $B^{\prime}\neq\mbox{\tt
KIND}$, there exists a sort $s^{\prime}$ such that
$\Gamma,x:A\vdash_{1}B^{\prime}:s^{\prime}$ is derivable.

Thus, by the rule (abs),
$\Gamma\vdash_{1}\lambda{x}\,{:}\,{A},{t}:\Pi{x}\,{:}\,{A},B^{\prime}$ is
derivable. So there is $D^{\prime}=\Pi{x}\,{:}\,{A},B^{\prime}$ in
$\Lambda(\Sigma_{1})$ such that
$\Pi{x}\,{:}\,{A},B\hookrightarrow_{0}^{*}D^{\prime}$ and
$\Gamma\vdash_{1}\lambda{x}\,{:}\,{A},{t}:D^{\prime}$ is derivable.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}t~{}u:(u/x)B\lx@proof@logical@and\Gamma\vdash_{0}t:\Pi{x}\,{:}\,{A},B\Gamma\vdash_{0}u:A$

as $\Gamma$, $t$, and $u$ are in $\Lambda(\Sigma_{1})$, by induction
hypothesis, there exist $C$ and $A_{2}$ in $\Lambda(\Sigma_{1})$, such that
$\Pi{x}\,{:}\,{A},B\hookrightarrow_{0}^{*}C$, $\Gamma\vdash_{1}t:C$ is
derivable, $A\hookrightarrow_{0}^{*}A_{2}$, and $\Gamma\vdash_{1}u:A_{2}$ is
derivable. As $\Pi{x}\,{:}\,{A},B\hookrightarrow_{0}^{*}C$ and rewriting rules
are of the form $(c~{}l_{1}\ldots l_{n}\hookrightarrow r)$, there exist
$A_{1}$ and $B_{1}$ in $\Lambda(\Sigma_{1})$ such that
$C=\Pi{x}\,{:}\,{A_{1}},B_{1}$, $A\hookrightarrow_{0}^{*}A_{1}$, and
$B\hookrightarrow_{0}^{*}B_{1}$. By confluence of $\hookrightarrow_{0}$, there
exists $A^{\prime}$ such that $A_{1}\hookrightarrow_{0}^{*}A^{\prime}$ and
$A_{2}\hookrightarrow_{0}^{*}A^{\prime}$. By Lemma 11, as
$A_{1}\in\Lambda(\Sigma_{1})$ and $A_{1}\hookrightarrow_{0}^{*}A^{\prime}$, we
have $A^{\prime}\in\Lambda(\Sigma_{1})$ and
$A_{1}\hookrightarrow_{1}^{*}A^{\prime}$. In a similar way, as
$A_{2}\in\Lambda(\Sigma_{1})$ and $A_{2}\hookrightarrow_{0}^{*}A^{\prime}$, we
have $A_{2}\hookrightarrow_{1}^{*}A^{\prime}$. By Lemma 1, as
$\Gamma\vdash_{1}t:\Pi{x}\,{:}\,{A_{1}},B_{1}$ is derivable and
$\Pi{x}\,{:}\,{A_{1}},B_{1}\neq\mbox{\tt KIND}$, there exists a sort $s$ such
that $\Gamma\vdash_{1}\Pi{x}\,{:}\,{A_{1}},B_{1}:s$ is derivable. Thus, by
Lemma 1, $\Gamma\vdash_{1}A_{1}:\mbox{\tt TYPE}$ is derivable.

As $\Gamma\vdash_{1}\Pi{x}\,{:}\,{A_{1}},B_{1}:s$,
$\Pi{x}\,{:}\,{A_{1}},B_{1}\hookrightarrow_{1}^{*}\Pi{x}\,{:}\,{A^{\prime}},B_{1}$,
and $\Sigma_{1},{\mathcal{R}}_{1}$ preserves typing,
$\Gamma\vdash_{1}\Pi{x}\,{:}\,{A^{\prime}},B_{1}:s$ is derivable. In a similar
way, as $\Gamma\vdash_{1}A_{1}:\mbox{\tt TYPE}$ is derivable, and
$A_{1}\hookrightarrow_{1}^{*}A^{\prime}$,
$\Gamma\vdash_{1}A^{\prime}:\mbox{\tt TYPE}$ is derivable. Therefore, by the
rule (conv), $\Gamma\vdash_{1}t:\Pi{x}\,{:}\,{A^{\prime}},B_{1}$ and
$\Gamma\vdash_{1}u:A^{\prime}$ are derivable. Therefore, by the rule (app),
$\Gamma\vdash_{1}t~{}u:(u/x)B_{1}$ is derivable. So there exists
$D^{\prime}=(u/x)B_{1}$ in $\Lambda(\Sigma_{1})$, such that
$(u/x)B\hookrightarrow_{0}^{*}D^{\prime}$ and
$\Gamma\vdash_{1}t~{}u:D^{\prime}$ is derivable.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}t:B\lx@proof@logical@and\Gamma\vdash_{0}t:A\Gamma\vdash_{0}B:s$

as $\Gamma$ and $t$ are in $\Lambda(\Sigma_{1})$, by induction hypothesis,
there exists $A^{\prime}$ in $\Lambda(\Sigma_{1})$ such that
$A\hookrightarrow_{0}^{*}A^{\prime}$ and $\Gamma\vdash_{1}t:A^{\prime}$ is
derivable. By confluence of $\hookrightarrow_{0}$, there exists $C$ such that
$A^{\prime}\hookrightarrow_{0}^{*}C$ and $B\hookrightarrow_{0}^{*}C$. As
$A^{\prime}\in\Lambda(\Sigma_{1})$ and $A^{\prime}\hookrightarrow_{0}^{*}C$ we
have, by Lemma 11, $C\in\Lambda(\Sigma_{1})$ and
$A^{\prime}\hookrightarrow_{1}^{*}C$.

As $B$ is typable and every subterm of a typable term is typable, KIND does
not occur in $B$. As $B\hookrightarrow_{0}^{*}C$ and no rule contains KIND,
KIND does not occur in $C$ as well. Thus $C\neq\mbox{\tt KIND}$. As
$A^{\prime}\hookrightarrow_{0}^{*}C$, $A^{\prime}\neq\mbox{\tt KIND}$. By
Lemma 1, as $\Gamma\vdash_{1}t:A^{\prime}$ and $A^{\prime}\neq\mbox{\tt
KIND}$, there exists a sort $s^{\prime}$ such that
$\Gamma\vdash_{1}A^{\prime}:s^{\prime}$ is derivable. Thus, as
$A^{\prime}\hookrightarrow_{1}^{*}C$, and $\Sigma_{1},{\mathcal{R}}_{1}$
preserves typing, $\Gamma\vdash_{1}C:s^{\prime}$ is derivable. a As
$\Gamma\vdash_{1}t:A^{\prime}$ and $\Gamma\vdash_{1}C:s^{\prime}$ are
derivable and $A^{\prime}\hookrightarrow_{1}C$, by the rule (conv),
$\Gamma\vdash_{1}t:C$ is derivable. Thus there exists $D^{\prime}=C$ in
$\Lambda(\Sigma_{1})$ such that $\Gamma\vdash_{1}t:D^{\prime}$ is derivable
and $B\hookrightarrow_{0}^{*}D^{\prime}$.

  * •

If the last rule of the derivation is

$\vdash_{0}[~{}]~{}\mbox{well-formed}$

by the rule (empty), $\vdash_{1}[~{}]~{}\mbox{well-formed}$ is derivable.

  * •

If the last rule of the derivation is

$\vdash_{0}\Gamma,x:A~{}\mbox{well-formed}\Gamma\vdash_{0}A:s$

as $\Gamma$ and $A$ are in $\Lambda(\Sigma_{1})$, by induction hypothesis,
there exist $A^{\prime}$ in $\Lambda(\Sigma_{1})$ such that
$s\hookrightarrow_{0}^{*}A^{\prime}$ and $\Gamma\vdash_{1}A:A^{\prime}$ is
derivable. As $s$ is a sort, $A^{\prime}=s$. Therefore, $\Gamma\vdash_{1}A:s$
is derivable and, by the rule (decl), $\vdash_{1}\Gamma,x:A~{}\mbox{well-
formed}$ is derivable.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}\mbox{\tt TYPE}:\mbox{\tt KIND}\vdash_{0}\Gamma~{}\mbox{well-
formed}$

as $\Gamma$ is in $\Lambda(\Sigma_{1})$, by induction hypothesis,
$\vdash_{1}\Gamma~{}\mbox{well-formed}$ is derivable. Thus, by the rule
(sort), $\Gamma\vdash_{1}\mbox{\tt TYPE}:\mbox{\tt KIND}$ is derivable. So
there exists $D^{\prime}=\mbox{\tt KIND}$ in $\Lambda(\Sigma_{1})$ such that
$\mbox{\tt KIND}\hookrightarrow_{0}^{*}D^{\prime}$ and
$\Gamma\vdash_{1}\mbox{\tt TYPE}:D^{\prime}$.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}c:A\vdash_{0}\Gamma~{}\mbox{well-
formed}~{}~{}~{}\vdash_{0}A:s$

as $\Gamma$ is in $\Lambda(\Sigma_{1})$, by induction hypothesis,
$\vdash_{1}\Gamma~{}\mbox{well-formed}$ is derivable. And as $c$ is in
$\Lambda(\Sigma_{1})$, it is in $|\Sigma_{1}|$, thus $c:A$ is in $\Sigma_{1}$
and, since $\Sigma_{1},{\mathcal{R}}_{1}$ is a fragment of
$\Sigma_{0},{\mathcal{R}}_{0}$, $A\in\Lambda(\Sigma_{1})$.

Thus, by induction hypothesis, there exists $A^{\prime}$ such that
$\vdash_{1}A:A^{\prime}$ is derivable and
$s\hookrightarrow_{0}^{*}A^{\prime}$. As $s$ is a sort, $A^{\prime}=s$. So
$\vdash_{1}A:s$ is derivable. Thus, by the rule (const), $\Gamma\vdash_{1}c:A$
is derivable. So, there exists $D^{\prime}=A$ in $\Lambda(\Sigma_{1})$ such
that $A\hookrightarrow_{0}^{*}D^{\prime}$ and $\Gamma\vdash_{1}c:D^{\prime}$
is derivable.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}x:A\vdash_{0}\Gamma~{}\mbox{well-formed}$

as $\Gamma$ is in $\Lambda(\Sigma_{1})$, by induction hypothesis,
$\vdash_{1}\Gamma~{}\mbox{well-formed}$ is derivable. Thus, by the rule (var),
$\Gamma\vdash_{1}x:A$ is derivable. So there exists $D^{\prime}=A$ in
$\Lambda(\Sigma_{1})$ such that $A\hookrightarrow_{0}^{*}D^{\prime}$ and
$\Gamma\vdash_{1}x:D^{\prime}$.

  * •

If the last rule of the derivation is

$\Gamma\vdash_{0}\Pi{x}\,{:}\,{A},B:s\lx@proof@logical@and\Gamma\vdash_{0}A:\mbox{\tt
TYPE}\Gamma,x:A\vdash_{0}B:s$

as $\Gamma$, $A$, and $B$ are in $\Lambda(\Sigma_{1})$, by induction
hypothesis, there exists $A^{\prime}$ in $\Lambda(\Sigma_{1})$ such that
$\mbox{\tt TYPE}\hookrightarrow_{0}^{*}A^{\prime}$ and
$\Gamma\vdash_{1}A:A^{\prime}$ is derivable and there exists $B^{\prime}$ in
$\Lambda(\Sigma_{1})$ such that $s\hookrightarrow_{0}^{*}B^{\prime}$ and
$\Gamma,x:A\vdash_{1}B:B^{\prime}$ is derivable. As TYPE and $s$ are sorts,
$A^{\prime}=\mbox{\tt TYPE}$ and $B^{\prime}=s$. Therefore,
$\Gamma\vdash_{1}A:\mbox{\tt TYPE}$ and $\Gamma,x:A\vdash_{1}B:s$ are
derivable. Thus, by the rule (prod), $\Gamma\vdash_{1}\Pi{x}\,{:}\,{A},B:s$ is
derivable. So there exists $D^{\prime}=s$ in $\Lambda(\Sigma_{1})$ such that
$s\hookrightarrow_{0}^{*}D^{\prime}$ and
$\Gamma\vdash_{1}\Pi{x}\,{:}\,{A},B:D^{\prime}$ is derivable.

######  Corollary 14.

Let $\Sigma_{0},{\mathcal{R}}_{0}$ be a confluent system,
$\Sigma_{1},{\mathcal{R}}_{1}$ be a fragment of $\Sigma_{0},{\mathcal{R}}_{0}$
that preserves typing. If $\Gamma\vdash_{0}t:D$,
$\Gamma\in\Lambda(\Sigma_{1})$, $t\in\Lambda(\Sigma_{1})$, and
$D\in\Lambda(\Sigma_{1})$, then $\Gamma\vdash_{1}t:D$.

In particular, if $\Sigma_{0},{\mathcal{R}}_{0}$ is a theory,
$\Sigma_{1},{\mathcal{R}}_{1}$ be a sub-theory of
$\Sigma_{0},{\mathcal{R}}_{0}$, $\Gamma\vdash_{0}t:D$,
$\Gamma\in\Lambda(\Sigma_{1})$, $t\in\Lambda(\Sigma_{1})$, and
$D\in\Lambda(\Sigma_{1})$, then $\Gamma\vdash_{1}t:D$.

######  Proof 4.4.

There is a $D^{\prime}\in\Lambda(\Sigma_{1})$ such that
$D\hookrightarrow_{0}^{*}D^{\prime}$ and $\Gamma\vdash_{1}t:D^{\prime}$. As
$D\in\Lambda(\Sigma_{1})$ and $D\hookrightarrow_{0}^{*}D^{\prime}$. By Lemma
11 we have $D\hookrightarrow_{1}^{*}D^{\prime}$, and we conclude with the rule
(conv).

######  Theorem 15 (Sub-theories of ${\mathcal{U}}$).

Every fragment $\Sigma_{1},{\mathcal{R}}_{1}$ of ${\mathcal{U}}$ (including
${\mathcal{U}}$ itself) is a theory, that is, is confluent and preserves
typing.

######  Proof 4.5.

The relation $\hookrightarrow_{\beta{\mathcal{R}}_{\mathcal{U}}}$ is confluent
on $\Lambda(\Sigma_{\mathcal{U}})$ since it is an orthogonal combinatory
reduction system [KvOvR93]. Hence, after the fragment theorem, it is
sufficient to prove that every rule of ${\mathcal{R}}_{\mathcal{U}}$ preserves
typing in any fragment $\Sigma_{1},{\mathcal{R}}_{1}$ containing the symbols
of the rule.

To this end, we will use the criterion described in [Bla20, Theorem 19] which
consists in computing the equations that must be satisfied for a rule left-
hand side to be typable, which are system-independent, and then check that the
right-hand side has the same type modulo these equations in the desired
system: for all rules $l\hookrightarrow r\in\Lambda(\Sigma_{1})$, sets of
equations ${\mathcal{E}}$ and terms $T$, if the inferred type of $l$ is $T$,
the typability constraints of $l$ are ${\mathcal{E}}$, and $r$ has type type
$T$ in the system $\Lambda(\Sigma_{1})$ whose conversion relation
$\equiv_{\beta{\mathcal{R}}{\mathcal{E}}}$ has been enriched with
${\mathcal{E}}$, then $l\hookrightarrow r$ preserves typing in
$\Lambda(\Sigma_{1})$.

This criterion can easily be checked for all the rules but (pred-red2) and
(fst-red) because, except in those two cases, the left-hand side and the
right-hand side have the same type.

In (pred-red2),
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pred}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
succ}}~{}x)\hookrightarrow x$, the left-hand side has type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ if the
equation
$type(x)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$
is satisfied. Modulo this equation, the right-hand side has type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$ in any
fragment containing the symbols of the rule.

In (fst-red),
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}}~{}t~{}p~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}~{}t^{\prime}~{}p^{\prime}~{}m)\hookrightarrow m$, the left-
hand side has type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t$ if $type(t)=Set$,
$type(p)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t\rightarrow Prop$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t^{\prime}~{}p^{\prime})={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)$,
$type(t^{\prime})={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}$,
$type(p^{\prime})={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t^{\prime}\rightarrow Prop$, and
$type(m)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t^{\prime}$. But, in ${\mathcal{U}}$, there is no rule of the form
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)\hookrightarrow r$. Hence, by confluence, the equation
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t^{\prime}~{}p^{\prime})={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}}~{}t~{}p)$ is equivalent to the equations $t^{\prime}=t$ and
$p^{\prime}=p$. Therefore, the right-hand side is of type
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}t$ in every fragment of ${\mathcal{U}}$ containing the symbols of the
rule.

##  5\. Examples of sub-theories of the theory ${\mathcal{U}}$

We finally identify 15 sub-theories of the theory ${\mathcal{U}}$, that
correspond to known theories. For each of these sub-theories
$\Sigma_{\mathcal{S}},{\mathcal{R}}_{\mathcal{S}}$, according to the Corollary
14, if $\Gamma$, $t$, and $A$ are in $\Lambda(\Sigma_{\mathcal{S}})$, and
$\Gamma\vdash_{\Sigma_{\mathcal{U}},{\mathcal{R}}_{\mathcal{U}}}t:A$, then
$\Gamma\vdash_{{\mathcal{R}}_{\mathcal{S}},\Sigma_{\mathcal{S}}}t:A$.

succ
---
pred
---
positive
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}^{\dagger}}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$
---
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto_{d}}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Scheme}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Els}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\uparrow},{\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}
A}}},{\rotatebox[origin={c}]{180.0}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}$\mathcal{A}$}}}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pi}$
---
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{d}}$
---
Set1
---
set
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Ty}},\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\rightsquigarrow_{d}}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
psub}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
pair}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
fst}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
snd}}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}_{c}},\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow_{c}},\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\wedge_{c}},\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\vee_{c}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall_{c}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\exists_{c}}$
---
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\leadsto}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}o}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\top},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bot},\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\neg}},$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$
---
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$
---
$\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$
---
Figure 2. The wind rose. In black: Minimal, Constructive, and Ecumenical
predicate logic. In orange: Minimal, Constructive, and Ecumenical simple type
theory. In green: Simple type theory with prenex polymorphism. In blue: Simple
type theory with predicate subtyping. In cyan: Simple type theory with
predicate subtyping and prenex polymorphism. In pink: the Calculus of
constructions with a constant
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$,
without and with prenex polymorphism.

###  5.1. Minimal predicate logic

The 8 axioms
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}$),
(Set), (El),
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}$),
(Prop), (Prf),
($\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}$),
and
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}$)
define Minimal predicate logic
$\Sigma_{\mathcal{M}},{\mathcal{R}}_{\mathcal{M}}$.

$\begin{array}[]{rcl}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}&:&\mbox{\tt
TYPE}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}&:&\mbox{\tt TYPE}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}&:&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\rightarrow\mbox{\tt TYPE}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}&:&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\iota}&\hookrightarrow&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}&:&\mbox{\tt TYPE}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}&:&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow\mbox{\tt TYPE}\\\
\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}&:&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}(x\mathbin{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Rightarrow}y)&\hookrightarrow&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prf}}~{}y\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall}&:&\Pi{x}\,{:}\,{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Set}}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
El}}~{}x\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}})\rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mbox{\it
Prop}}\\\