jmath amalg mathscr

[a] [a]

# Sharing proofs with predicative theories
through universe polymorphic elaboration

Thiago Felicissimo  and  Frédéric Blanqui  Université Paris-Saclay, INRIA
project, Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, 91190
France<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

As the development of formal proofs is a time-consuming task, it is important
to devise ways of sharing the already written proofs to prevent wasting time
redoing them. One of the challenges in this domain is to translate proofs
written in proof assistants based on impredicative logics to proof assistants
based on predicative logics, whenever impredicativity is not used in an
essential way.

In this paper we present a transformation for sharing proofs with a core
predicative system supporting prenex universe polymorphism (like in Agda). It
consists in trying to elaborate each term into a predicative universe
polymorphic term as general as possible. The use of universe polymorphism is
justified by the fact that mapping each universe to a fixed one in the target
theory is not sufficient in most cases. During the elaboration, we need to
solve unification problems in the equational theory of universe levels. In
order to do this, we give a complete characterization of when a single
equation admits a most general unifier. This characterization is then employed
in an algorithm which uses a constraint-postponement strategy to solve
unification problems.

The proposed translation is of course partial, but in practice allows one to
translate many proofs that do not use impredicativity in an essential way.
Indeed, it was implemented in the tool Predicativize and then used to
translate semi-automatically many non-trivial developments from Matita’s
library to Agda, including proofs of Bertrand’s Postulate and Fermat’s Little
Theorem, which (as far as we know) were not available in Agda yet.

###### Key words and phrases:

Type Theory, Impredicativity, Predicativity, Proof Translation, Universe
Polymorphism, Universe Polymorpic Elaboration, Unification for Universe
Levels, Agda, Dedukti

##  1\. Introduction

An important achievement of the research community in logic is the invention
of proof assistants. Such tools allow for interactively writing proofs, which
are then checked automatically and can then be reused in other developments.
Proof assistants do not only help mathematicians to make sure that their
proofs are indeed correct, but are also used to verify the correctness of
safety-critical software.

##### Interoperability of proof assistants

Unfortunately, a proof written in a proof assistant cannot be directly reused
in another one, which makes each tool isolated in its own library of proofs.
This is specially the case when considering two proof assistants with
incompatible logics, as in this case simply translating from one syntax to
another would not work. Therefore, in order to share proofs between systems it
is often required to do logical transformations.

A naive approach to share proofs from a proof assistant $A$ to a proof
assistant $B$ is to define a transformation acting directly on the syntax of
$A$ and then implement it using the codebase of $A$. However, this code would
be highly dependent on the implementation of $A$ and can easily become
outdated if the codebase of $A$ evolves. Moreover, if there is another proof
assistant $A^{\prime}$ whose logic is very similar to the one of $A$ then this
transformation would have to be implemented once again in order to be used
with $A^{\prime}$ — the translation is implementation dependent.

##### Logical Frameworks & Dedukti

A better solution is instead to first define the logics of all proof
assistants in a common formalism, a logical framework. Then, proof
transformations can be defined uniformly inside the logical framework. Hence,
such transformations do not depend on the implementations anymore, but instead
on the logics that are implemented.

The logical framework Dedukti [ABC+16] is a good candidate for a system where
multiple logics can be encoded, allowing for logical transformations to be
defined uniformly inside Dedukti. Indeed, first, the framework was already
shown to be sufficiently expressive to encode the logics of many proof
assistants [BDG+23]. Moreover, previous works have shown how proofs can be
transformed inside Dedukti. For instance, Thiré describes in [Thi18] a
transformation to translate a proof of Fermat’s Little Theorem from the
Calculus of Inductive Constructions to Higher Order Logic (HOL), which can
then be exported to multiple proof assistants such as HOL, PVS, Lean, etc.
Géran also used Dedukti to export the formalization of Euclid’s Elements Book
1 in Coq [BNW19] to several proof assistants [Gé].

##### (Im)Predicativity

One of the challenges in proof interoperability is sharing proofs coming from
impredicative proof assistants (the majority of them) with predicative ones
such as Agda. Indeed, impredicativity, which states that propositions can
refer to entities of arbitrary sizes, is a logical principle absent from
predicative systems. It is therefore clear that any proof that uses
impredicativity in an essential way cannot be translated to a predicative
system. Nevertheless, one can wonder if most proofs written in impredicative
systems really use impredicativity and, if not, how one could devise a way for
detecting and translating them to predicative systems.

##### A predicativization transformation

In this paper, we tackle this problem by proposing a transformation that tries
to do precisely this. Our translation works by forgetting all the universe
information of the initial impredicative term, and then trying to elaborate it
into a predicative universe-polymorphic term as general as possible. The need
for universe polymorphism arises from the fact that mapping each universe to a
unique one in the target theory does not work in most cases — this is
explained in details in Section 3.

##### Universe level unification

During the translation, we need to solve level unification problems which are
generated when elaborating the impredicative term into a universe polymorphic
one. We therefore develop a unification algorithm for the equational theory of
universe levels. This is done by first giving a novel and complete
characterization of which equations admit a most general unifier (m.g.u.),
along with an explicit description of a m.g.u. when it exists. This
characterization is then employed in a unification algorithm implementing a
constraint-postponement strategy: at each step, we look for an equation
admitting a m.g.u. and solve it while applying the obtained substitution to
the other equations, in the hope of bringing new ones to the fragment
admitting a m.g.u..

##### The implementation

Our predicativization algorithm was implemented on top of the DkCheck type-
checker for Dedukti with the tool Predicativize (openly available at
https://github.com/Deducteam/predicativize), allowing for the translation of
proofs semi-automatically inside Dedukti. These proofs can then be exported to
Agda, the main proof assistant based on predicative type theory.

##### Translating Matita’s arithmetic library

The tool has been used to translate to the proof assistant Agda the whole of
Matita’s arithmetic library in a semi-automatic way, making many important
mathematical developments available to Agda users. In particular, this work
has lead to (as far as we know) the first ever proofs of Fermat’s Little
Theorem and Bertrand’s Postulate in Agda. The proof of Bertrand’s Postulate in
Matita had even been the subject of a whole journal publication [AR12],
evidencing its complexity and importance. Thanks to Predicativize, the same
hard work did not have to be repeated to make it available in Agda, as the
transformation allowed the translation of the whole proof without any need of
specialist knowledge about it.

##### Outline

We start in Section 2 with an introduction to Dedukti, before moving to
Section 3, where we present informally the problems that appear when
translating proofs to predicative systems. We then introduce in Section 4 a
predicative universe-polymorphic system, which is a subsystem of Agda and is
used as the target of the translation. This is followed by Section 5, in which
we present the elaboration algorithm. Section 6 then contributes with a
complete characterization of equations admitting a m.g.u., which is then used
to give an algorithm for universe level unification. We then introduce the
tool Predicativize in Section 7, and describe the translation of Matita’s
arithmetic library in Section 8. Finally, Section 9 concludes and discusses
future work.

##### Related version

A preliminary version of this work [FBB23] was published in the proceedings of
the 31st EACSL Annual Conference on Computer Science Logic. This journal
version contains a number of improvements, among which are the following:

  1. (1)

A main novelty with respect to [FBB23] is that we provide a complete
characterization of when a single equation between universe levels admit a
m.g.u. (most general unifier), along with an explicit description of such a
m.g.u.. This characterization then allows us to give a much improved algorithm
for level unification, which in particular is complete for singleton problems,
whereas the original algorithm is not.

  2. (2)

The confluence proof of $\mathbb{UPP}$ in [FBB23] relied on the ad hoc
restriction that level variables could only be replaced by levels. We make
this condition more precise and integrate it in the definition of Dedukti by
adopting a presentation featuring confinement, a technique first proposed in
[ADJL17] which allows to isolate a first-order subset of terms from the
higher-order part of the syntax.

  3. (3)

Finally, most of the text has been rewritten in order to improve the
presentation.

##  2\. Dedukti

[EmptyCtx] ⋅⊢ [ExtCtx] Γ⊢A : Type Γ, α: A ⊢ α: A ∈Γ[Var] Γ⊢ Γ⊢α: A c : A ∈Σ or
c : A := u ∈Σ [Cons] Γ⊢ Γ⊢c : A f : Δ→A ∈Σ[ConsC] Γ⊢→e:Δ Γ⊢f(→e) : A[→iΔ↦→e]
[Sort] Γ⊢ Γ⊢Type: Kind A ≡B [Conv] Γ⊢t : A
Γ⊢B : s Γ⊢t : B A ≡B [ConvC] Γ⊢e : A
Γ⊢B : s Γ⊢e : B [Arrow] Γ⊢A : Type
Γ, α: A ⊢B : s Γ⊢(α: A) →B : s [Abs] Γ⊢A : Type
Γ, α: A ⊢B : s
Γ, α: A ⊢t : B Γ⊢α. t : (α: A) →B
[App] Γ⊢t : (x : A) →B
Γ⊢u : A Γ⊢t u : B[x ↦u] [AppC] Γ⊢t : (i : A) →B
Γ⊢e : A Γ⊢t e : B[i ↦e]

Figure 1. Typing rules of Dedukti

In this work we use Dedukti [ABC+16, BDG+23] as the framework in which we
express the various type theories and define our proof transformation.
Therefore, we start with a quick introduction to this system. For a reader
familiar with Dedukti, see Remark 1 for a comparison of our presentation of
Dedukti with more standard ones — in particular, note that we use a version
with confinement [ADJL17].

The syntax of Dedukti is defined by the following grammars. Here, $c$ ranges
in a set of constants $\mathcal{C}$ and $f$ ranges in a set of confined
constants $\mathcal{F}$. Similarly, $x$ ranges in an infinite set of variables
$\mathcal{V}$, whereas $i$ ranges in a infinite set of confined variables
$\mathcal{I}$, and we write $\alpha$ for either $x$ or $i$. We assume that the
sets $\mathcal{V}$, $\mathcal{I}$, $\mathcal{C}$ and $\mathcal{F}$ are
pairwise disjoint, and that each confined constant $f$ comes with an arity
$n\in\mathbb{N}$. We write $\alpha.t$ for abstraction, $(\alpha:A)\to B$ for
the dependent function type, and whenever $\alpha$ does not appear free in $B$
we write $A\to B$ instead of $(\alpha:A)\to B$. Note in the definition of the
grammars that confined terms are not terms, but can appear in the right side
of an application.

$\displaystyle(\textsc{Sorts})$ $\displaystyle s,s^{\prime}$
$\displaystyle::=\textsf{{Type}}\mid\textsf{{Kind}}$
$\displaystyle(\textsc{Variables})$ $\displaystyle\alpha,\alpha^{\prime}$
$\displaystyle::=x\mid i$ $\displaystyle(\textsc{Terms and Types})$
$\displaystyle A,B,t,u$ $\displaystyle::=x\mid s\mid c\mid(\alpha:A)\to
B\mid\alpha.t\mid t~{}u\mid t~{}e$ $\displaystyle(\textsc{Confined Terms})$
$\displaystyle e,e^{\prime}$ $\displaystyle::=i\mid
f(e_{\\_}{1},...,e_{\\_}{n})\hskip 30.00005pt\text{where }\textsf{arity}(f)=n$

A substitution $\theta$ is a finite set of pairs $x\mapsto t$ or $i\mapsto e$
— note that regular variables can only be mapped to regular terms, and
confined variables only to confined terms. We write $t[\theta]$ or $e[\theta]$
for its application to a term or confined term, and $\textsf{{dom}}(\theta)$
for the set of variables that are assigned to a term or confined term by
$\theta$.

A context $\Gamma$ is a finite sequence of entries of the form $\alpha:A$. A
signature $\Sigma$ is a finite sequence of entries of the form $c:A$ or
$c:A:=t$ or $f:(i_{\\_}{1}:B_{\\_}{1}..i_{\\_}{n}:B_{\\_}{n})\to A$, where we
must have $\text{arity}(f)=n$. We adopt the convention of writing the names of
constants of the signature in blue sans serif font.

A rewrite system $\mathcal{R}$ is a set of rewrite rules, which are pairs of
the form $c~{}\vec{t}\longrightarrow u$ or $f(\vec{e})\longrightarrow
e^{\prime}$. Given a signature $\Sigma$, we also consider the $\delta$ rules
allowing for the unfolding of definitions: we have $c\longrightarrow
t\in\delta$ for each $c:A:=t\in\Sigma$. We then denote by
$\longrightarrow_{\\_}\mathcal{R}$ the closure by context and substitution of
$\mathcal{R}$, and by $\longrightarrow_{\\_}\delta$ the closure by context of
$\delta$. Finally, we define $\longrightarrow_{\\_}{\beta}$ as the closure by
context of $(x.t)u\longrightarrow t[u/x]$,
$\longrightarrow_{\\_}{\beta_{\\_}{c}}$ as the closure by context of
$(i.t)e\longrightarrow t[e/i]$, and we write
$\longrightarrow_{\\_}{\beta\beta_{\\_}{c}\mathcal{R}\delta}$ for
$\longrightarrow_{\\_}\beta\cup\longrightarrow_{\\_}{\beta_{\\_}{c}}\cup\longrightarrow_{\\_}\mathcal{R}\cup\longrightarrow_{\\_}\delta$.

Rewriting allows us to define equality by computation, but not all equalities
can be defined like this in a well-behaved way, e.g. the commutativity of some
operator. Therefore, we also consider rewriting modulo equations [Bla03]. If
$\mathcal{E}$ is a set of equations of the form $t\simeq t^{\prime}$ or
$e\simeq e^{\prime}$, we write $\simeq_{\\_}{\mathcal{E}}$ for its congruence
closure — that is, its reflexitive, symmetric and transitive closure by
context and substitution. Because $\mathcal{R}$ and $\mathcal{E}$ are usually
kept fixed, in the following we write $\longrightarrow$ for
$\longrightarrow_{\\_}{\beta\beta_{\\_}{c}\mathcal{R}\delta}$, $\simeq$ for
$\simeq_{\\_}{\mathcal{E}}$ and $\equiv$ for the reflexitive, symmetric and
transitive closure of $\longrightarrow\cup\simeq$.

One notion central in Dedukti is that of theory, which is a triple
$\mathbb{T}=(\Sigma,\mathcal{R},\mathcal{E})$ where $\Sigma$ is a signature
and all constants appearing in $\mathcal{R}$ and $\mathcal{E}$ are declared in
$\Sigma$. Theories are used to define in Dedukti the object logics in which we
work (for instance, predicate logic). Given a theory $\mathbb{T}$, we define
the typing rules of Dedukti as the ones of Figure 1. There, we write
$\Gamma\vdash\vec{e}:\Delta$ for $\Gamma\vdash
e_{\\_}{k}:B_{\\_}{k}[i_{\\_}{1}\mapsto e_{\\_}{1}..i_{\\_}{k-1}\mapsto
e_{\\_}{k-1}]$ for all $k=1..n$ when
$\Delta=i_{\\_}{1}:B_{\\_}{1}..i_{\\_}{n}:B_{\\_}{n}$. Note moreover that the
signature $\Sigma$ and the conversion relation $\equiv$ are the ones defined
by the theory $\mathbb{T}$. Whenever the underlying theory is not clear from
the context, we write $\Gamma\vdash^{\mathbb{T}}t:A$.

A signature entry $c:A$ or $c:A:=t$ or $f:\Delta\to A$ is valid in
$\mathbb{T}$ if, respectively, $\vdash^{\mathbb{T}}A:s$ or
$\vdash^{\mathbb{T}}t:A$ or $\Delta\vdash^{\mathbb{T}}A:s$. A theory
$\mathbb{T}$ is then said to be well-formed if each entry in
$\Sigma_{\\_}{\mathbb{T}}$ is valid in
$(\Sigma^{\prime},\mathcal{R}^{\prime},\mathcal{E}^{\prime})$, where
$\Sigma^{\prime}$ is the prefix of $\Sigma_{\\_}{\mathbb{T}}$ preceding the
entry in question, and $\mathcal{R}^{\prime},\mathcal{E}^{\prime}$ are the
restrictions of $\mathcal{R}_{\\_}{\mathbb{T}},\mathcal{E}_{\\_}{\mathbb{T}}$
to rules and equations only containing constants in $\Sigma^{\prime}$.

######  Remark 1.

Compared with most presentations of Dedukti [ABC+16, BDG+23], ours feature
three relevant differences:

  1. (1)

We consider a syntax with non-annotated abstractions. As shown in [Dow93],
this leads to undecidable type checking. However, in this article we only work
with adequate encodings [Fel22], in which the only terms of interest are the
$\beta$-normal forms, for which type checking remains decidable and thus
annotations would be redundant.

  2. (2)

As mentioned previously, we consider a version with confinement. This notion,
first introduced in [ADJL17], allows to syntactically isolate a first-order
part of the syntax from the higher-order one. In [ADJL17] it is used to
provide a confluence criterion for non-left linear rewriting, and in this work
we also rely on it to show confluence of one of our theories.

  3. (3)

Like some other works [ADJL17, Gen20, Bla22], we consider a version of Dedukti
with rewriting modulo. This is essential to support some equations which
cannot be oriented into rewrite rules.

We recall the following basic metaproperties of Dedukti.

######  Proposition 2 (Basic metaproperties).

Let us write $\Gamma\sqsubseteq\Gamma^{\prime}$ when $\Gamma$ is a subsequence
of $\Gamma^{\prime}$.

Weakening:

Suppose $\Gamma\sqsubseteq\Gamma^{\prime}$ and $\Gamma^{\prime}\vdash$. If
$\Gamma\vdash t:A$ then $\Gamma^{\prime}\vdash t:A$, and if $\Gamma\vdash e:A$
then $\Gamma^{\prime}\vdash e:A$.

Substitution property:

If $\Gamma,x:B,\Gamma^{\prime}\vdash t:A$ and $\Gamma\vdash u:B$ then
$\Gamma,\Gamma^{\prime}[u/x]\vdash~{}t[u/x]~{}:~{}A[u/x]$. If
$\Gamma,i:B,\Gamma^{\prime}\vdash t:A$ and $\Gamma\vdash e:B$ then
$\Gamma,\Gamma^{\prime}[e/i]\vdash~{}t[e/i]~{}:~{}A[e/i]$

In the following, suppose that the underlying theory is well-formed.

Validity:

If $\Gamma\vdash t:A$ then either $A=\textsf{{Kind}}$ or $\Gamma\vdash A:s$
for some sort $s$

Subject reduction for $\delta$:

If $\Gamma\vdash t:A$ and $t\longrightarrow_{\\_}\delta t^{\prime}$ then
$\Gamma\vdash t^{\prime}:A$

We say that injectivity of dependent products holds when $(\alpha:A)\to
B\equiv(\alpha:A^{\prime})\to B^{\prime}$ implies $A\equiv A^{\prime}$ and
$B\equiv B^{\prime}$.

Subject reduction for $\beta$ and $\beta_{\\_}{c}$:

If injectivity of dependent products holds, then $\Gamma\vdash t:A$ and
$t\longrightarrow_{\\_}{\beta\beta_{\\_}{c}}t^{\prime}$ implies $\Gamma\vdash
t^{\prime}:A$.

A rule $l\longrightarrow r\in\mathcal{R}$ is said to preserve typing whenever
$\Gamma\vdash l[\theta]:A$ implies $\Gamma\vdash r[\theta]:A$, for every
$\theta,\Gamma,A$.

Subject reduction for $\mathcal{R}$:

If every rule in $\mathcal{R}$ preserves typing, then $\Gamma\vdash t:A$ and
$t\longrightarrow_{\\_}{\mathcal{R}}t^{\prime}$ implies $\Gamma\vdash
t^{\prime}:A$.

######  Proof 2.1.

We refer to [Bla01, Sai15a] for detailed proofs — even if there the definition
of the typing system is not exactly the same, the proofs for the variant used
here are straightforward adaptions of their proofs.

###  2.1. Defining type theories in Dedukti

We briefly review how one can define type theory with Russell-style universes
and dependent products [Fel22]111Other approaches also exists [CD07], however
as argued in [Fel22] they lead to less well-behaved encodings.. Given a set
$\mathfrak{S}$ of sorts, we start by declaring for each $s\in\mathfrak{S}$ a
framework type of object types, and a framework family of object terms indexed
by object types.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}:\textsf{{Type}}$
for $s\in\mathfrak{S}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}\to\textsf{{Type}}$
for $s\in\mathfrak{S}$

Then, an object type $A$ is represent as an element of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$
for some sort $s$, and an object term $t$ of type $A$ is represented as an
element of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A$,
where $s$ is the sort of $A$. That is, we write
$A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$
to represent the object-level judgment form $A~{}\textsf{type}_{\\_}{s}$, and
$t:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A$
to represent the object-level judgment form $t:_{\\_}{s}A$. As an example, if
we wanted to add natural numbers at sort $s_{\\_}{0}\in\mathfrak{S}$, we would
add constants
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Nat}}}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s_{\\_}{0}}$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{0}}}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s_{\\_}{0}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Nat}}}$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s_{\\_}{0}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Nat}}}\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s_{\\_}{0}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Nat}}}$,
and then a constant for its elimination principle along with its corresponding
rewrite rules.

We now add universes. To do this, we suppose we are given a functional
relation $\mathfrak{A}\subseteq\mathfrak{S}^{2}$, relating a sort to its
successor, and then postulate a type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}$
in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}}$
for each $(s,s^{\prime})\in\mathfrak{A}$. We now want the terms of type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}$
to correspond to the types in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$.
One way of achieving this is by postulating a definitional isomorphism
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}\simeq{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$,
which defines Coquand-style universes [Coq18, KHS19, ABKT19]. But because in
Dedukti we have type-level rewrite rules, we can replace this isomorphism with
an identification using a rewrite rule, yielding Russell-style universes. The
terms of the object-level type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}$
thus become the same as the object-level types at sort $s$.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}}$
for $(s,s^{\prime})\in\mathfrak{A}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}\longrightarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$
for $(s,s^{\prime})\in\mathfrak{A}$

Let us now define dependent products. We now suppose we are given a relation
$\mathfrak{R}\subseteq\mathfrak{S}^{3}$, which is functional when seen as a
relation $\mathfrak{S}^{2}\times\mathfrak{S}$. Then, for each pair
$(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$, we postulate a constant
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}$
mapping a type
$A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$
and a family
$B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}}$
to a type in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime\prime}}$.
Then we add abstraction
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}$,
mapping a family
$(x:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}(B~{}x)$
to an element of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime\prime}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}B)$,
and application
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}$,
mapping terms
$t:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime\prime}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}B)$
and
$u:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A$
to a term in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}(B~{}u)$.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}:(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s})\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime\prime}}$
for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}:(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s})\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}})\to$
$\displaystyle\hskip
15.00002pt((x:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}(B~{}x))\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime\prime}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}B)$
for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}:(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s})\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}})\to$
$\displaystyle\hskip
15.00002pt(t:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime\prime}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}B))\to(u:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}(B~{}u)$
for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$

Finally, we need to state the associated computation rule of dependent
products. The most natural choice would be to take the following rule.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}~{}A~{}B~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}~{}A~{}B~{}t)~{}u\longrightarrow
t~{}u$ for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$

However, this rule is non left-linear, and thus the rewrite system it
generates is non-confluent on raw terms [Klo63]. Instead, the standard
solution is to linearize [Bla05, Sai15b, MW96] the rule, by replacing the
second occurrences of variables $A,B$ by new fresh variables
$A^{\prime},B^{\prime}$.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}~{}A~{}B~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}~{}A^{\prime}~{}B^{\prime}~{}t)~{}u\longrightarrow
t~{}u$ for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$

Note that the left-hand side is not well-typed anymore, but this is not a
problem. Indeed, the important property we can show is that for all well-typed
instances of the left-hand side, $A$ becomes convertible to $A^{\prime}$ and
$B$ becomes convertible to $B^{\prime}$, which then guarantees that the right-
hand side is well-typed with the same type as the left one.

This concludes the definition of the theory, which is resumed in Figure 2. In
the following, we adopt some conventions to make the notation lighter. First,
we write
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}x:A.B$
for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}(x.B)$,
or
$A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}_{\\_}{s,s^{\prime}}B$ when
$x\not\in\textsf{{fv}}(B)$. Moreover, in order to keep examples readable it
will be essential to treat some arguments as implicit: namely, we will write
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}A$
instead of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}x:A.B$
instead of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}x:A.B$,
$t_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}u$
instead of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}~{}A~{}B~{}t~{}u$
and
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.t$
instead of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}~{}A~{}B~{}(x.t)$.
Nevertheless, note that this is just an informal notation, as there is no
support in Dedukti for omitting arguments — alternatively, one can work with a
framework with native support for erased arguments, such as [Fel23].

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}:\textsf{{Type}}$
for $s\in\mathfrak{S}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}\to\textsf{{Type}}$
for $s\in\mathfrak{S}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}}$
for $(s,s^{\prime})\in\mathfrak{A}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}\longrightarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}$
for $(s,s^{\prime})\in\mathfrak{A}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}:(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s})\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime\prime}}$
for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}:(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s})\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}})\to$
$\displaystyle\hskip
15.00002pt((x:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}(B~{}x))\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime\prime}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}B)$
for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}:(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s})\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s^{\prime}})\to$
$\displaystyle\hskip
15.00002pt(t:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime\prime}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}~{}A~{}B))\to(u:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s^{\prime}}~{}(B~{}u)$
for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}~{}A~{}B~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}~{}A^{\prime}~{}B^{\prime}~{}t)~{}u\longrightarrow
t~{}u$ for $(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}$ Figure 2. Dedukti
theory defined by specification $(\mathfrak{S},\mathfrak{A},\mathfrak{R})$

######  Remark 3.

In the Pure Type Systems (PTS) [Bar93] literature, the triple
$(\mathfrak{S},\mathfrak{A},\mathfrak{R})$ is known as a (functional) PTS
specification, and each such specification defines a PTS. The main result of
[Fel22] is that the theory in Figure 2 defines an adequate encoding of the
associated PTS in Dedukti.

##  3\. An informal look at predicativization

In this informal section we present the problem of proof predicativization and
discuss the challenges that arise through the use of examples. Even though the
examples might be unrealistic, they showcase real problems we found during our
first predicativization attempt of Fermat’s little theorem library in HOL
[Thi18] – some of them being already noted in [Del20].

We first start by defining the predicative theory $\mathbb{P}$ and the
impredicative theory $\mathbb{I}$, which will serve respectively as source and
target of our proof transformation. They are defined by instantiating the
theory of Figure 2 with the following specifications — following Remark 3,
they can equivalently be seen as the Pure Type Systems defined by these
specifications.

$\displaystyle\mathfrak{S}_{\\_}{\mathbb{I}}:=\\{\Omega,\square\\}$
$\displaystyle\mathfrak{S}_{\\_}{\mathbb{P}}:=\mathbb{N}$
$\displaystyle\mathfrak{A}_{\\_}{\mathbb{I}}:=\\{(\Omega,\square)\\}$
$\displaystyle\mathfrak{A}_{\\_}{\mathbb{P}}:=\\{(n,n+1)\mid
n\in\mathbb{N}\\}$
$\displaystyle\mathfrak{R}_{\\_}{\mathbb{I}}:=\\{(\Omega,\Omega,\Omega),(\square,\Omega,\Omega),(\square,\square,\square)\\}$
$\displaystyle\mathfrak{R}_{\\_}{\mathbb{P}}:=\\{(n,m,\textsf{max}\\{n,m\\})\mid
n,m\in\mathbb{N}\\}$

Note that in the theory $\mathbb{I}$ we have
$(\square,\Omega,\Omega)\in\mathfrak{R}_{\\_}{\mathbb{I}}$, and thus for
$\Gamma\vdash
A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{\square}$
and
$\Gamma,x:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}A\vdash
B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{\Omega}$
we have
$\Gamma\vdash{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}x:A.B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{\Omega}$.
Therefore, the sort $\Omega$ is closed under dependent products indexed over
types in $\square$, a larger sort, so $\mathbb{I}$ is indeed an impredicative
theory. Finally, we note that $\mathbb{P}$ is a subtheory of the one
implemented in Agda, whereas $\mathbb{I}$ is a subtheory of the ones
implemented in Coq, Matita, Isabelle, etc, justifying why they are of
interest.

In the following, a signature $\Phi$ is said to be well-formed in a theory
$\mathbb{T}$ when the theory
$(\Sigma^{\prime},\mathcal{R}_{\\_}{\mathbb{T}},\mathcal{E}_{\\_}{\mathbb{T}})$
is well-formed, where $\Sigma^{\prime}:=\Sigma_{\\_}{\mathbb{T}},\Phi$. In
this case, $\Phi$ is said to be a local signature, in contrast to
$\Sigma_{\\_}{\mathbb{T}}$ which is global. We will also write names of
constants in the local signature in sans serif black in order to distinguish
them, whereas names in the global one are still written in sans serif blue.

Then, the problem of proof predicativization consists in defining a
transformation such that, given a local signature $\Phi$ well-formed in
$\mathbb{I}$, allows to translate it to a local signature $\Phi^{\prime}$
well-formed in $\mathbb{P}$. Stated informally, we would like to translate
constants declarations $c:A$ (which represent axioms) and constant definitions
$c:A:=t$ (which also represent proofs) from $\mathbb{I}$ to $\mathbb{P}$ —
confined constant declarations $f:\Delta\to A$ will not be of interest here.
Note in particular that such a transformation is not applied to a single term
but to a sequence of constants and definitions, which can be related by
dependency — this dependency turns out to be a major issue as we will see.

Now that our basic notions are explained, let us try to predicativize proofs.
For our first step, consider a very simple development showing that for every
type $A$ in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}$
we can build a term in
$A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A$ — this is actually just the
polymorphic identity function at sort $\Omega$. Note that we adopt an Agda-
like syntax to display entries of the local signature.

$\displaystyle\textsf{id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$

To translate this simple development, the first idea that comes to mind is to
define a mapping on sorts: the sort $\Omega$ is mapped to $0$ and the universe
$\square$ is mapped to $1$. If this mapping defined a specification
morphism222That is, if $(s,s^{\prime})\in\mathfrak{A}_{\\_}{\mathbb{I}}$
implied $(\phi(s),\phi(s^{\prime}))\in\mathfrak{A}_{\\_}{\mathbb{P}}$ and
$(s,s^{\prime},s^{\prime\prime})\in\mathfrak{R}_{\\_}{\mathbb{I}}$ implied
$(\phi(s),\phi(s^{\prime}),\phi(s^{\prime\prime}))\in\mathfrak{R}_{\\_}{\mathbb{P}}$,
where $\phi:\mathfrak{S}_{\\_}{\mathbb{I}}\to\mathfrak{S}_{\\_}{\mathbb{P}}$
is the sort mapping. then this transformation would always produce a valid
definition in $\mathbb{P}$ [Geu93, Lemma 4.2.6]. Unfortunately, it is easy to
check that it does not define a specification morphism (worst, no function
$\mathfrak{S}_{\\_}{\mathbb{I}}\to\mathfrak{S}_{\\_}{\mathbb{P}}$ defines a
specification morphism). Nevertheless, this does not mean that it cannot
produce something well-typed in $\mathbb{P}$ in some cases. For instance, by
applying it to id we get the following entry, which is actually well-typed in
$\mathbb{P}$.

$\displaystyle\textsf{id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$

This naive approach however quickly fails when considering other cases. For
instance, suppose now that one adds the following definition.

$\displaystyle\textsf{id-to-
id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A){\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A))$ $\displaystyle\textsf{id-to-
id}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$

If we try to perform the same syntactic translation as before, we get the
following result.

$\displaystyle\textsf{id-to-
id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A){\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A))$ $\displaystyle\textsf{id-to-
id}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$

However, one can verify that this term is not well typed. Indeed, in the
original term one quantifies over all types in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}$
in the term
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A$, and because of impredicativity this
term stays at
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}$.
However, in $\mathbb{P}$ quantifying over all elements of the universe
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}$
in
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A$ lifts the overall type of the term to
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{1}$.
As id expects a term of type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}$,
the term
$\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$ is not well-typed.

The takeaway lesson from this first try is that impredicativity introduces a
kind of typical ambiguity, as it allows us to put in a single universe
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}$
types which, in a predicative setting, would have to be stratified and placed
in larger universes. Therefore, we should not translate every occurrence of
$\Omega$ as $0$ naively as we did, but try to compute for each occurrence of
$\Omega$ some natural number $n$ such that replacing it by $n$ would produce a
valid term in $\mathbb{P}$. In other words, we should erase all sort
information and then elaborate it into a well-typed term in $\mathbb{P}$.

Thankfully, performing such kind of transformations is exactly the goal of the
tool Universo [Thi20]. To understand how it works, let us come back to the
previous example. Universo starts here by replacing each sort $i$ by a fresh
metavariable representing a natural number.

$\displaystyle\textsf{id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$
$\displaystyle\textsf{id-to-
id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{2}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A){\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A))$ $\displaystyle\textsf{id-to-
id}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{4}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$

Then, in the following step Universo tries to elaborate the term into a well-
typed one in $\mathbb{P}$. To do so, it first tries to typecheck it and
generates constraints in the process. These constraints are then given to a
SMT solver, which is used to compute for each metavariable $i$ a natural
number so that the local signature is valid in $\mathbb{P}$. For instance,
applying Universo to our previous example would produce the following local
signature, which is indeed valid with respect to $\mathbb{P}$.

$\displaystyle\textsf{id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{1}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$
$\displaystyle\textsf{id-to-
id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A){\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A))$ $\displaystyle\textsf{id-to-
id}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{0}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$

By using Universo it is possible to go much further than with the naive method
shown before. Still, this approach also fails when being employed with real
libraries. To see the reason, consider the following minimum example, in which
one uses id twice to build another element of the same type.

$\displaystyle\textsf{id}^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}^{\prime}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}\textsf{id}$

If we repeat the same procedure as before, we get the following entries, which
when type checked generate unsolvable constraints.

$\displaystyle\textsf{id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$
$\displaystyle\textsf{id}^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{2}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}^{\prime}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}\textsf{id}$

The reason is that the application
$\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}\textsf{id}$
forces $i_{\\_}{1}$ to be both $i_{\\_}{3}$ and $i_{\\_}{3}+1$, which is of
course impossible. Therefore, the takeaway lesson from this second try is that
impredicativity does not only hide the fact that types need to be stratified,
but also the fact that they need to be usable at multiple levels of this
stratification. Indeed, in our example we would like to use id both at type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A$ and at type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}+1}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A$. In practice, when trying to translate
libraries using Universo we found that at very early stages a translated proof
or object was already needed at multiple universes at the same time, causing
the translation to fail.

Therefore, in order to properly compensate for the lack of impredicativity, we
should not translate entries by fixing once and for all their universes, but
instead we should let them vary by using universe polymorphism [HP91, ST14].
This feature, present in some type theories (and also in the one of Agda
[Tea]), allows defining terms containing universe variables, which can later
be instantiated at various concrete universes.

Our translation will then work by first computing for each definition or
declaration its set of constraints. However, instead of assigning concrete
values to metavariables, we perform unification which allows us to solve
constraints in a symbolic way. The result will then be a universe polymorphic
term, which will be usable at multiple universes when translating the next
entries. In order to define this formally, we first start in the next section
by refining the target type theory $\mathbb{P}$ with universe polymorphism.

##  4\. A Universe-Polymorphic Predicative Theory

In this section we define $\mathbb{UPP}$, a theory which refines $\mathbb{P}$
by internalizing sort annotations and allowing for prenex universe
polymorphism [HP91, Gen20]. This is in particular a subsystem of the one
underlying the Agda proof assistant [Tea].

The main change with respect to $\mathbb{P}$ is that, instead of indexing
constants externally, we index them inside the framework [Ass15]. To do this,
we first introduce in Dedukti a syntax for universe levels (which is just the
terminology used in the literature for predicative sorts, i.e. $\mathbb{N}$),
using the following declarations. Note that the constants
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}},{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}},{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}$ are declared as confined, which will be
needed later to show the confluence of the theory.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}}:\textsf{{Type}}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}:(i:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}}\hskip
10.00002pt\text{(confined)}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}:()\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}}\hskip
10.00002pt\text{(confined)}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}:(i:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}},i^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}}\hskip
10.00002pt\text{(confined)}$

In the following, we write $\hskip 1.99997pt\sqcup\hskip 1.99997pt$ in infix
notation, S in curryfied notation, and consider $\hskip 1.99997pt\sqcup\hskip
1.99997pt$ as having a lower precedence than S — for instance,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}j$
should be parsed as
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}(i),({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}(j))$.
We now call level a confined term containing only $\hskip
1.99997pt\sqcup\hskip 1.99997pt$, S or $0$ as constants, and from now on we
refer to them by the letter $l$. Equivalently, they are generated by the
following grammar.

$l,l^{\prime}::=i\mid{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}\mid{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}l\mid
l{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}l^{\prime}$

The definitions of Figure 2 are then replaced by the following ones. Note that
the two rewrite rules are presented in linearized form, in order for them to
be left-linear.

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}:(l:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to\textsf{{Type}}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}:(l:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l\to\textsf{{Type}}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}:(l:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}l)$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l^{\prime}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}~{}l)\longrightarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}:(l~{}l^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l)\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l^{\prime})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}(l{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}l^{\prime})$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}:(l~{}l^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l)\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l^{\prime})\to$
$\displaystyle\hskip
15.00002pt((x:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l^{\prime}~{}(B~{}x))\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(l{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}l^{\prime})~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}~{}l~{}l^{\prime}~{}A~{}B)$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}:(l~{}l^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to(A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l)\to(B:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l~{}A\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}l^{\prime})\to$
$\displaystyle\hskip
15.00002pt(t:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(l{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}l^{\prime})~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}~{}l~{}l^{\prime}~{}A~{}B))\to(u:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l~{}A)\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}l^{\prime}~{}(B~{}u)$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}~{}l~{}l^{\prime}~{}A~{}B~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}~{}l^{\prime\prime}~{}l^{\prime\prime\prime}~{}A^{\prime}~{}B^{\prime}~{}t)~{}u\longrightarrow
t~{}u$

In the following, we adopt a subscript notation for levels and write
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{l}$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{l}$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l}$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l,l^{\prime}}$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{l,l^{\prime}}$
and
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{l,l^{\prime}}$
to improve clarity. We also continue to write
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l,l^{\prime}}x:A.B$
for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l,l^{\prime}}~{}A~{}(x.B)$
or
$A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}_{\\_}{l,l^{\prime}}B$ when
$x\not\in\textsf{{fv}}(B)$. Finally, in order to keep examples readable we
also reuse our convention for implicit arguments and write
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}A$
for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{l}~{}A$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}x:A.B$
for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l,l^{\prime}}x:A.B$,
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.t$
for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{l,l^{\prime}}~{}A~{}B~{}(x.t)$,
and
$t_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}u$
for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{l,l^{\prime}}~{}A~{}B~{}t~{}u$.

Universe polymorphism can now be represented directly with the use of the
framework’s function type [Ass15]. Indeed, if a definition contains free level
variables, it can be made universe polymorphic by abstracting over such
variables. The following example illustrates this.

The universe polymorphic identity function is given by

$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{id}}}:(i:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{id}}}:=i.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}a.a$

This then allows to use id at any universe level: for instance, we can obtain
the polymorphic identity function at the level $0$ with the application id
$0$, which has type
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$.

######  Remark 4.

Note that unlike some other proposals [BCDE23] there is no object-level
operation for universe level abstraction, which is instead handled by the
framework function type. Therefore, universe polymorphic definitions are best
understood as schemes.

In order to finish the definition of the theory we need to specify the
definitional equality satisfied by levels, which is the one generated by the
following equations [Tea]. This then concludes the definition of the theory
$\mathbb{UPP}$.

$\displaystyle
i_{\\_}{1}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}(i_{\\_}{2}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}i_{\\_}{3})$
$\displaystyle\simeq(i_{\\_}{1}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}i_{\\_}{2}){\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}i_{\\_}{3}$
$\displaystyle{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}(i_{\\_}{1}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}i_{\\_}{2})$
$\displaystyle\simeq{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i_{\\_}{1}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i_{\\_}{2}$
$\displaystyle
i{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}$
$\displaystyle\simeq i$ $\displaystyle
i_{\\_}{1}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}i_{\\_}{2}$ $\displaystyle\simeq
i_{\\_}{2}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}i_{\\_}{1}$ $\displaystyle
i{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i$
$\displaystyle\simeq{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i$
$\displaystyle
i{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}i$ $\displaystyle\simeq i$

As we will see later with Proposition 23, the definition of $\simeq$ ensures
us that two levels are convertible exactly when they are arithmetically
equivalent, allowing us for instance to exchange
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}i{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}$
and
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i$.

###  4.1. Metatheory of $\mathbb{UPP}$

We now look at the metatheory of $\mathbb{UPP}$.

######  Proposition 5.

The theory $\mathbb{UPP}$ is well-formed.

######  Proof 4.1.

Can be easily verified manually, or automatically with Lambdapi [Ded].

######  Proposition 6.

The rewrite system $\mathcal{R}_{\\_}{\mathbb{UPP}}$ is confluent together
with the rules $\beta$, $\beta_{\\_}{c}$ and $\delta$.

######  Proof 4.2.

Follows from the fact that the rewrite rules define an orthogonal combinatory
rewrite system [Kvv93].

The following basic property is similar to [Voe14, Lemma 4.1.6] and shows that
$\longrightarrow$ and $\simeq$ interact well.

######  Proposition 7.

The relation $\simeq$ is a simulation with respect to $\longrightarrow$.
Diagrammatically,

${t}$${u}$${{\exists
t^{\prime}}}$${{u^{\prime}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$

######  Proof 4.3.

By induction on the rewrite context of $u\longrightarrow u^{\prime}$. The
induction steps are easy, we only show the base cases.

  1. (1)

If $u\longrightarrow u^{\prime}$ with a $\delta$ rule, then $u$ is a constant,
so $u=t$ and $t\longrightarrow u^{\prime}$.

  2. (2)

If
$u={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{l_{\\_}{1}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l_{\\_}{2}}\longrightarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{l_{\\_}{2}}=u^{\prime}$,
then we have
$t={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{l^{\prime}_{\\_}{1}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l^{\prime}_{\\_}{2}}$
with $l_{\\_}{k}\simeq l^{\prime}_{\\_}{k}$ for $k=1,2$. Therefore,
$t\longrightarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{l_{\\_}{2}^{\prime}}\simeq{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{l_{\\_}{2}}=u^{\prime}$.

  3. (3)

If
$u={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{l_{\\_}{1},l_{\\_}{2}}~{}A_{\\_}{1}~{}B_{\\_}{1}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{l_{\\_}{3},l_{\\_}{4}}~{}A_{\\_}{2}~{}B_{\\_}{2}~{}v)~{}s\longrightarrow
v~{}s=u^{\prime}$, then we have
$t={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{l^{\prime}_{\\_}{1},l^{\prime}_{\\_}{2}}~{}A^{\prime}_{\\_}{1}~{}B^{\prime}_{\\_}{1}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{l^{\prime}_{\\_}{3},l^{\prime}_{\\_}{4}}~{}A^{\prime}_{\\_}{2}~{}B^{\prime}_{\\_}{2}~{}v^{\prime})~{}s^{\prime}$
with $v\simeq v^{\prime}$, $s\simeq s^{\prime}$ and other relations that we
will not need. Therefore, $t\longrightarrow v^{\prime}~{}s^{\prime}\simeq
v~{}s=u^{\prime}$.

  4. (4)

If $u=(x.v)s\longrightarrow v[s/x]$, then $t=(x.v^{\prime})s^{\prime}$ with
$v\simeq v^{\prime}$ and $s\simeq s^{\prime}$. Therefore, $t\longrightarrow
v^{\prime}[s^{\prime}/x]$ and $v^{\prime}[s^{\prime}/x]\simeq v[s/x]$ follows
by stability under substitution.

  5. (5)

If $u=(i.v)l\longrightarrow v[l/i]$, then $t=(i.v^{\prime})l^{\prime}$ with
$v\simeq v^{\prime}$ and $l\simeq l^{\prime}$. Therefore, $t\longrightarrow
v^{\prime}[l^{\prime}/i]$ and $v^{\prime}[l^{\prime}/i]\simeq v[l/i]$ follows
by stability under substitution.

######  Remark 8.

We remark that the use of confinement was essential in the previous proof.
Indeed, had
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}},{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}},{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}$
been declared as regular constants, their associated equations would also have
to be declared with regular variables, and we would have $x\simeq
x{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip 1.99997pt$}}}x$. Then, this equation could be used in
cases in which $x$ is instantiated by redexes: for instance, we could have

${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}\simeq{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}\longrightarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\sqcup\hskip
1.99997pt$}}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}$

But then
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}$
is the only reduct of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}$,
yet
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}\simeq{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}\sqcup{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}~{}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$0$}}}}$
does not hold, showing that Proposition 7 fails in this setting.

We will need the following simple property about abstract rewriting. Recall
that an abstract equational rewrite system $(\blacktriangleright,\sim)$ is
given by a binary relation $\blacktriangleright~{}\subseteq X^{2}$ and an
equivalence relation $\sim~{}\subseteq X^{2}$. Then
$(\blacktriangleright,\sim)$ is said to be Church-Rossier modulo if
$x~{}(\blacktriangleright\cup\blacktriangleleft\cup\sim)^{*}~{}y$ implies
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}~{}y$, where we
write juxtaposition for composition of relations, and $\blacktriangleleft$ for
the inverse of $\blacktriangleright$.

######  Proposition 9.

Let $(\blacktriangleright,\sim)$ be an abstract equational rewrite system. If
$\blacktriangleright$ is confluent and $\sim$ is a simulation for
$\blacktriangleright$, then $(\blacktriangleright,\sim)$ is Church-Rossier
modulo.

######  Proof 4.4.

If $x~{}(\blacktriangleright\cup\blacktriangleleft\cup\sim)^{*}~{}y$, then we
have $x~{}(\blacktriangleright\cup\blacktriangleleft\cup\sim)^{n}~{}y$ for
some $n$. We prove the result by induction on $n$, the base case being
trivial. For the inductive step, we have

$x~{}(\blacktriangleright\cup\blacktriangleleft\cup\sim)^{n}~{}z~{}(\blacktriangleright\cup\blacktriangleleft\cup\sim)~{}y$

for some $z$. First note that by i.h. we have
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}~{}z$. We now have
three possibilities:

  1. (1)

$z\blacktriangleright y$ : We have
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}\blacktriangleright~{}y$,
and so by confluence we have
$x~{}{\blacktriangleright}^{*}\sim{\blacktriangleright}^{*}~{}{}^{*}{\blacktriangleleft}~{}y$.
Using the fact that $\sim$ is a simulation with respect to
$\blacktriangleright$, we then get
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}~{}y$.

  2. (2)

$z\blacktriangleleft y$ : We have
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}\blacktriangleleft~{}y$,
and thus $x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}~{}y$.

  3. (3)

$z\sim y$ : We have
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}\sim y$, thus
using the fact that $\sim$ is a simulation with respect to
$\blacktriangleright$, we get
$x~{}{\blacktriangleright}^{*}\sim{}^{*}{\blacktriangleleft}~{}y$.

######  Corollary 10 (Church-Rossier modulo).

If $t\equiv u$ then $t\mathrel{{\longrightarrow}^{*}}t^{\prime}\simeq
u^{\prime}\mathrel{{}^{*}{\longleftarrow}}u$.

######  Proof 4.5.

Direct consequence of Propositions 7 and 9.

The previous corollary has two important consequences. First, in order to
check $t\equiv u$ we do not need to employ matching modulo $\simeq$, but
instead only regular syntactic matching. This is important because it means
that in order to decide $\equiv$ we do not need to design a specific matching
algorithm for $\simeq$, but only to decide $\simeq$ (which is indeed decidable
by Theorem 22) and to show $\longrightarrow$ to be strongly normalized for
well-typed terms (a property we conjecture to be true). Second, Church-Rossier
modulo easily implies injectivity of type formers, from which subject
reduction follows, a property that will be essential to show soundness of
elaboration (in particular, it is used in Theorem 15).

######  Proposition 11 (Injectivity of type formes).

  * •

${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l}\equiv{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l^{\prime}}$
implies $l\equiv l^{\prime}$.

  * •

${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l_{\\_}{A},l_{\\_}{B}}x:A.B\equiv{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l_{\\_}{A^{\prime}},l_{\\_}{B^{\prime}}}x:A^{\prime}.B^{\prime}$
implies $l_{\\_}{A}\equiv l_{\\_}{A^{\prime}}$ and $l_{\\_}{B}\equiv
l_{\\_}{B^{\prime}}$ and $A\equiv A^{\prime}$ and $B\equiv B^{\prime}$.

######  Proof 4.6.

If
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l}\equiv{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l^{\prime}}$
then
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l}\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{l^{\prime}}$
and thus
$l\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}l^{\prime}$.
Similarly, if
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l_{\\_}{A},l_{\\_}{B}}x:A.B\equiv{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l_{\\_}{A^{\prime}},l_{\\_}{B^{\prime}}}x:A^{\prime}.B^{\prime}$
then
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l_{\\_}{A},l_{\\_}{B}}x:A.B\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{l_{\\_}{A^{\prime}},l_{\\_}{B^{\prime}}}x:A^{\prime}.B^{\prime}$
and thus
$l_{\\_}{A}\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}l_{\\_}{A^{\prime}}$
and
$l_{\\_}{B}\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}l_{\\_}{B^{\prime}}$
and
$A\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}A^{\prime}$
and
$B\mathrel{{\longrightarrow}^{*}}\simeq\mathrel{{}^{*}{\longleftarrow}}B^{\prime}$.

######  Proposition 12 (Subject Reduction).

If $\Gamma\vdash t:A$ and $t\longrightarrow t^{\prime}$ then $\Gamma\vdash
t^{\prime}:A$.

######  Proof 4.7.

From Church-Rossier modulo we get the injectivity of the framework’s dependent
function type, so from Proposition 2 we conclude subject reduction of
$\delta$, $\beta$ and $\beta_{\\_}{c}$.

By Proposition 2 once again, to show subject reduction for
$\mathcal{R}_{\\_}{\mathbb{UPP}}$ it suffices to prove that all rewrite rules
preserve typing, which easily follows from inversion of typing and Proposition
11. Alternatively, preservation of typing can also be verified using Lambdapi
[Ded, Bla20] or DkCheck [Sai15b].

######  Remark 13.

Injectivity of type formers and subject reduction rely on Church-Rossier
modulo, which in turn is shown using Proposition 7. As discussed in Remark 8,
the proof of this proposition crucially relies on the use of confinement, so
it is less clear how to derive Church-Rossier modulo in a setting without it.
Because $\mathcal{R}_{\\_}{\mathbb{UPP}}$ is left-linear and there are no
critical pairs between $\mathcal{R}_{\\_}{\mathbb{UPP}}$ and
$\mathcal{E}_{\\_}{\mathbb{UPP}}$, nor between
$\mathcal{R}_{\\_}{\mathbb{UPP}}$ and itself, one possibility would be to
apply [MN98, Theorem 5.11] to show the restriction of $\equiv$ to strongly
normalizing (s.n.) terms to be Church-Rossier modulo. However, to show Church-
Rossier modulo for the well-typed restriction of $\equiv$ and then subject
reduction we would then need to show $\longrightarrow$ to be s.n. for well-
typed terms. The use of confinement is thus an interesting alternative to this
option, as it allows us to establish the main correctness property of
elaboration (Theorem 15) without relying on strong normalization.

##  5\. Universe-polymorphic elaboration

We are now ready to define the (partial) transformation of a local signature
$\Phi$ to the theory $\mathbb{UPP}$. As hinted at the end of Section 3, our
translation works by incrementally trying to elaborate each entry of $\Phi$
into a universe-polymorphic one in $\mathbb{UPP}$, such that at the end we get
a local signature $\Phi_{\\_}{\mathbb{UPP}}$ well-formed in $\mathbb{UPP}$, if
no errors are produced in the process.

In order to explain it, we now suppose that we have already translated a local
signature $\Phi$ to a local signature $\Phi_{\\_}{\mathbb{UPP}}$ well-formed
in $\mathbb{UPP}$, and try to translate a new entry either of the form $c:A$
or $c:A:=t$. In order to understand all the following steps intuitively, we
will make use of a running example. Note that, following our previously
established convention, we keep some arguments implicit in order to improve
readability. The last example of Section 3 corresponds to the following local
signature, which is well-formed in $\mathbb{I}$.

$\displaystyle\textsf{id}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$
$\displaystyle\textsf{id}^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}^{\prime}:=\textsf{id}_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}\textsf{id}$

Let us suppose that the first entry of the signature has already been
translated, giving the following local signature $\Phi_{\\_}{\mathbb{UPP}}$.

$\displaystyle\textsf{id}:(i:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}:=i.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}A.{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}x.x$

Therefore, as a running example, we will translate step by step the second
entry $\textsf{id}^{\prime}$.

###  5.1. Schematic terms

The source syntax of our elaborator will be the one of $\mathbb{UPP}$, but
where the only allowed confined terms are unsolved confined variables $i$ — we
henceforth call such terms schematic terms. Therefore, in order to translate
proofs from $\mathbb{I}$ the first step is defining a translation from the
syntax of $\mathbb{I}$ to the schematic terms of $\mathbb{UPP}$, given by
Figure 3. Note that the translation is not defined for terms of the form
$t~{}e$ or $i.t$ or $(i:A)\to B$ because these are not used in the theory
$\mathbb{I}$. Moreover, because the first step is erasing all sort
information, this actually defines a translation starting from any theory
defined by instantiating Figure 2 with a specification. Therefore, it can also
be applied to theories using much more complex universe hierarchies, such as
those of the proof assistants Matita or Coq.

$\displaystyle|x|:=x$ $\displaystyle|t~{}u|:=|t||u|$
$\displaystyle|x.t|:=x.|t|$ $\displaystyle|(x:A)\to B|:=(x:|A|)\to|B|$
$\displaystyle|\textsf{{Type}}|:=\textsf{{Type}}$
$\displaystyle|\textsf{{Kind}}|:=\textsf{{Kind}}$
$\displaystyle|c|:=c~{}i_{\\_}{1}..i_{\\_}{k}\quad\text{if
}c:(j_{\\_}{1}..j_{\\_}{k}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to
A\in\Phi_{\\_}{\mathbb{UPP}}$

$\displaystyle|{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}_{\\_}{s}|:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Ty}}}~{}i$
$\displaystyle|{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}_{\\_}{s}|:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}i$
$\displaystyle|{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{s}|:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}~{}i$
$\displaystyle|{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{s,s^{\prime}}|:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}~{}i~{}i^{\prime}$
$\displaystyle|{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}_{\\_}{s,s^{\prime}}|:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\lambda$}}}~{}i~{}i^{\prime}$
$\displaystyle|{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}_{\\_}{s,s^{\prime}}|:={\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}~{}i~{}i^{\prime}$

Figure 3. Translation from the syntax of Figure 2 to the schematic terms of
$\mathbb{UPP}$
(each inserted level variable is assumed to be different from the previous
ones)

Let us explain the translation of Figure 3. First, all of the constants in the
definition of $\mathbb{I}$ are mapped to their correspondants in
$\mathbb{UPP}$, except that they are also applied to fresh level variables
which are to be solved during elaboration. Then, constants from $\Phi$ are
translated as they are, except that they are also given fresh level variables
in order to fill in the number of level arguments that they expect. Note that
this second step is necessary because the translation of the entries preceding
the current one introduced new dependencies on level variables which were not
present in $\mathbb{I}$. When applying $|-|$ to $\textsf{id}^{\prime}$ we get
the following entry.

$\displaystyle\textsf{id}^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}^{\prime}:=(\textsf{id}~{}i_{\\_}{2})_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}(\textsf{id}~{}i_{\\_}{4})$

Note that the occurrences of
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{\Omega}$
have been replaced by
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i}$
(which is just a notation for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}~{}i$)
for some fresh $i$. Moreover, because the type of id in
$\Phi_{\\_}{\mathbb{UPP}}$ is
$(i:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}(\Pi
A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$, each occurrence of id is replaced by
$\textsf{id}~{}i$ for some fresh $i$. Finally, note that because of implicit
arguments we are hiding many new variables that were also inserted. For
instance, the subterm
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A$ is an implicit notation for
${\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}_{\\_}{i_{\\_}{5},i_{\\_}{6}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}_{\\_}{i_{\\_}{7},i_{\\_}{8}}A$. However,
the term
$(\textsf{id}~{}i_{\\_}{2})_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}(\textsf{id}~{}i_{\\_}{4})$
without implicit arguments would not even fit into a line, so for readability
reasons we will not write it fully.

###  5.2. Computing constraints

Our next step is then to define a type system for computing constraints. This
is done by adapting the seminal work of Harper and Pollack [HP91], with the
difference that our system will be bidirectional.

In regular bidirectional type systems, the typing judgment $\Gamma\vdash t:A$
is split in modes infer $\Gamma\vdash t\Rightarrow A$ and check $\Gamma\vdash
t\Leftarrow A$. In mode infer we start with $\Gamma,t$ and we should find a
type $A$ for $t$ in $\Gamma$, whereas in mode check we are given $\Gamma,t,A$
and we should check that $t$ indeed has type $A$ in $\Gamma$. Crucial in
bidirectional typing is the proper bookkeeping of pre-conditions and post-
conditions, which are resumed in the following table — there, we mark inputs
with $-$ and outputs with $+$.

Judgment | Pre-condition | Post-condition
---|---|---
$\Gamma^{-}\vdash t^{-}\Rightarrow A^{+}$ | $\Gamma\vdash$ | $\Gamma\vdash t:A$
$\Gamma^{-}\vdash t^{-}\Leftarrow A^{-}$ | $\Gamma\vdash A:s$ | $\Gamma\vdash t:A$

In order to refine these judgments with constraints, let us start with some
preliminary definitions. A (level unification) problem $\mathcal{C}$ is a set
containing constraints of the form
$l\overset{\scriptscriptstyle?}{=}l^{\prime}$, referred to also as equations.
In the following definitions, let $\theta$ be a substitution whose domain only
contains level variables. We write $\theta\vDash\mathcal{C}$ when
$l[\theta]\simeq l^{\prime}[\theta]$ for all
$l\overset{\scriptscriptstyle?}{=}l^{\prime}\in\mathcal{C}$, in which case
$\theta$ is called a unifier (or solution) for $\mathcal{C}$. Let
$\Xi_{\\_}{\theta}$ be a context containing
$j:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}}$
for each level variable appearing in $i[\theta]$, for each level variable $i$
inserted in the schematic terms. We then also write
$\Gamma\vdash_{\\_}{\mathcal{C}}$ when, for all $\theta$,
$\theta\vDash\mathcal{C}$ implies $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash$,
and $\Gamma\vdash_{\\_}{\mathcal{C}}t:A$ when, for all $\theta$,
$\theta\vDash\mathcal{C}$ implies $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash
t[\theta]:A[\theta]$.

Intuitively, just like the context $\Gamma$ in $\Gamma\vdash t:A$ allows us to
state a typing judgment $t:A$ with typing hypothesis of the form
$x:B\in\Gamma$, the set of constraints $\mathcal{C}$ in
$\Gamma\vdash_{\\_}{\mathcal{C}}t:A$ refines this with equational hypothesis
of the form $l\simeq l^{\prime}$. With this in mind, we can now given the new
typing judgments in the following table. Compared with the previous table, we
now start with a set of constraints $\mathcal{D}$, which guarantees that the
pre-condition holds, and in the process we must also find constraints
$\mathcal{C}$ ensuring that the post-condition holds.

Judgment | Pre-condition | Post-condition
---|---|---
$\Gamma^{-}\uparrow\mathcal{D}^{-}\vdash t^{-}\Rightarrow A^{+}\downarrow\mathcal{C}^{+}$ | $\Gamma\vdash_{\\_}{\mathcal{D}}$ | $\Gamma\vdash_{\\_}{\mathcal{C}\cup\mathcal{D}}t:A$
$\Gamma^{-}\uparrow\mathcal{D}^{-}\vdash t^{-}\Leftarrow A^{-}\downarrow\mathcal{C}^{+}$ | $\Gamma\vdash_{\\_}{\mathcal{D}}A:s$ | $\Gamma\vdash_{\\_}{\mathcal{C}\cup\mathcal{D}}t:A$

We now come to the definition of the bidirectional type system for computing
constraints, given in Figure 4 — we mark inputs with $-$ and outputs with $+$.
Note that it also relies on two new conversion judgments $A\equiv
B\downarrow\mathcal{C}$ and $A\equiv_{\\_}{\text{whnf}}B\downarrow\mathcal{C}$
used to compute a set of constraints needed for the conversion to hold. In the
given rules, we write $t\longrightarrow^{\text{wh}}u$ for the reduction of $t$
to a weak-head normal form (whnf) $u$.

$A^{-}\equiv B^{-}\downarrow\mathcal{C}^{+}$ A ⟶^wh A’
B ⟶^wh B’
A’ ≡whnf B’ ↓C A ≡B ↓C
$A^{-}\equiv_{\\_}{\text{whnf}}B^{-}\downarrow\mathcal{C}^{+}$ t = x, c, s t
≡whnf t ↓∅ t ≡t’ ↓C α.t ≡whnf α. t’↓C A ≡A’ ↓C1
B ≡B’ ↓C2 (α: A) →B ≡whnf (α: A’) →B’ ↓C1∪C2 t ≡whnf t’ ↓C1
u ≡u’ ↓C2 t u ≡whnf t’ u’ ↓C1∪C2 t ≡whnf t’ ↓C t l ≡whnf t’ l’ ↓C∪{l ?=l’}
$\Gamma^{-}\uparrow\mathcal{D}^{-}\vdash t^{-}\Leftarrow
A^{-}\downarrow\mathcal{C}^{+}$ [Switch] Γ↑D ⊢t ⇒A↓C1
A ≡B↓C2 Γ↑D ⊢t ⇐B↓C1 ∪C2 [Abs] C ⟶^wh (x : A) →B

Γ,x:A ↑D ⊢t ⇐B ↓C Γ↑D ⊢x.t ⇐C ↓C $\Gamma^{-}\uparrow\mathcal{D}^{-}\vdash
t^{-}\Rightarrow A^{+}\downarrow\mathcal{C}^{+}$ [Var] x : A ∈Γ Γ↑D ⊢x ⇒A ↓∅
[Cons] c : A ∈Σ, Φ or  c : A := t ∈Σ, Φ

A = (j1..jk : Lvl) →B Γ↑D ⊢c i1..ik ⇒B[→i/→j] ↓∅
[Sort] Γ↑D ⊢Type⇒Kind↓∅ [Pi] Γ↑D ⊢A ⇐Type↓C1

Γ, x : A ↑D ∪C1⊢B⇒C ↓C2
C ⟶^wh s Γ↑D ⊢(x : A) →B ⇒s ↓C1 ∪C2 [App] Γ↑D ⊢t ⇒C ↓C1
C ⟶^wh (x : A) →B
Γ↑D ∪C1 ⊢u ⇐A ↓C2 Γ↑D ⊢t u ⇒B[u/x] ↓C1 ∪C2

Figure 4. Bidirectional type system for computing universe level constraints

In order to compute the constraints of the entry

$\displaystyle\textsf{id}^{\prime}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)$
$\displaystyle\textsf{id}^{\prime}:=(\textsf{id}~{}i_{\\_}{2})_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}(\textsf{id}~{}i_{\\_}{4})$

we first compute the constraints necessary for its type to be of type Type:

$()\uparrow\emptyset\vdash{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)\Leftarrow\textsf{{Type}}\downarrow\mathcal{C}_{\\_}{1}$

Then, once we know that the type is valid under the constraints
$\mathcal{C}_{\\_}{1}$, we can do the same with the term:

$()\uparrow\mathcal{C}_{\\_}{1}\vdash(\textsf{id}~{}i_{\\_}{2})_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{3}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip
1.99997pt$}}}A)_{\\_}{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$@$}}}}(\textsf{id}~{}i_{\\_}{4})\Leftarrow{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Tm}}}~{}({\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\Pi$}}}A:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{U}}}_{\\_}{i_{\\_}{1}}.A{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{$\hskip
1.99997pt\leadsto\hskip 1.99997pt$}}}A)\downarrow\mathcal{C}_{\\_}2$

In the end we get the constraints

$\mathcal{C}_{\\_}{1}\cup\mathcal{C}_{\\_}{2}:=\\{{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{S}}}~{}i_{\\_}{1}\overset{\scriptscriptstyle?}{=}i_{\\_}{2},i_{\\_}{1}\overset{\scriptscriptstyle?}{=}i_{\\_}{3},i_{\\_}{1}\overset{\scriptscriptstyle?}{=}i_{\\_}{4},...\\}$

where the hidden constraints concern level variables appearing in implicit
arguments.

We can show the soundness of the new type system by verifying that each rule
locally preserves the invariants of the table — this is the essence of the
proof of Theorem 15. Before showing it, we first need a lemma establishing
soundness of conversion checking.

######  Lemma 14.

Suppose that $A\equiv B\downarrow\mathcal{C}$ or
$A\equiv_{\\_}{\textup{whnf}}B\downarrow\mathcal{C}$. If
$\theta\vDash\mathcal{C}$ then $A[\theta]\equiv B[\theta]$.

######  Proof 5.1.

By an easy mutual induction on $A\equiv B\downarrow\mathcal{C}$ and
$A\equiv_{\\_}{\textup{whnf}}B\downarrow\mathcal{C}$.

######  Theorem 15 (Soundness of type system for computing constraints).

  * •

If $\Gamma\vdash_{\\_}{\mathcal{D}}A:s$ and $\Gamma\uparrow\mathcal{D}\vdash
t\Leftarrow A\downarrow\mathcal{C}$ then
$\Gamma\vdash_{\\_}{\mathcal{C}\cup\mathcal{D}}t:A$

  * •

If $\Gamma\vdash_{\\_}{\mathcal{D}}$ and $\Gamma\uparrow\mathcal{D}\vdash
t\Rightarrow A\downarrow\mathcal{C}$ then
$\Gamma\vdash_{\\_}{\mathcal{C}\cup\mathcal{D}}t:A$

######  Proof 5.2.

By mutual induction on the elaborator judgments.

  * •

Case Var : Let $\theta\vDash\emptyset\cup\mathcal{D}$. By hypothesis we have
$\Xi_{\\_}{\theta},\Gamma[\theta]\vdash$, and hence
$\Xi_{\\_}{\theta},\Gamma[\theta]\vdash x:A[\theta]$.

  * •

Case Sort : Similar to the previous case.

  * •

Case Cons : Let $\theta\vDash\emptyset\cup\mathcal{D}$. By hypothesis we have
$\Xi_{\\_}{\theta},\Gamma[\theta]\vdash$, and hence
$\Xi_{\\_}{\theta},\Gamma[\theta]\vdash
c:(j_{\\_}{1}..j_{\\_}{k}:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}})\to
B[\theta]$. Because $i_{\\_}{n}[\theta]$ is a level with free variables among
$\Xi_{\\_}{\theta}$, we then also have $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash
i_{\\_}{n}[\theta]:{\color[rgb]{0,0.1171875,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1171875,0.62890625}\textsf{{Lvl}}}$,
for all $n=1..k$. By the typing rule for application with a confined term, we
get $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash
c~{}i_{\\_}{1}[\theta]..i_{\\_}{k}[\theta]:B[\vec{i}/\vec{j}][\theta]$.

  * •

Case Switch : Let
$\theta\vDash\mathcal{C}_{\\_}{1}\cup\mathcal{C}_{\\_}{2}\cup\mathcal{D}$. By
hypothesis we have $\Gamma\vdash_{\\_}{\mathcal{D}}B:s$ and thus
$\Gamma\vdash_{\\_}{\mathcal{D}}$, therefore by i.h. we have
$\Gamma\vdash_{\\_}{\mathcal{C}_{\\_}{1}\cup\mathcal{D}}t:A$, from which we
get $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash t[\theta]:A[\theta]$. Moreover,
from Lemma 14 we also get $A[\theta]\equiv B[\theta]$. Finally, from
$\Gamma\vdash_{\\_}{\mathcal{D}}B:s$ we have
$\Xi_{\\_}{\theta},\Gamma[\theta]\vdash B[\theta]:s$, and therefore we
conclude $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash t[\theta]:B[\theta]$ by rule
Conv.

  * •

Case Pi : Let
$\theta\vDash\mathcal{C}_{\\_}{1}\cup\mathcal{C}_{\\_}{2}\cup\mathcal{D}$. By
hypothesis we have $\Gamma\vdash_{\\_}{\mathcal{D}}$ and thus
$\Gamma\vdash_{\\_}{\mathcal{D}}\textsf{{Type}}:\textsf{{Kind}}$, therefore by
i.h. we have
$\Gamma\vdash_{\\_}{\mathcal{C}_{\\_}{1}\cup\mathcal{D}}A:\textsf{{Type}}$,
from which we get $\Xi_{\\_}{\theta},\Gamma[\theta]\vdash
A[\theta]:\textsf{{Type}}$ and
$\Gamma,x:A\vdash_{\\_}{\mathcal{C}_{\\_}{1}\cup\mathcal{D}}$. Therefore, by
i.h. once again we also have
$\Gamma\vdash_{\\_}{\mathcal{C}_{\\_}{1}\cup\mathcal{C}_{\\_}{2}\cup\mathcal{D}}B:C$
and thus $\Xi_{\\_}{\theta},\Gamma[\theta],x:A[\theta]\vdash
B[\theta]:C[\theta]$.

We now claim that $\Xi_{\\_}{\theta},\Gamma[\theta],x:A[\theta]\vdash
B[\theta]:s$. Indeed, by validity we have either $C=\textsf{{Kind}}$ or
$\Xi_{\\_}{\theta},\Gamma[\theta],x:A[\theta]\vdash C[\theta]:s^{\prime}$ for
some $s^{\prime}$. If $C[\theta]=\textsf{{Kind}}$ then we must have
$s=\textsf{{Kind}}$, and thus the claim follows from
$\Xi_{\\_}{\theta},\Gamma[\theta],x:A[\theta]\vdash B[\theta]:C[\theta]$. If
$\Xi_{\\_}{\theta},\Gamma[\theta],x:A[\theta]\vdash C[\theta]:s^{\prime}$ for
some $s^{\prime}$, then by subject reduction we have
$\Xi_{\\_}{\theta},\Gamma[\theta],x:A[\theta]\vdash s:s^{\prime}$, in which
case we must have $s=\textsf{{Type}}$ and $s^{\prime}=\textsf{{Kind}}$.
Therefore, by the conversion rule with $C[\theta]\equiv\textsf{{Type}}$ we get