# Encoding impredicative hierarchy of type universes with variables

Yoan Géran

► To cite this version:

Yoan Géran. Encoding impredicative hierarchy of type universes with variables. 2023. hal-04311936

HAL Id: hal-04311936

https://hal.science/hal-04311936v1

Preprint submitted on 28 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Encoding impredicative hierarchy of type universes with variables

Yoan Géran Ⓔ

Mines Paris - PSL, Centre de Recherche en Informatique

Université Paris-Saclay, Laboratoire Méthodes Formelles, ENS Paris-Saclay

## Abstract

Logical frameworks can be used to translate proofs from a proof system to another one. For this purpose, we should be able to encode the theory of the proof system in the logical framework. The Lambda Pi calculus modulo theory is one of these logical frameworks. Powerful theories such as pure type systems with an infinite hierarchy of universes have been encoded, leading to partial encodings of proof systems such as Coq, Matita or Agda. In order to fully represent systems such as Coq and Lean, we introduce a representation of an infinite universe hierarchy with an impredicative universe and universe variables where universe equivalence is equality, and implement it as a terminating and confluent rewrite system.

**2012 ACM Subject Classification** Theory of computation → Equational logic and rewriting; Theory of computation → Type theory

**Keywords and phrases** type theory, logical framework, rewriting theory, type universes

**Digital Object Identifier** 10.4230/LIPIcs.CVIT.2016.23

**Supplementary Material** An implementation is available at https://gitlab.crans.org/geran/dedukti-level-implementation

**Acknowledgements** I want to thank my PhD advisors Olivier Hermant and Gilles Dowek for the helpful discussions and comments.

## 1 Introduction

The formalization of mathematical theorems and the verification of softwares are done in several tools, and many logical systems and theories are developed as the research on proof-checking makes progress. Interoperability is then a big challenge which aims to avoid the redevelopment of the same proof in each system. Instead of developing translators from each system to another one, *logical frameworks* propose to define theories in a common language, which makes translation easier. Thus, the logical framework should be expressive enough and work should be done to define the wanted theories in the framework.

In this paper, our goal is to show how to define the universe levels of the theory of the Coq proof system in one of these frameworks, the λΠ-calculus modulo rewriting. Since a lot of theories are expressed as extensions of *Pure Type Systems*, the first part of this introduction will define them. Then, we will present the λΠ-calculus modulo rewriting and the type system behind Coq, in particular the universe levels.

### Pure Type Systems

A lot of theories are based on extensions of Church's simply-typed λ-calculus (STLC). In [5], Barendregt introduced the λ-cube which classifies type systems depending on the possibility to quantify on types or terms to build new types or new terms. It captures systems such as System F (with type polymorphism), λω (with type operators), λΠ (with dependent types), and the Calculus of Constructions (CC) which allows all these quantifications.

<figure><img src="image_2.png" /></figure>
## 23:2 Encoding impredicative hierarchy of type universes with variables

More generally, these constructions can be extended, leading to more powerful systems called *Pure Type Systems* [6, 8].

**Definition 1.** A Pure Type System (PTS) is defined by a set of sorts $\mathcal{S}$ (that we will also call universes), a set of axioms $\mathcal{A} \subseteq \mathcal{S}^2$ and a set of rules $\mathcal{R} \subseteq \mathcal{S}^3$.

$\mathcal{A}$ describes the sorts typing $(s_1$ has the type $s_2$ when $(s_1, s_2) \in \mathcal{A})$, and $\mathcal{R}$ describes the possible quantifications and their typing rules. The terms are the following, where $s \in \mathcal{S}$ and $x$ is an element of a countable set of variables $\mathcal{X}$.

$$t := s \mid x \mid \Pi x: t \cdot t \mid (\lambda x: t \cdot t) \mid t \; t$$

and the typing rules are given in Figure 1.

$$ (\text{EMPTY}) \quad \overline{[] \text{ WF}} \qquad (\text{DECL}) \quad \frac{\Gamma \vdash A: s \quad x \notin \Gamma}{\Gamma, x: A \text{ WF}} \qquad (\text{VAR}) \quad \frac{\Gamma \text{ WF} \quad (x: A) \in \Gamma}{\Gamma \vdash x: A} $$

$$ (\text{SORT}) \quad \overline{\vdash s_1: s_2} \quad (s_1, s_2) \in \mathcal{A} \qquad (\text{PROD}) \quad \frac{\Gamma \vdash A: s_1 \quad \Gamma, x: A \vdash B: s_2}{\Gamma \vdash \Pi x: A \cdot B: s_3} \quad (s_1, s_2, s_3) \in \mathcal{R} $$

$$ (\text{APP}) \quad \frac{\Gamma \vdash t: \Pi x: A \cdot B \quad \Gamma, \vdash u: A}{\Gamma \vdash t \; u: B[x := u]} \qquad (\text{ABS}) \quad \frac{\Gamma, x: A \vdash t: B \quad \Gamma \vdash \Pi x: A \cdot B: s}{\Gamma \vdash \lambda x \cdot t: \Pi x: A \cdot B} $$

$$ (\text{CONV}) \quad \frac{\Gamma \vdash B: s \quad \Gamma \vdash t: A \quad A \equiv_{\beta} B}{\Gamma \vdash t: B} \quad s \in \mathcal{S} $$

<caption>Figure 1 Typing rules</caption>

**Definition 2 (Functional and full PTS).** A PTS is said to be functional if $\mathcal{A}$ and $\mathcal{R}$ are functional relations from $\mathcal{S}$ and $\mathcal{S} \times \mathcal{S}$ to $\mathcal{S}$, that is to say $(s_1, s_2) \in \mathcal{A} \wedge (s_1, s_3) \in \mathcal{A} \Rightarrow s_2 = s_3$ and $(s_1, s_2, s_3) \in \mathcal{R} \wedge (s_1, s_2, s_4) \in \mathcal{R} \Rightarrow s_3 = s_4$.

A PTS is called full if $\mathcal{A}$ and $\mathcal{R}$ are total functions from $\mathcal{S}$ and $\mathcal{S} \times \mathcal{S}$ to $\mathcal{S}$.

## The $\lambda\Pi$-calculus modulo rewriting

$\lambda\Pi$, the extension of STLC with dependent types, is the language of the *Edinburgh Logical Framework* (ELF) [22]. However, computation plays an essential role in type theories, then in modern proof assistant, and $\lambda\Pi$ is not well-suited for this. To address this point, the $\lambda\Pi$-calculus modulo rewriting ($\lambda\Pi/\equiv$) [12] extends $\lambda\Pi$ by allowing user-defined higher-order rewrite rules [16, 30] that can be used to define functions but also types. Types are then identified modulo $\beta$ and these rewrite rules.

In order to have good properties such as the decidability of the type-checking, the rewrite rules introduced should preserve typing and form a confluent and strongly normalizing rewrite system, which adds some restrictions and requires more efforts to show that these properties are respected.

**Remark 3.** In the rest of this article, we will use the syntax $u \to v$ (where $u$ may contain free variables used for matching) to define a rewrite rule and the syntax $u \leftrightarrow v$ to indicate that the term $u$ rewrites to the term $v$.

The $\lambda\Pi/\equiv$ can express CC and its subtheories [10], and, in [15], Cousineau and Dowek show how to embed functional PTS (with a possibly infinite number of symbols and rules):

1. for each sort $s$, symbols $U_s$: Type and $E1_s$: $U_s \to$ Type,

2. for each axiom $(s_1, s_2)$, a symbol $u_{s_1}$: $U_{s_2}$ and a rewrite rule $E1_{s_2}(s_1) \to U_{s_1}$,
3. for each rule $(s_1, s_2, s_3)$, a symbol $\pi_{(s_1,s_2)}: (x: U_{s_1}) \to (\mathrm{El}_{s_1}(x) \to U_{s_2}) \to U_{s_3}$ and a rewrite rule $\mathrm{El}_{s_3}(\pi_{(s_1,s_2)}(A, B)) \to (x: \mathrm{El}_{s_1}(A)) \to \mathrm{El}_{s_2}(B)$.

$u_s$ corresponds to the sort $s$ as a term, $U_s$ to the sort $s$ as a type, and $\mathrm{El}_s$ associates a sort (as term) of type $s$ to its corresponding type, hence the rewrite rule added for each axiom, and $\pi_{(s_1,s_2)}AB$ is the term corresponding to the types of the function from $A$ to $B(A)$, hence the rewrite rule added to obtain the type associated to this term.

Several systems have been encoded in $\lambda\Pi/\equiv$: HOL-LIGHT [31, 2], AGDA [20], MATITA [2], but also parts of COQ, on which we will come back to later. Besides, since there exist multiple implementations of the $\lambda\Pi/\equiv$ such as DEDUKTI [3], LAMBDAPI [24], or KONTROLI [18], these embeddings have been effectively implemented leading to translations from the proofs systems to these implementations, but also to translations from these implementations of $\lambda\Pi/\equiv$ to proof assistants [31, 32].

## Coq's type system

The theory of COQ is based on CC extended with an infinite hierarchy of universes and an impredicative universe Prop. It corresponds to a slightly different version of the following PTS (where Prop is denoted as Type₀).

**Definition 4 (Impredicative max).** We define $\mathrm{imax}: \mathbb{N} \to \mathbb{N} \to \mathbb{N}$ by $\mathrm{imax}(i, 0) = 0$ and $\mathrm{imax}(i, j + 1) = \max(i, j + 1)$.

**Definition 5 (CC$^\infty$).** CC$^\infty$ is the full PTS defined with an infinite sequence of sorts Typeᵢ indexed on N, the axioms (Typeᵢ, Typeᵢ₊₁), and the rules (Typeᵢ, Typeⱼ, Typeᵢₘax(i,j)).

**Remark 6.** One can also define a predicative PTS where the products from Typeᵢ to Typeⱼ are elements of Typeᵢₘax(i,j) instead of Typeᵢₘax(i,j). This latter is the building on AGDA proof system while CC$^\infty$ is the one of COQ but also of LEAN or MATITA.

In both cases, the sorts are characterized by *levels* indexed on $\mathbb{N}$; the functions $\mathcal{R}$ and $\mathcal{A}$ can be defined in the $\lambda\Pi/\equiv$, and we can adapt the general embedding of Cousineau and Dowek to a finite embedding. For that, we define the natural numbers $N$ with the successor function $s$, $\max: N \to N \to N$, $\imax: N \to N \to N$, and

- symbols $U: N \to \mathrm{Type}$ and $\mathrm{El}: (i: N) \to U(i) \to \mathrm{Type}$,

- a symbol $u: (i: N) \to U(s(i))$ and a rewrite rule $\mathrm{El\_i} \to U i$,

- a symbol $\pi: (i: N) \to (j: N) \to (A: U i) \to (\mathrm{El\_i} A \to U j): U(\mathrm{imax\_i} j)$ and a rewrite rule $\mathrm{El\_i}(\pi\_i j A B) \to (x: \mathrm{El\_i} A) \to \mathrm{El\_i} j (B x)$.

COQ extend CC$^\infty$ with other features. Some of them have been encoded, leading to a partial translator from COQ to DEDUKTI [11, 17], and to the sharing of developements of the GeoCoq library [7], a formalization of geometry, to other proof assistants [21]. Extensions such as inductive types [13, 28] and cumulativity [27] have been widely covered: Burel and Boespflug in [11], then Férey in his thesis [17] proposes embeddings of inductive constructions and cumulativity have been studied by Assaf [1, 2], Férey [17] and Thiré [32].

In this paper, we are interested in another feature, the level variables, which permits to extend CC$^\infty$ with floating universes [25] or with universe polymorphism [29, 23, 14].

## Level variables

We extend the syntax of the levels with variables.
23:4 Encoding impredicative hierarchy of type universes with variables

118 ► **Definition 7 (Levels).** A level is a term of the grammar

119 $t := 0 \mid s(t) \mid \max(t, t) \mid \operatorname{imax}(t, t) \mid x$

120 where $x$ is an element of a countable set of variables $\mathcal{X}$. We denote by $\mathcal{L}$ the set of the levels,
121 and we say that $t$ is a concrete level if $t$ does not contain any variable.

122 ► **Definition 8 (Valuation).** A valuation is a function $\sigma: \mathcal{X} \to \mathbb{N}$.

123 ► **Definition 9.** Let $\sigma: \mathcal{X} \to \mathbb{N}$ be a valuation. We define inductively the value of a level $t$
124 over $\sigma$, denoted as $\llbracket t \rrbracket_\sigma$ with

125 $\llbracket 0 \rrbracket_\sigma = 0 \qquad \llbracket s(t) \rrbracket_\sigma = s(\llbracket t \rrbracket_\sigma)$ \\
126 $\llbracket \max(t_1, t_2) \rrbracket_\sigma = \max(\llbracket t_1 \rrbracket_\sigma, \llbracket t_2 \rrbracket_\sigma)$ \\
$\llbracket \operatorname{imax}(t_1, t_2) \rrbracket_\sigma = \operatorname{imax}(\llbracket t_1 \rrbracket_\sigma, \llbracket t_2 \rrbracket_\sigma)$

127 We use the same symbol $s$, $\max$, and $\imax$ for the syntax of the levels and the functions
128 of the natural numbers. However, levels are abstract terms and are interpreted through
129 valuations. Besides, the concrete levels can clearly be identified as the natural numbers which
130 justifies the use of the same symbol and permits to see the interpretation as a function that
131 concretizes a level, turning it into a concrete level.

132 ► **Definition 10 (Level comparison).** Let $t_1, t_2 \in \mathcal{L}$. We say that $t_1 \leq_{\mathcal{L}} t_2$ if for all valuations $\sigma$, $\llbracket t_1 \rrbracket_{\sigma} \leq \llbracket t_2 \rrbracket_{\sigma}$. In the same way, we say that $t_1 =_{\mathcal{L}} t_2$ if for all valuations $\sigma$, $\llbracket t_1 \rrbracket_{\sigma} = \llbracket t_2 \rrbracket_{\sigma}$. Hence $t_1 =_{\mathcal{L}} t_2$ if and only if $t_1 \leq_{\mathcal{L}} t_2$ and $t_2 \leq_{\mathcal{L}} t_1$.

135 With level variables, the equivalence is no more the syntactic equality and the above
136 embedding does not reflect it anymore: $\max(x, y)$ and $\max(y, x)$ are not convertible and adding
137 rules for that would lead to a non-terminating system. In the same way, commutativity and
138 equivalences such as $\max(x, x) =_{\mathcal{L}} x$ or $\max(s(x), x) =_{\mathcal{L}} s(x)$ are hard to express, and the
139 impredicativity introduces other:$\imax(x, x) =_{\mathcal{L}} x$, $\max(\imax(x, y), x) =_{\mathcal{L}} \max(x, y)$, etc.

140 And yet, a correct embedding of the levels should reflect these equivalences. For instance,
141 a term of the universe Type$_x$ is also a term of the universe Type$_{imax(x,x)}$, and then we should
142 be able to identify the universes such as Type$_x$ and Type$_{imax(x,x)}$. This paper presents a
143 new embedding that faithfully represents levels with variables.

144 **Related work**

145 Some solutions have been studied in the predicative case. The big issue is the associativity and
146 commutativity of the max symbol. In [20], Genestier solved this problem to encode AGDA's
147 universe polymorphism. For that, he used rewriting modulo associativity and commutativity
148 (AC). The idea, also mentionned in a draft of Voevodsky [33], is to represent each level
149 as $\max(n, n_1 + x_1, \dots, n_k + x_k)$ where $n \ge \max(n_1, \dots, n_k)$. Besides, if there exists $i \ne j$
150 such that $x_j = x_i$, we simplify the term and keep only $\max(n_i, n_j) + x_i$. Then, we obtain a
151 minimal representation of terms of the max-successor algebra.

152 Blanqui gives another presentation of this algebra in [9], with an encoding without
153 matching modulo AC. However, this solution requires to keep the level in some AC canonical
154 form, and can then require the modification of the $\lambda\Pi/ \equiv$ type-checker.

155 The imax-successor algebra is less studied and we do not know easy ways to reflect its
156 equalities. A confluent encoding is proposed in [4], but it does not fully reflect the equalities;
157 for instance, the levels $\max(\imax(x, y), x)$ and $\max(x, y)$ are not convertible. Besides, Férey
158 designed a non-confluent encoding of universe polymorphism in [17].
Contribution and outline

159

160

161

162

163

We introduce a new representation for the levels, using the idea presented above in the
predicative case: find a set of subterms such that any level can be expressed as a maximum
of subterms. They should be easily comparable to simplify max(u, v) into u if u ≤ v and
obtain minimal representations, and they should ensure the uniqueness property:

164

$$
\max(u_1, \dots, u_n) =_{\mathcal{L}} \max(v_1, \dots, v_m) \iff \{u_1, \dots, u_n\} = \{v_1, \dots, v_m\}.
$$

165

166

167

Intuitively, the subterms should be very basic and simple: a subterm *u* must not be equivalent to a maximum of other subterms. With this representation, we obtain a deep understanding of the imax-successor algebra, and an easy procedure-decision for the level inequality problem.

168

169

170

171

172

173

In the Section 2, we study the semantic of the imax operator and establish a suitable
set of subterms. Then, in the Section 3, we introduce the minimal representation and
show that equivalent terms have the same minimal representation. And the Section 4 is
dedicated to the implementation of this representation into the λΠ/ ≡ as a first-order
confluent and terminating rewrite system. An implementation in DEDUKTI is available on
https://gitlab.crans.org/geran/dedukti-level-implementation.

174

2 Universe representation in impredicative hierarchy

175

176

177

In this section, we study the imax operators and its interaction with max and the successor
and establish semantic equalities that permits to simplify the levels in order to find a set of
sublevels for the desired representation.

178

2.1 Levels as maximum

179

180

181

The very first step is to show that any level can be expressed as a maximum of levels that do
not contain any max, that is the principle of our idea of representation. The successor can be
distributed over max, the two next propositions show how to distribute imax over max.

182

► **Proposition 11.** For all $u, v, w \in \mathcal{L}$, $\operatorname{imax}(u, \max(v, w)) =_{\mathcal{L}} \max(\operatorname{imax}(u, v), \operatorname{imax}(u, w))$.

183

Proof. Let $\sigma$ be a valuation, $t = \operatorname{imax}(u, \max(v, w))$, $t_1 = \operatorname{imax}(u, v)$ and $t_2 = \operatorname{imax}(u, w)$.

184

■ If [[v]]<sub>σ</sub> = [[w]]<sub>σ</sub> = 0, then [[max(t<sub>1</sub>, t<sub>2</sub>)]]]<sub>σ</sub> = 0 = [[t]]<sub>σ</sub>.

185

■ If [[v]]<sub>σ</sub> ≠ 0 and [[w]]<sub>σ</sub> = 0, then [[max(t<sub>1</sub>, t<sub>2</sub>)]]]<sub>σ</sub> = max([u]]<sub>σ</sub>, [v]]<sub>σ</sub>) = [[t]]<sub>σ</sub>.

186

■ If [[v]]<sub>σ</sub> = 0 and [[w]]<sub>σ</sub> ≠ 0, then [[max(t<sub>1</sub>, t<sub>2</sub>)]]]<sub>σ</sub> = max([u]]<sub>σ</sub>, [w]]<sub>σ</sub>) = [[t]]<sub>σ</sub>.

187

■ Else, [[max(t<sub>1</sub>, t<sub>2</sub>)]]]<sub>σ</sub> = max([u]]<sub>σ</sub>, [v]]<sub>σ</sub>, [[w]]<sub>σ</sub>) = [[t]]<sub>σ</sub>.

188

<figure><img src="image_3.png" /></figure>

189

► **Proposition 12.** For all $u, v, w \in \mathcal{L}$, $\operatorname{imax}(\max(u, v), w) =_{\mathcal{L}} \max(\operatorname{imax}(u, w), \operatorname{imax}(v, w))$.

190

Proof. Let $\sigma$ be a valuation.

191

■ If [[w]]<sub>σ</sub> = 0, then [[max(imax(u, w), imax(u, w))]]<sub>σ</sub> = 0 = [[imax(max(u, v), w)]]]<sub>σ</sub>.

192

■ Else, [[max(imax(u, w), imax(v, w))]]<sub>σ</sub> = max([u]]<sub>σ</sub>, [v]]<sub>σ</sub>, [[w]]<sub>σ</sub>) = [[imax(max(u, v), w)]]]<sub>σ</sub>.

193

<figure><img src="image_4.png" /></figure>

Then, any level can then be expressed as a maximum of levels without max. Note that
for this, we consider that max takes a set of levels as argument. We obtain this theorem.

194

195

► **Theorem 13.** For all $t \in \mathcal{L}$, there exists $u_1, \dots, u_n$ in the grammar $t := 0 \mid s(t) \mid \text{imax}(t, t) \mid x$ such that $t =_{\mathcal{L}} \max(u_1, \dots, u_n)$.

196

197
## 2.2 Simplification of the levels

We can now focus on levels without maximum. The uniqueness property sought for the representation requires the subterms to be very basic, and then search to simplify the levels.

The main issue is imax: its asymmetry complicates its interaction with other symbols. The previous equalities show how to remove the interaction between imax and max, now, we will study the interactions between imax and the other symbols. The goal is to restrict the localisation of the imax symbols to specific parts of the levels in order to understand and control their influence on the levels semantic.

Firstly, we recall these equalities that are direct consequences of the semantic of imax. They permit to deal with 0 and the successor.

**Proposition 14.** For all $u, v \in \mathcal{L}$, $\text{imax}(u, 0) =_\mathcal{L} 0$ and $\text{imax}(u, s(v)) = \max(u, s(v))$.

And we show how to remove imax symbol in second argument of imax.

**Proposition 15.** For all $u, v, w \in \mathcal{L}$, $\text{imax}(u, \text{imax}(v, w)) =_\mathcal{L} \max(\text{imax}(u, w), \text{imax}(v, w))$.

**Proof.** Let $\sigma$ be a valuation.

■ If $[[w]]_\sigma = 0$, then $[[\max(\text{imax}(u, w), \text{imax}(u, w))]_\sigma = 0 = [[\text{imax}(u, \text{imax}(v, w))]_\sigma$.

■ Else, $[[\max(\text{imax}(u, w), \text{imax}(v, w))]_\sigma = \max([[u]]_\sigma, [[v]]_\sigma, [[w]]_\sigma) = [[\text{imax}(u, \text{imax}(v, w))]_\sigma]$.

Thus, we can consider that the second argument of a imax is always a variable. It is more complicated to directly enforce the form of its first argument, but we can obtain one restriction by distributing the successor over the imax. However, we cannot do it as directly as we distribute the successor over the max, as shown in the next example.

**Example 16.** We show that $s(\text{imax}(y, x)) \neq_\mathcal{L} \text{imax}(s(y), s(x))$ by considering a valuation $\sigma$ such that $\sigma(x) = 0$ and $\sigma(y) = 1$.

**Proposition 17.** For all $u, v, w \in \mathcal{L}$, $s(\text{imax}(v, w)) =_\mathcal{L} \max(s(w), \text{imax}(s(v), w))$.

**Proof.** Let $\sigma$ be a valuation.

■ If $[[w]]_\sigma = 0$, then $[[s(\text{imax}(v, w))]_\sigma = s(0) = [[\max(s(w), \text{imax}(s(v), w))]_\sigma$.

■ Else $[[s(\text{imax}(v, w))]_\sigma = s(\max([[v]]_\sigma, [[w]]_\sigma)) = [[\max(s(w), \text{imax}(s(v), w))]_\sigma]$.

Finally, all of these propositions lead to this grammar restriction.

**Theorem 18.** For all $u \in \mathcal{L}$, there exists $u_1, \dots, u_n$ in the grammar $t := s^k(x) \mid s^k(0) \mid \text{imax}(t, x)$ such that $u =_\mathcal{L} \max(u_1, \dots, u_n)$.

**Remark 19.** For all $t$ in the grammar of Theorem 18, there exists $x_1, \dots, x_n \in \mathcal{X}$, and $v = s^k(0)$ or $v = s^k(x)$ such that $t = \text{imax}(\text{imax}(\text{imax}(\dots \text{imax}(v, x_1), x_2)\dots)), x_{n-1}), x_n)$.

## 2.3 Introducing new levels

Here, we continue the simplification of the levels under max in order to find simple enough terms to reach the uniqueness property. Indeed, the terms of the grammar of Theorem 18 are still not enough.

**Example 20.** Let us consider $t = \max(\text{imax}(x, y), \text{imax}(y, x))$. Then, $t =_\mathcal{L} \max(x, y)$.
To better understand the issue, we should have a deep understanding of the semantic of $\mathrm{imax}(x, y)$. It means that we always consider the value of $y$, but we only consider the value of $x$ if $y$ is not zero: the position of the variables is essential in the levels. But, taking into account $\mathrm{imax}(y, x)$ leads to offset this, and the value of $x$ and $y$ are always considered.

Here, we come to a solution that consists of introducing new symbols that permit to represent the current levels, without taking into account the order of the variables.

**Definition 21 (Sublevels).** We define new symbols $\mathcal{A}$ and $\mathcal{B}$. $\mathcal{A}$ takes as argument a set of variables, a variable and an integer, and $\mathcal{B}$ takes as argument a set of variables and an integer. They have the following semantic.

$$ \llbracket \mathcal{A}(E, x, S) \rrbracket_{\sigma} = \begin{cases} 0 & \text{if there exists } y \in E \text{ such that } \sigma(y) = 0 \\ \llbracket x \rrbracket_{\sigma} + S & \text{else} \end{cases} $$

$$ \llbracket \mathcal{B}(E, S) \rrbracket_{\sigma} = \begin{cases} 0 & \text{if there exists } y \in E \text{ such that } \sigma(y) = 0 \\ S & \text{else} \end{cases} $$

In the next proposition, we show that any level of the grammar of Theorem 18 can be written as a maximum of terms of this new grammar.

**Proposition 22.** If $t = \mathrm{imax}(\mathrm{imax}(\mathrm{imax}(\cdots \mathrm{imax}(s^k(y), x_1)) \cdots)), x_{n-1}), x_n)$, then
$$ t = \mathcal{L} \max(\mathcal{A}(\emptyset, x_n, 0), \mathcal{A}(\{x_n\}, x_{n-1}, 0), \dots, \mathcal{A}(\{x_2, \dots, x_n\}, x_1, 0), \mathcal{A}(\{x_1, \dots, x_n\}, y, k)). $$

And if $t = \mathrm{imax}(\mathrm{imax}(\mathrm{imax}(\cdots \mathrm{imax}(s^k(0), x_1)) \cdots)), x_{n-1}), x_n)$, then
$$ t = \mathcal{L} \max(\mathcal{A}(\emptyset, x_n, 0), \mathcal{A}(\{x_n\}, x_{n-1}, 0), \dots, \mathcal{A}(\{x_2, \dots, x_n\}, x_1, 0), \mathcal{B}(\{x_1, \dots, x_n\}, k)). $$

**Proof.** We show the result for the first case. Let $\sigma$ be a valuation. If $\forall 1 \le i \le n$, $\sigma(x_i) \ne 0$, then

$$ \begin{align*} \llbracket t \rrbracket_{\sigma} &= \max(\sigma(x_n), \dots, \sigma(x_1), k + \sigma(y)) \\ \forall 1 < i \le n, \llbracket \mathcal{A}(\{x_n, \dots, x_{i+1}\}, x_i, 0) \rrbracket_{\sigma} &= \sigma(x_i) \\ \llbracket \mathcal{A}(\{x_n, \dots, x_1\}, y, k) \rrbracket_{\sigma} &= k + \sigma(y) \end{align*} $$

and else, we take the largest $1 \le i \le n$ such that $\sigma(x_i) = 0$, then

$$ \begin{align*} \llbracket t \rrbracket_{\sigma} &= \max(\sigma(x_n), \dots, \sigma(x_{i+1})) & \forall 1 < j \le i, \llbracket \mathcal{A}(\{x_n, \dots, x_{j+1}\}, x_j, 0) \rrbracket_{\sigma} &= 0 \\ \llbracket \mathcal{A}(\{x_n, \dots, x_1\}, y, k) \rrbracket_{\sigma} &= 0 & \forall i < j \le n, \llbracket \mathcal{A}(\{x_n, \dots, x_{j+1}\}, x_j, 0) \rrbracket_{\sigma} &= \sigma(x_j) \end{align*} $$

hence the equality.

And the second case is very similar. Let $\sigma$ be a valuation. If $\forall 1 \le i \le n$, $\sigma(x_i) \ne 0$, then

$$ \begin{align*} \llbracket t \rrbracket_{\sigma} &= \max(\sigma(x_n), \dots, \sigma(x_1), k) \\ \forall 1 < i \le n, \llbracket \mathcal{A}(\{x_n, \dots, x_{i+1}\}, x_i, 0) \rrbracket_{\sigma} &= \sigma(x_i) \\ \llbracket \mathcal{B}(\{x_n, \dots, x_1\}, k) \rrbracket_{\sigma} &= k \end{align*} $$

and else, we take the largest $1 \le i \le n$ such that $\sigma(x_i) = 0$, then

$$ \begin{align*} \llbracket t \rrbracket_{\sigma} &= \max(\sigma(x_n), \dots, \sigma(x_{i+1})) & \forall 1 < j \le i, \llbracket \mathcal{A}(\{x_n, \dots, x_{j+1}\}, x_j, 0) \rrbracket_{\sigma} &= 0 \\ \llbracket \mathcal{B}(\{x_n, \dots, x_1\}, k) \rrbracket_{\sigma} &= 0 & \forall i < j \le n, \llbracket \mathcal{A}(\{x_n, \dots, x_{j+1}\}, x_j, 0) \rrbracket_{\sigma} &= \sigma(x_j) \end{align*} $$

hence the equality.

<figure><img src="image_5.png" /></figure>
23:8 Encoding impredicative hierarchy of type universes with variables

The two equivalences are quite similar, the difference being in the very last subterm of the max which is a $\mathcal{A}$ in the first case (we have to take into account $s^k(y)$ that is to say $k+y$) and a $\mathcal{B}$ in the second one ($k$ is taken into account with a $\mathcal{B}$).

The sublevels that we search for our representation are elements of this grammar. We just have two slightly modifications, two simplifications to make. The first one is illustrated by this example.

**Example 23.** With $t_1 = \mathcal{A}(\emptyset, x, 0)$ and $t_2 = \mathcal{A}(\{x\}, x, 0)$, we have $t_1 =_\mathcal{L} t_2$ since for all valuation $\sigma$, $[[t_1]]_\sigma = \sigma(x) = [[t_2]]_\sigma$.

The issue here is the fact that the second argument of a $\mathcal{A}$ symbol does not necesarily appear in its first argument. This creates equalities as shown in the next proposition.

**Proposition 24.** Let $x \in \mathcal{X}$, $E \subset \mathcal{X} \setminus \{x\}$ and $S \in \mathbb{N}$. Then

$$ \mathcal{A}(E, x, S) =_\mathcal{L} \max(\mathcal{A}(E \cup \{x\}, x, S), \mathcal{B}(E, S)). $$

**Proof.** Let $\sigma$ be a valuation, $t = \mathcal{A}(E, x, S)$, $u = \mathcal{A}(E \cup \{x\}, x, S)$ and $v = \mathcal{B}(E, S)$.

■ If there exists $y \in E$ such that $\sigma(y) = 0$, then $[[t]]_\sigma = [[u]]_\sigma = [[v]]_\sigma = 0$.

■ Else, if $\sigma(x) = 0$, then $[[t]]_\sigma = S$, $[[u]]_\sigma = 0$ and $[[v]]_\sigma = S$.

■ Else, $\sigma(x) \neq 0$, and then $[[t]]_\sigma = \sigma(x) + S$, $[[u]]_\sigma = \sigma(x) + S$ and $[[v]]_\sigma = S$.

Hence the result.

Then, we will only consider elements of the form $\mathcal{A}(E, x, S)$ such that $x \in E$.

The second modification is related to the representation of 0. Indeed, for all $E \subset \mathcal{X}$, $\mathcal{B}(E, 0) =_\mathcal{L} 0$, and we should then keep at most one of them. However, since we already have $0 =_\mathcal{L} \max(\emptyset)$, we can remove all of them.

And we end up with this set of sublevels which permits to express any level of $\mathcal{L}$.

**Definition 25.** We denote by $\mathcal{L}_s$ the set of the sublevels that check the following conditions.

1. $\mathcal{A}(E, x, S) \in \mathcal{L}_s \iff x \in E$,

2. $\mathcal{B}(E, S) \in \mathcal{L}_s \iff S > 0$.

**Theorem 26.** Let $t \in \mathcal{L}$. Then there exists $u_1, \dots, u_n \in \mathcal{L}_s$ such that $t =_\mathcal{L} \max(u_1, \dots, u_n)$.

**Remark 27.** By convenience, we will note $u_i \in t$ if there exists $u_1, \dots, u_n \in \mathcal{L}_s$ such that $t =_\mathcal{L} \max(u_1, \dots, u_n)$.

3 A minimal representation

In the previous section, we find a set $\mathcal{L}_s$ and showed that any level can be represented as a maximum of elements of $\mathcal{L}_s$. The goal of this one is to show that any level has a minimal representation as maximum of elements of $\mathcal{L}_s$ and that this representation is unique. Intuitevely, the sublevels of a minimal representation should be incomparable (else one of the sublevels could be removed).

**Definition 28 (Minimal representation).** Let $t$ be a term. We say that $t$ is a minimal representation if and only if there exists $u_1, \dots, u_n \in \mathcal{L}_s$ such that

1. $t = \max(u_1, \dots, u_n)$,

2. $\forall i \neq j, u_i$ and $u_j$ are incomparable.

We denote by $\mathcal{L}_r$ the set of the minimal representations.
Of course, any level $t$ has a minimal representation. We can express $t$ as a maximum of elements of $\mathcal{L}_s$ (by Theorem 26) and we remove elements if they are comparable. The challenging part is its uniqueness. To show it, we study the core of the definition of a minimal representation: the sublevel comparison.

**▶ Theorem 29 (Sublevels comparison).** Elements of $\mathcal{L}_s$ are compared as follows.

$$ \mathcal{A}(E, x, S) \not\leq_{\mathcal{L}} \mathcal{B}(F, K) \qquad (1) $$

$$ \mathcal{B}(E, S) \leq_{\mathcal{L}} \mathcal{B}(F, K) \iff F \subset E \wedge S \leq K \qquad (2) $$

$$ \mathcal{B}(E, S) \leq_{\mathcal{L}} \mathcal{A}(F, x, K) \iff (F \subset E \wedge S \leq K + 1) \qquad (3) $$

$$ \mathcal{A}(E, x, S) \leq_{\mathcal{L}} \mathcal{A}(F, y, K) \iff F \subset E \wedge x = y \wedge S \leq K \qquad (4) $$

**Proof.** With $\sigma$ such that $\sigma(x) = K + 1$ and $\sigma(y) = 1$ if $y \neq x$, we show the first case. Indeed, $[[\mathcal{A}(E, x, S)]_\sigma = K + 1 + S > K = [[\mathcal{B}(F, K)]_\sigma]$ hence $\mathcal{A}(E, x, S) \not\leq_{\mathcal{L}} \mathcal{B}(F, K)$. The cases 2, 3 and 4 correspond to Propositions 30–32 proved below. ◀

**▶ Proposition 30.** Let $E, F \subset \mathcal{X}, x \in E, y \in F$ and $S, K \in \mathbb{N}$. Then

$$ \mathcal{A}(E, x, S) \leq_{\mathcal{L}} \mathcal{A}(F, y, K) \iff F \subset E \wedge x = y \wedge S \leq K. $$

**Proof.** We note $t_1 = \mathcal{A}(E, x, S)$ and $t_2 = \mathcal{A}(F, y, K)$. Let us suppose $F \subset E, x = y$ and $S \leq K$. Let $\sigma$ be a valuation.

■ If there exists $y \in F$ such that $\sigma(y) = 0$, then $[[t_2]]_\sigma = 0$ and since $F \subset E, [[t_1]]_\sigma = 0$.

■ Else, $[[t_1]]_\sigma \leq \sigma(x) + S \leq \sigma(x) + K = [[t_2]]_\sigma$.

In both cases, $[[t_1]]_\sigma \leq [[t_2]]_\sigma$ hence $t_1 \leq_K t_2$.

Now, we show the other implication by contraposition.

■ If there exists $z \in F$ such that $z \notin E$, we take $\sigma$ such that $\sigma(z) = 0$ and for all $j \neq z$, $\sigma(j) = 1$. We note that $z \neq x$ (since $z \notin E$ and $x \in E$) hence $\sigma(x) = 1$. Then, $[[t_1]]_\sigma = S + 1 > 0 = [[t_2]]_\sigma$.

■ If $x \neq y$ we take $\sigma$ such that $\sigma(x) = K + 2, \sigma(y) = 1$ and for all $z \neq x$ and $z \neq y, \sigma(z) = 1$. Then, $[[t_1]]_\sigma = K + S + 2 > K + 1 = [[t_2]]_\sigma$.

■ If $S > K$ we take $\sigma$ such that for all $z, \sigma(z) = 1$. Then, $[[t_1]]_\sigma = S + 1 > K + 1 = [[t_2]]_\sigma$.

**▶ Proposition 31.** Let $E, F \subset \mathcal{X}$ and $S, K \in \mathbb{N}$. Then

$$ \mathcal{B}(E, S) \leq_{\mathcal{L}} \mathcal{B}(F, K) \iff F \subset E \wedge S \leq K. $$

**Proof.** We note $t_1 = \mathcal{B}(E, S)$ and $t_2 = \mathcal{B}(F, K)$. Let us suppose $F \subset E$ and $S \leq K$. Let $\sigma$ be a valuation.

■ If there exists $y \in F$ such that $\sigma(y) = 0$, then $[[t_2]]_\sigma = 0$ and since $F \subset E, [[t_1]]_\sigma = 0$.

■ Else, $[[t_1]]_\sigma \leq K \leq S = [[t_2]]_\sigma$.

In both cases, $[[t_1]]_\sigma \leq [[t_2]]_\sigma$ hence $t_1 \leq_K t_2$.

Now, we show the other implication by contraposition.

■ If there exists $y \in F$ such that $y \notin E$, we take $\sigma$ such that $\sigma(y) = 0$ and for all $z \neq y$, $\sigma(z) = 1$. Then, $[[t_1]]_\sigma = S > 0 = [[t_2]]_\sigma$.

■ If $S < K$ we take $\sigma$ such that for all $y, \sigma(y) = 1$. Then, $[[t_2]]_\sigma = K > S = [[t_1]]_\sigma$.

**▶ Proposition 32.** Let $E, F \subset \mathcal{X}, x \in E$ and $K, S \in \mathbb{N}$. Then

$$ \mathcal{B}(E, S) \leq_{\mathcal{L}} \mathcal{A}(F, x, K) \iff (F \subset E \wedge S \leq K + 1). $$
23:10 Encoding impredicative hierarchy of type universes with variables

**Proof.** We note $t_1 = \mathcal{B}(E, S)$ and $t_2 = \mathcal{A}(F, x, K)$. Let us suppose $F \subset E$ and $S \le K + 1$. Let $\sigma$ be a valuation.

351

352

■ If there exists $y \in F$ such that $\sigma(y) = 0$, then $[[t_2]]_\sigma = 0$ and since $F \subset E$, $[[t_1]]_\sigma = 0$.

353

354

■ Else, $\sigma(x) \ge 1$ (because $x \in F$) and then $[[t_2]]_\sigma = \sigma(x) + K \ge 1 + K \ge S \ge [[t_1]]_\sigma$.
In both cases, $[[t_1]]_\sigma \le [[t_2]]_\sigma$ hence $t_1 \le t_2$.

355

356

Now, we show the other implication by contraposition. First, we note that $S > 0$.

357

■ If there exists $y \in F$ such that $y \notin E$, we take $\sigma$ such that $\sigma(y) = 0$ and for all $z \ne y$, $\sigma(z) = 1$. Then, $[[t_1]]_\sigma = K > 0 = [[t_2]]_\sigma$.

358

359

■ If $S > K + 1$ we take $\sigma$ such that for all $y$, $\sigma(y) = 1$. Then, $[[t_1]]_\sigma = S > K + 1 = [[t_1]]_\sigma$.

360

◀

As a corollary, we get that the sublevel equivalence is a syntactic equality, which is quite natural; the uniqueness property would be impossible otherwise.

361

362

**▶ Corollary 33.** Let $t_1, t_2 \in \mathcal{L}_s$. Then $t_1 =_\mathcal{L} t_2 \iff t_1 = t_2$.

363

**Proof.** We have $t_1 =_\mathcal{L} t_2 \iff t_1 \le t_2 \wedge t_2 \le t_1$, and we conclude with the Theorem 29. ◀

364

◀

And we can show the uniqueness of the minimal representation. First, we show that two equivalent minimal representations have the same $\mathcal{A}$.

365

366

**▶ Proposition 34.** Let $t_1, t_2 \in \mathcal{L}_r$ such that $t_1 =_\mathcal{L} t_2$. Then

367

$$ \mathcal{A}(E, x, S) \in t_1 \iff \mathcal{A}(E, x, S) \in t_2. $$

368

**Proof.** Let us note

369

$$ t_1 = \max(\mathcal{A}(E_0, x_0, S_0), \dots, \mathcal{A}(E_n, x_n, S_n), \mathcal{B}(G_0, T_0), \dots, \mathcal{B}(G_p, T_p)) $$

370

$$ t_2 = \max(\mathcal{A}(F_0, y_0, K_0), \dots, \mathcal{A}(F_m, y_m, K_m), \mathcal{B}(H_0, L_0), \dots, \mathcal{B}(H_q, L_q)). $$

371

372

Let $\mathcal{A}(E, x, S)$ be an sublevel of $t_1$. We consider $\sigma$ such that

$$ \sigma(y) = \begin{cases} \max(S_0, \dots, S_n, K_0, \dots, K_m, T_0, \dots, T_p, L_0, \dots, L_q) + 1 & \text{if } y = x \\ 1 & \text{if } y \in E \setminus \{x\} \\ 0 & \text{else} \end{cases} $$

373

374

We have $[[t_1]]_\sigma = [[\mathcal{A}(E, x, S)]]_\sigma = S + \sigma(x)$ and then $[[t_2]]_\sigma = S + \sigma(x)$. Then, there exists $\mathcal{A}(F, y, K)$ in $t_2$ such that $F \subset E \cup \{x\} = E$ (else $F$ contains a variable $z$ such that $\sigma(z) = 0$) and $\sigma(y) + K = \sigma(x) + S$ or there exists $\mathcal{B}(F, K)$ in $t_2$ such that $K = \sigma(x) + S$. Since $\sigma(x) > \max(S_0, \dots, S_n, K_0, \dots, K_m)$, we deduce that it is the first case and $y = x$.

375

376

377

Then, there is $(F, x, S)$ in $t_2$ with $F \subset E$ and $\sigma(y) + K = \sigma(x) + S$. If $F \subsetneq E$, then by the same reasoning, we show that there exists $\mathcal{A}(G, x, S) \in t_1$ with $G \subset F \subsetneq E$. But, by Definition 28, it is impossible to have $\mathcal{A}(E, x, S)$ and $\mathcal{A}(G, x, S)$ in $t_1$ with $G \subset E$ since they are comparable.

379

380

381

Then $E = F$ and $\mathcal{A}(E, x, S)$ is also an element of $t_2$. ◀

382

◀

And we show the same for the $\mathcal{B}$.

383

**▶ Proposition 35.** Let $t_1, t_2 \in \mathcal{L}_r$ such that $t_1 =_\mathcal{L} t_2$. Then

384

$$ \mathcal{B}(E, S) \in t_1 \iff \mathcal{B}(E, S) \in t_2. $$

385
**Proof.** Let us note

386

$$t_1 = \max(\mathcal{A}(E_0, x_0, S_0), \dots, \mathcal{A}(E_n, x_n, S_n), \mathcal{B}(G_0, T_0), \dots, \mathcal{B}(G_p, T_p))$$

387

$$t_2 = \max(\mathcal{A}(F_0, y_0, K_0), \dots, \mathcal{A}(F_m, y_m, K_m), \mathcal{B}(H_0, L_0), \dots, \mathcal{B}(H_q, L_q)).$$

388

389

390

391

We show the result by induction on $E$. Let $\mathcal{B}(E, S)$ be a sublevel of $t_1$. If $E = \emptyset$, we consider $\sigma$ the zero function. Then, $\llbracket t_1 \rrbracket_\sigma = S$, hence $\llbracket t_2 \rrbracket_\sigma = S$. Since $S > 0$, it follows that $\mathcal{B}(\emptyset, S)$ is a sublevel of $t_2$.

392

393

394

In the induction case, we consider $\sigma$ such that $\sigma(x) = 1$ if $x \in E$ and $\sigma(x) = 0$ otherwise, hence $\llbracket t_1 \rrbracket_\sigma = S$. Then, $\llbracket t_2 \rrbracket_\sigma = S$ and since $S > 0$, there exists $\mathcal{A}(F, x, K)$ in $t_2$ such that $F \subset E$ and $\sigma(x) + K = S$ or there exists $\mathcal{B}(F, S)$ in $t_2$ such that $F \subset E$ and $K = S$.

395

396

397

In the first case, we have $x \in F \subset E$, then $\sigma(x) = 1$ and $K = S - 1$. Then, by Proposition 34, $\mathcal{A}(F, x, S - 1) \in t_1$ which is impossible by Definition 28 since it would be comparable with $\mathcal{B}(E, S) \in t_1$.

398

399

Then, we have $\mathcal{B}(F, S) \in t_2$. If $F \subsetneq E$, we apply the induction hypothesis and obtain $\mathcal{B}(F, S) \in t_1$, impossible because it would be comparable with $\mathcal{B}(E, S)$.

400

Then $E = F$ and $\mathcal{B}(E, S)$ is also an element of $t_2$.

◀

401

402

We immediately obtain that equivalence of minimal representations is the syntactic equality.

403

**Proposition 36.** For all $t_1, t_2 \in \mathcal{L}_r$, $t_1 =_\mathcal{L} t_2 \iff t_1 = t_2$.

404

405

**Proof.** The reverse implication is trivial and the first one is a consequence of the Propositions 34 and 35. ◀

◀

406

407

408

And finally, we obtain the main theorem: the existence and uniqueness of a minimal representation for each level. First, we show the intuitive property that the minimal representation of a maximum of sublevels is formed with elements of these sublevels.

409

410

**Proposition 37.** For all $u_1, \dots, u_n \subset \mathcal{L}_s$, there exists a unique $\{v_1, \dots, v_m\} \subseteq \{u_1, \dots, u_n\}$ such that $\max(u_1, \dots, u_n) = \max(v_1, \dots, v_m)$ and $\max(v_1, \dots, v_m) \in \mathcal{L}_r$.

411

412

413

**Proof.** We apply the following procedure. We consider $E = \{u_1, \dots, u_n\}$. While there exists $u, v \in E$ such that $u \leq_{\mathcal{L}} v$, we remove $u$ from $E$. The Proposition 36 permits to obtain the uniqueness of this minimal representation. ◀

◀

414

415

416

**Theorem 38 (Representation).** For all $t \in \mathcal{L}$, there exists a unique $\{u_1, \dots, u_n\} \subset \mathcal{L}_s$ such that $t =_\mathcal{L} \max(u_1, \dots, u_n)$. We say that $\max(u_1, \dots, u_n)$ is the minimal representation of $t$ and we denote it as $\text{repr}(t)$.

417

418

**Proof.** By Theorem 26, there exists $u_1, \dots, u_n \in \mathcal{L}_s$ such that $t =_\mathcal{L} \max(u_1, \dots, u_n)$, and by Proposition 37, there exists a unique minimal representation of $\max(u_1, \dots, u_n)$. ◀

◀

419

420

421

Having a unique minimal representation is useful to have a faithful embedding of $\mathcal{L}$ in the $\lambda\Pi/\equiv$, which is done in Section 4. Moreover, this representation also gives us an easy way to compare two terms. Indeed, a sublevel can be compared to a level using the representation.

422

423

**Lemma 39.** Let $u, v_1, \dots, v_n \in \mathcal{L}_s$. Then $u \leq_{\mathcal{L}} \max(v_1, \dots, v_n)$ if and only if there exists $i$ such that $u \leq_{\mathcal{L}} v_i$.

424

425

**Proof.** The reverse implication is trivial. We show the direct implication by contraposition. We suppose that for all $i$, $u \not\leq_{\mathcal{L}} v_i$.

426

427

If $u = \mathcal{B}(E, S)$, we consider $\sigma$ such that $\sigma(x) = 1$ if $x \in E$ and 0 otherwise. Then, for all $v_i$, we have either
23:12 Encoding impredicative hierarchy of type universes with variables

$$
428 \quad \text{or } v_i = \mathcal{A}(F, x, K) \text{ with } F \subseteq E \text{ and } K < S - 1 \text{ hence } [v_i]_{\sigma} = K + 1 < S = [u]_{\sigma},
$$

$$
429 \quad \text{or } v_i = \mathcal{A}(F, x, K) \text{ with } F \subseteq E \text{ and } K < S - 1 \text{ hence } [v_i]_{\sigma} = K + 1 < S = [u]_{\sigma},
$$

$$
430 \quad \text{or } v_i = \mathcal{B}(F, K) \text{ with } K < S - 1 \text{ hence } [v_i]_{\sigma} = K < S = [t]_{\sigma}.
$$

$$
431 \quad \text{Then } u \not\le_{\mathcal{L}} \max(v_1, \dots, v_n).
$$

432 If $u = \mathcal{A}(E, x, S)$, then, each $v_i$ is of the form $\mathcal{A}(F_i, x_i, K_i)$ or $\mathcal{B}(F_i, K_i)$, we consider $M$
433 the maximum of these $K_i$ and $\sigma$ such that $\sigma(x) = M + 2$, $\sigma(y) = 1$ if $y \in E \setminus \{x\}$ and $0$
434 otherwise. Then, for all $v_i$, we have either

$$
435 \quad v_i = \mathcal{B}(F, K) \text{ hence } [v_i]_{\sigma} \le K < S + M + 2 = [u]_{\sigma},
$$

$$
436 \quad \text{or } v_i = \mathcal{A}(F, y, K) \text{ and } F \not\subset E \text{ hence } [v_i]_{\sigma} = 0 < S = [u]_{\sigma},
$$

$$
437 \quad \text{or } v_i = \mathcal{A}(F, y, K) \text{ with } F \subseteq E \text{ and } x \neq y, \text{ hence } [v_i]_{\sigma} = K + 1 < S + M + 2 = [u]_{\sigma},
$$

$$
438 \quad \text{or } v_i = \mathcal{A}(F, x, K) \text{ with } F \subseteq E \text{ and } K < S, \text{ hence } [v_i]_{\sigma} = K + M + 2 < S + M + 2 = [u]_{\sigma}.
$$

$$
439 \quad \text{Then } u \not\le_{\mathcal{L}} \max(v_1, \dots, v_n).
$$

<figure><img src="image_6.png" /></figure>

440 And we use this lemma to compare two levels, for instance by comparing each sublevel
441 of the minimal representation of the first one to the second one. More generally, two
442 representations are compared in the following way.

443 ▶ Theorem 40. Let $u_1, \dots, u_n, v_1, \dots, v_m \in \mathcal{L}_s$. Then, $\max(u_1, \dots, u_n) \leq_{\mathcal{L}} \max(v_1, \dots, v_m)$
444 if and only if for all $i$, there exists $j$ such that $u_i \leq_{\mathcal{L}} v_j$.

445 Proof. If $\max(u_1, \dots, u_n) \leq_{\mathcal{L}} \max(v_1, \dots, v_n)$, then for all $i$, $u_i \leq_{\mathcal{L}} \max(v_1, \dots, v_n)$ and by
446 the Lemma 39, there exists $v_j$ such that $u_i \leq_{\mathcal{L}} v_j$. The reverse implication is trivial. $\quad$
447

<figure><img src="image_7.png" /></figure>

One can note that the Lemma 39 gives us a new proof of the uniqueness property stated
in Proposition 36.

449 **Proof.** Let $u = \max(u_1, \dots, u_n)$ and $v = \max(v_1, \dots, v_m)$ be two minimal representations
450 such that $u =_\mathcal{L} v$. We want to show that for all $i$, there exists $j$ such that $u_i = v_j$.

We have $u_i \le \mathcal{L} u \le \mathcal{L} v$, hence by Lemma 39, there exists $v_j$ such that $u_i \le \mathcal{L} v_j$. In
the same way, there exists $u_k$ such that $v_j \le \mathcal{L} u_k$. Then, by Definition 28, $i = k$ (because
$u_1, \dots, u_n$ are incomparable), and then $u_i = \mathcal{L} v_j$ hence $u_i = v_j$ by Corollary 33. $\quad$

This shows that there is a link between the Lemma 39 and the uniqueness property. In
fact, this lemma should be understood as an *independence* lemma. Indeed, if we consider
max($u_1, \dots, u_n$) as a linear combination of $u_1, \dots, u_n$, then this lemma states that the only
way to be smaller than a linear combination is to depend on and be smaller than one of the
elements of this combination.

This analogy provides a new point of view on our work: $\mathcal{L}_s$ is a ‘linearly independent’
family (uniqueness of the minimal representation) which generates at least $\mathcal{L}$ (for instance,
max($\mathcal{A}(\{x\}, y, 0)$) or max($\mathcal{B}(\{x\}, 1)$) are not equivalent to any level).

4 A rewriting system for this universe representation

This section is dedicated to the implementation of this representation in the $\lambda\Pi/\equiv$.

**4.1 Basic tools**

Here, we define the very basic term that we will used. The booleans and the natural numbers,
to begin with, are necessary.
**Definition 41 (Booleans).** We define a type B, with constructors true: B, false: B and functions and: B → B, or: B → B and not: B → B. B is interpreted as the Booleans, true, false, and, or and not as ⊤, ⊥, the conjunction, the disjunction and the negation.

**Definition 42 (Natural numbers).** We define a type N, with constructors 0: N, s: N → N and functions +: N → N → N, <=N: N → N → B, =N: N → N → B, <N: N → N → B (with infix notation) and maxN: N → N → N. N is interpreted as N, 0 as 0, s, +, <=N, =N and maxN as 0, s, +, <=, = and max.

Moreover, we define a *if-then-else* structure. It is not really necessary, but will be very convenient to facilitate the writing of some rules.

**Definition 43.** Let $T$ be a type. We define the function $ite_T: B \to T \to T \to T$ such that
$\forall u, v \in T$, $ite_T \text{ true } u \ v \leftrightarrow u$ and $ite_T \text{ false } u \ v \leftrightarrow v$. For convenience reasons, we will denote $ite_T b u v$ by if $b$ then $u$ else $v$.

And finally, we show how to define a type of sets for all ordered types. It will be used for set of natural numbers (to define the sublevels), but also for set of sublevels (to define the representations).

**Definition 44 (Sets).** Let $T$ be a type equipped with a total order function $leq_T: T \to T \to B$. Then, we define a type $S[T]$ corresponding to the finite set of elements of $T$ with a constructor $\{\}_T: S[T]$ and the functions (all with infix notation) $\llcorner_T: S[T] \to T \to S[T]$, $++_T: S[T] \to S[T] \to S[T]$, $in_T: T \to S[T] \to B$, $sub_T: S[T] \to S[T] \to B$ and $=_{S[T]}: S[T] \to S[T] \to B$.

$S[T]$ is interpreted as the set of finite subsets of $T$, $\{\}_T$ as the empty set, $\llcorner_T$ as the function that adds an element to a set, $++_T$, $in_T$, $sub_T$ and $=_{S[T]}$ as $\cup, \in, \subseteq$ and $=$.

For convenience reasons, we will denote the term $\{\}_T \llcorner_T x_1 \llcorner_T \cdots \llcorner_T x_n$ by $\{x_1, \dots, x_n\}_T$. In particular, $\{x\}_T$ will represent a singleton.

$S[T]$ is implemented as a sorted list of elements of $T$ with the constructors $\{\}_T: S[T]$ and $::T: T \to S[T] \to S[T]$, and the function $\llcorner_T$ adds an element to a list while keeping the uniqueness and order properties. Then, a set will be built through $\{\}_T$ and $\llcorner_T$ and the constructor $::T$ will only be used in patterns of rewrite rules.

**Definition 45 (Set order).** Let $T$ be a type with a total order function $leq_T$. Then, we define a total order $leq_{s[T]}$ by considering the lexicographic order on sorted word of $T$. Besides, we define the corresponding strict total order $lq_{s[T]}$.

We do not give the rules for these elements since they are quite basic. However, the DEDUKTI implementation is available if necessary.

## 4.2 Level encoding

In order to implement the sets of sublevels and to compare two sublevels, we should be able to compare and sort level variables. That is why we use a deep encoding where each variable is encoded as a natural number. We denote by $\gamma: \mathcal{X} \to \mathbb{N}$ a bijection that associates each variable to a natural number.

**Definition 46.** We define $L$, the type of the levels together with the constructors $O_L: L$, $S_L: L \to L$, $\max_L: L \to L \to L$, $\imax_L: L \to L \to L$ and $\text{var}_L: N \to L$. We define inductively a translation function $|\cdot|: \mathcal{L} \to L$ with

$$ 
\begin{align*}
|0| &= O_L & |s(t)| &= s_L |t| & |x| &= \text{var}_L |\gamma(x)|_N \\
|\max(u, v)| &= \max_L |u| |v| & |\imax(u, v)| &= \imax_L |u| |v|
\end{align*}
$$
23:14 Encoding impredicative hierarchy of type universes with variables

510 ▶ Definition 47. We define L<sub>S</sub>, the type of the sublevels, with the constructors a : S [N] →
511 N → N → L<sub>S</sub> and b : S [N] → N → L<sub>S</sub>. We define a translation function |·|<sub>s</sub> : L<sub>s</sub> → L<sub>S</sub> by
512 |A(E, x, S)|<sub>s</sub> = a |E| |x| |S| and |B(E, S)|<sub>s</sub> = b |E| |S|.

513 In order to define S[L<sub>S</sub>], we need a total order on L<sub>S</sub>. We consider the order where all the
514 a are before the b, and the a (respectively) the b are sorted according to the lexicographic
515 order:

516 $\quad \text{a } E \ x \ S \leq \text{b } F \ K,$

517 $\quad \text{a } E \ x \ S \leq \text{a } |F| \ |y| \ |K|$ is the lexicographic order between $(E, x, S)$ and $(F, y, K)$ (which
518 is a total order since $\mathbb{N}$ and $\mathcal{S}[\mathbb{N}]$ are equipped with a total order by Definition 45),

519 $\quad \text{b } E \ S \leq \text{b } F \ K$ is the lexicographic order between $(E, S)$ and $(F, K)$.

520 ▶ Definition 48 (Total order on sublevels). We define a total leq<sub>L<sub>S</sub></sub> on L<sub>S</sub> (and its corresponding strict order lq<sub>L<sub>S</sub></sub>). Indeed, we consider these rewrite rules.

$$
\begin{align*}
& (a \ E \ x \ S) \ \mathbf{leq}_{\mathcal{L}_S} \ (b \ F \ K) \longrightarrow \mathbf{true} \\
& (a \ E \ x \ S) \ \mathbf{leq}_{\mathcal{L}_S} \ (a \ F \ y \ K) \longrightarrow \mathbf{or} \ (E \ \mathbf{leq}_{\mathcal{L}_S} \ F) \\
& \qquad \qquad \qquad \text{and } (E =_{\mathcal{S}[N]} F) \left( (\mathbf{or} \ (x <_{N} y) \ (\mathbf{and} \ (x =_{N} y) \ (S \leq_{N} K))) \right) \\
& b \ E \ S \ \mathbf{leq}_{\mathcal{L}_S} \ b \ F \ K \longrightarrow \mathbf{or} \ (E \ \mathbf{leq}_{\mathcal{L}_S} \ F, \text{ and } (E =_{\mathcal{S}[N]} F, \ S \leq_{N} K))
\end{align*}
$$

526 And we can then define the representations.

527 ▶ Definition 49. We define a function $\max_{L_S} : S[L_S] \to L$ that embeds a set of $L_S$ into a $L$ and a
528 translation function $|\cdot|_r : \mathcal{L}_r \to L$ defined by $|\max(u_1, \dots, u_n)|_r = \max_{L_S}(\{|u_1|_S, \dots, |u_n|_S\}_T)$.

529 Now, we have defined all the types and the elements of $\mathcal{L}_r$ have translations in $\lambda\Pi/\equiv$.
530 The next step is to provide rewrite rules that transform a level into its minimal representation.
531 The cases of $0_L$ and of variables are easy.

$$
532 \qquad 0_L \rightarrow \max_{L_S}(\{\iota_{L_S}\}) \qquad \mathrm{var}_L(x) \rightarrow \max_{L_S}(\{\mathrm{a}(\{x\}_{\mathrm{N}}, x, 0)\}_{L_S})
$$

533 For the other cases, and in particular for the max, the sublevel comparison will be useful,
534 so we define it.

535 ▶ Definition 50 (Sublevels comparison). We define $<=_{L_S} : L_S \to L_S \to B$ interpreted as $\leq_L$
536 with these rewrite rules.

537 $a(E, x, S) <=_{L_S} b(F, K) \rightarrow false$ (1)

538 $b(E, S) <=_{L_S} b(F, K) \rightarrow \text{and}(F \ \text{sub}_N E, S <=_N K)$ (2)

539 $b(E, s_L(S)) <=_{L_S} a(F, y, K) \rightarrow \text{and}(F \ \text{sub}_N E, S <=_N K + 1)$ (3)

540 $a(E, x, S) <=_{L_S} a(F, y, K) \rightarrow \text{and}(F \ \text{sub}_N E, \text{ and } (x =_N y, S <=_N K))$ (4)

541 ▶ Proposition 51. Let $u, v \in \mathcal{L}_s$. Then, $u \leq_{\mathcal{L}} v \iff |u| \leq_{\mathcal{L}_s} |v| \mapsto^* true$.

542 Proof. Each rule (i) corresponds to the case *i* of the Theorem 29.

543 And now, we can give the rules to normalize the other levels.
## 4.3 The successor

We show how to compute the minimal representation of $s(\max(u_1, \dots, u_n))$.

**Definition 52.** We define $s_s$ on the sublevels by $s_s(A(E, x, S)) = A(E, x, S + 1)$ and $s_s(B(E, S)) = B(E, S + 1)$. Then $s_s(u) =_L s(u)$.

**Proposition 53.** $\mathrm{repr}(s(\max(\emptyset))) = \max(B(\emptyset), s(0))$ and for all $n > 0$ and $t = \max(u_1, \dots, u_n) \in \mathcal{L}_r$, $\mathrm{repr}(s(t)) = \max(s_s(u_1), \dots, s_s(u_n))$.

We create a function $s_{L_s}: S[L_s] \to S[L_s]$ corresponding to $s_s$.

$$s_{L_s}(\{\}_L) \to \{\}_L \qquad s_{L_s}(b(E, S)\because_L q) \to s_{L_s}(q) \prec_L b(E, s(S))$$

$$s_{L_s}(a(E, x, S)\because_L q) \to s_{L_s}(q) \prec_L a(E, x, s(S))$$

And we compute the minimal representation of a successor according to Proposition 53.

$$s_L(\max_{L_s}(\{\}_L)) \to \max_{L_s}(b(\{\}_L, s(0))) \qquad s_L(\max_{L_s}(u\because_L q)) \to \max_{L_s}(s_{L_s}(u\because_L q))$$

**Proposition 54.** For all $t \in \mathcal{L}_r$, $s_L(|t|_r) \leftrightarrow^* |\mathrm{repr}(s(t))|_r$.

## 4.4 The maximum

For the maximum, we define $\max_s$, that adds a sublevel to a minimal representation.

**Definition 55.** We define inductively $\max_s: \mathcal{P}(\mathcal{L}_s) \times \mathcal{L}_s \to \mathcal{P}(\mathcal{L}_s)$ inductively defined by $\max_s(\emptyset, u) = \{u\}$ and

$$\max_s(\{u_1, \dots, u_n\} \cup \{u\}, v) = \begin{cases} \{u_1, \dots, u_n, u\} & \text{if } v \le_L u, \\ \{u_1, \dots, u_n, v\} & \text{if } u \le_L v, \\ \max_s(\{u_1, \dots, u_n\}, v) \cup \{u\} & \text{else.} \end{cases}$$

**Proposition 56.** For all minimal representations $t = \max(u_1, \dots, u_n) \in \mathcal{L}_r$ and $v \in \mathcal{L}_s$, $\mathrm{repr}(\max(u_1, \dots, u_n, v)) = \max_s(\{u_1, \dots, u_n\}, v)$.

We implement $\max_s$ as a function $\mathrm{maxhelper}: S[L_s] \to L_s \to S[L_s]$ with these rewrite rules.

$$\mathrm{maxhelper}(\{\}_L, u) \to \{u\}_L$$

$$\mathrm{maxhelper}(u\because_L E, v) \to \begin{cases} v \le_L u & \text{if } v \le_L u \text{ then } E \prec_L u \\ v \ge_L u & \text{else} \end{cases}$$

$$\mathrm{maxhelper}(E, v) \to \begin{cases} v \le_L u & \text{if } v \le_L u \text{ then } E \prec_L v \\ v \ge_L u & \text{else} \end{cases}$$

And we compute the minimal representation for $\max_L$ according to Proposition 56.

$$\max_L(\max_{L_s}(E), \max_{L_s}(\{\}_L)) \to \max_{L_s}(E)$$

$$\max_L(\max_{L_s}(E), \max_{L_s}(u\because_L F)) \to \max_L(\mathrm{maxhelper}(E, u), \max_{L_s}(F))$$

**Proposition 57.** For all $t_1, t_2 \in \mathcal{L}_r$, $\max_L(|t_1|_r, |t_2|_r) \leftrightarrow^* |\mathrm{repr}(\max(t_1, t_2))|_r$.

## 4.5 The impredicative maximum

To begin, we study $\mathrm{imax}(u, v)$ where $u, v \in \mathcal{L}_s$.

**Proposition 58.** Let $f(E, S)$ be either $A(E, x, S)$ or $B(E, S)$ and $g(F, K)$ be either $A(F, x, K)$ or $B(F, K)$. Then

$$\mathrm{imax}(f(E, S), g(F, K)) =_L \max(f(E \cup F, S), g(F, K)).$$
23:16 Encoding impredicative hierarchy of type universes with variables

Proof. We note $u = f(E, x, S)$ and $v = g(F, K)$. Let $\sigma$ be a valuation.

■ If there exists $y \in F$ such that $\sigma(y) = 0$, then $\llbracket \mathrm{imax}(u, v) \rrbracket_\sigma = 0 = \llbracket \max(f(E \cup F, S), v) \rrbracket_\sigma$.

■ Else, $\llbracket v \rrbracket_\sigma = K > 0$ and then $\llbracket \mathrm{imax}(u, v) \rrbracket_\sigma = \max(\llbracket u \rrbracket_\sigma, K)$. Besides, since $\sigma(y) \neq 0$ for all $y \in F$, there exists $y \in E \cup F$ such that $\sigma(y) = 0$ if and only if there exists $y \in E$ such that $\sigma(y) = 0$, hence $\llbracket u \rrbracket_\sigma = \llbracket f(E \cup F, S) \rrbracket_\sigma$.

Hence the result.

◀

We implement it as a function $\mathrm{imax}_{L_S}: L_S \to L_S \to L$.

$\mathrm{imax}_{L_S}(a(E, x, S), b(F, K)) \to \max_L(\max_{L_S}(a(E \to_n F, x, S)), \max_{L_S}(b(F, K)))$

$\mathrm{imax}_{L_S}(b(E, S), b(F, K)) \to \max_L(\max_{L_S}(b(E \to_n F, S)), \max_{L_S}(b(F, K)))$

$\mathrm{imax}_{L_S}(b(E, S), a(F, x, K)) \to \max_L(\max_{L_S}(b(E \to_n F, S)), \max_{L_S}(a(F, x, K)))$

$\mathrm{imax}_{L_S}(a(E, x, S), a(F, y, K)) \to \max_L(\max_{L_S}(a(E \to_n F, x, S)), \max_{L_S}(a(F, y, K)))$

Then, following the equalities $\mathrm{imax}(0, t) =_\mathcal{L} t$ and $\mathrm{imax}(t, 0) =_\mathcal{L} 0$, and Propositions 11 and 12, we define $\mathrm{imax}_\mathrm{aux}: L_S \to L \to L$ and add these rewrite rules.

$\mathrm{imax}_L(\max_{L_S}(\{\}_L_S), t) \to t$

$\mathrm{imax}_L(\max_{L_S}(u::_{L_S} q), t) \to \max_L(\mathrm{imax}_\mathrm{aux}(u, t), \mathrm{imax}_L(q, t))$

$\mathrm{imax}_\mathrm{aux}(u, \max_{L_S}(\{\}_L_S)) \to \max_{L_S}(\{\}_L_S)$

$\mathrm{imax}_\mathrm{aux}(u, \max_{L_S}(v::_{L_S} q)) \to \max_L(\mathrm{imax}_{L_S}(u, v), \mathrm{imax}_\mathrm{aux}(u, q))$

► Proposition 59. For all $t_1, t_2 \in \mathcal{L}_r$, $\mathrm{imax}_L(|t_1|_r, |t_2|_r) \hookrightarrow^* |\mathrm{repr}(\mathrm{imax}(t_1, t_2))|_r$.

Proof. By Propositions 57 and 58, for all $u, v \in \mathcal{L}_s$, $\mathrm{imax}_{L_S}(|u|_s, |v|_s) \to^* |\mathrm{repr}(\mathrm{imax}(u, v))|$. Then, by induction on $t \in \mathcal{L}_r$ and using Proposition 57, we show that $\forall u \in \mathcal{L}_s$, $\mathrm{imax}_\mathrm{aux}(|u|_s, |t|_r) \hookrightarrow^* |\mathrm{repr}(\mathrm{imax}(u, t))|_r$. And finally, we show the result by induction on $t_2$ using Propositions 11 and 12 and the equivalences $\mathrm{imax}(0, t) =_\mathcal{L} t$ and $\mathrm{imax}(t, 0) =_\mathcal{L} 0$. ◀

4.6 Implementing the substitution

Since we use a deep encoding, $\beta$-reduction cannot be used for substitution. Then, we implement a substitution function. First, we implement $\mathrm{eval}_{L_S}: L_S \to N \to N \to L$ for the sublevels following the semantic given in the Definition 21.

$\mathrm{eval}_{L_S}(b(E, S), y, n) \to \begin{cases} \text{if and } (y \text{ in}_N E, n =_N 0) & \text{then } \max_{L_S}(\{\}_L_S) \\ \text{else} & \end{cases}$

$\max_{L_S}(b(E \setminus N y, S))$

$\mathrm{eval}_{L_S}(a(E, x, S), y, n) \to \begin{cases} \text{if and } (y \text{ in}_N E, n =_N 0) & \text{then } \max_{L_S}(\{\}_L_S) \\ \text{else} & \end{cases}$

$\max_{L_S}(b(\{\}_N, S + n))$

$\max_{L_S}(a(E \setminus N y, x, S))$

Then, we create a function $\mathrm{eval}_L: L \to N \to N \to L$ that evaluate a level using the fact that $[\max(u_1, \dots, u_n)]\{x \mapsto n\} = \max([u_1]\{x \mapsto n\}, \dots, [u_n]\{x \mapsto n\})$.

$\mathrm{eval}_L(\{\}_L_S, y, n) \to \{\}_L_S \qquad \mathrm{eval}_L(u::_{L_S} q, y, n) \to \max_L(\mathrm{eval}_{L_S}(u, y, n), \mathrm{eval}_L(q, y, n))$

► Proposition 60. Let $t \in \mathcal{L}$. Then, the normal form of $||t|\{x \mapsto u\}|$ is $\mathrm{eval}_L(|t|, |u|)$.
## 4.7 Properties of the rewrite system

The rewrite system that we designed have strong properties. First, one can note that it is does not use any higher-order rewrite rule, hence it can be implemented in a first order system.

**▶ Theorem 61.** *The rewrite system is confluent and strongly normalizing.*

*Proof.* The termination has been proved with two termination checkers, $T_1T_2$ [26] and SizeChangeTool [19], and the confluence with CSI [34].

And of course, we show that it is sound relatively to the minimal representation.

**▶ Theorem 62 (Soundness).** Let $t \in \mathcal{L}$. Then, the normal form of $|t|$ is $|\text{repr}(t)|_r$.

*Proof.* We show that $t \to^* |\text{repr}(t)|_r$ by induction on $t$: $\text{var}_L(x) \to \max_{L_S}(\{a(x)\}_{N}, 0, x)\}_{L_S}$, $0 \to \max_{L_S}\{\}_{L_S}$, and we show the cases $s$, $\max$ and $\imax$ using Propositions 54, 57, and 59. Since no rewrite rule can be applied to $\max_{L_S}$, the normal form of $|t|$ is $|\text{repr}(t)|_r$.

Theorems 38 and 62 give us that the translations of two equivalent levels are convertible, and even more, they have the same normal form. In other words, this embedding faithfully represent the level equivalences.

Besides, one could note some drawbacks of this embedding. First, we do not have a back translation from $\lambda\Pi/ \equiv$ to $L$. There are two main reason for this.

1. a and b are not exact translations of $\mathcal{A}$ and $\mathcal{B}$.

2. $\mathcal{L}_r$ and $\mathcal{L}$ are not equivalent.

The first reason is linked to the restrictions that we added to $\mathcal{A}$ and $\mathcal{B}$. Here, it is possible to write terms $b E 0$ or $a E x k$ where $x$ is not an element of $E$. In the same way, it is possible to write $\max_{L_S} L$ while two sublevels of $L$ are comparable.

A solution could be to add a dependent term as argument, to check these conditions. For instance, a would have the type $(E: S[N]) \to (x: N) \to \text{Prf}(x \text{ in}_N E) \to N \to L_S$ where $\text{Prf}: B \to \text{Type}$ represents the proof of a proposition. We declare $I: \text{Prf true}$ and we use $a E x k I$ using the fact that $x \text{ in}_N E$ reduces to true if and only if $x$ is an element of $E$.

The second reason is not related to the embedding, but to the representation that we introduced. Indeed, we already noted that some minimal representations are not equivalent to any level $(\max(\mathcal{A}(\{x\}, y, 0)) \text{ or } \max(\mathcal{B}(\{x\}, 1)) \text{ as examples}). Then, it could be a good idea to find a characterization of the elements of $\mathcal{L}_r$ that actually correspond to levels.

# 5 Conclusion

We introduced a new representation of the levels of the impredicative PTS where equivalent levels have the same representation. It provides us an easy procedure decision for the inequality problem in the imax-successor algebra, and it permits us to get a sound encoding of these levels in the $\lambda\Pi/ \equiv$, in the sense that equivalent levels have convertible translations. Moreover, this encoding corresponds to a first-order, confluent and strongly normalizing rewrite system, and in particular it permits to decide level equality.

This encoding of the levels permits to encode $\mathbb{C}\mathbb{C}^\infty$ with universe polymorphism. Besides, we still have to study how this encoding behaves well together with encodings of inductive types or cumulativity in order to get a better encoding of COQ. The ideas mentioned at the end of Section 4 are also interesting. In particular, the characterization of the elements of $\mathcal{L}_r$ that are actually levels would lead to a better understanding of the imax-successor grammar.
23:18 Encoding impredicative hierarchy of type universes with variables

Finally, this idea of representation, with the linear algebra analogy, could certainly be
adapted to some sets of terms built over a maximum, a supremum or other similar operations.
In addition to providing decision procedures, it would permit to define a concept similar
to the basis of a vector space on these spaces on these sets, and then it seems to be an
interesting direction to explore.

References

1 Ali Assaf. A calculus of constructions with explicit subtyping. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, *20th International Conference on Types for Proofs and Programs (TYPES 2014)*, volume 39 of *LIPICS*, Institut Henri Poincaré, Paris, France, May 2014. URL: https://hal.archives-ouvertes.fr/hal-01097401.

2 Ali Assaf. *A framework for defining computational higher-order logics*. Theses, École polytechnique, 09 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303.

3 Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti : a logical framework based on the $\lambda\pi$-calculus modulo theory. 2016.

4 Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu. Encoding Proofs in Dedukti: the case of Coq proofs. In *Proceedings Hammers for Type Theories*, Proc. Higher-Order rewriting Workshop, Coimbra, Portugal, July 2016. Easy Chair. URL: https://inria.hal.science/hal-01330980.

5 Henk Barendregt. Introduction to generalized type systems. *Journal of Functional Programming*, 1(2):125–154, 1991. doi:10.1017/S0956796800020025.

6 Henk Barendregt, S. Abramsky, D. Gabbay, T. Maibaum, and Henk (Hendrik) Barendregt. Lambda calculi with types. 10 2000.

7 Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, and Julien Narboux. GeoCoq, June 2018. URL: https://inria.hal.science/hal-01912024.

8 Stefano Berardi. *Type dependence and constructive mathematics*. PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990.

9 Frédéric Blanqui. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In Amy P. Felty, editor, *7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)*, volume 228 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 24:1–24:14, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2022/16305, doi:10.4230/LIPIcs.FSCD.2022.24.

10 Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In Naoki Kobayashi, editor, *6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)*, volume 195 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 20:1–20:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2021/14258, doi:10.4230/LIPIcs.FSCD.2021.20.

11 Mathieu Boespflug and Guillaume Burel. Coqine: Translating the calculus of inductive constructions into the $\lambda\pi$-calculus modulo. In *in "Second International Workshop on Proof Exchange for Theorem Proving", 2012*.

12 Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. The $\lambda\Pi$-calculus Modulo as a Universal Proof Language. *CEUR Workshop Proceedings*, 878, 06 2012.

13 Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, *COLOG-88*, pages 50–66, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg.

14 Judicaël Courant. Explicit universes for the calculus of constructions. In Victor A. Carreño, César A. Muñoz, and Sofiène Tahar, editors, *Theorem Proving in Higher Order Logics*, pages 115–130, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.
705

706

15 Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. pages 102–117, 06 2007. doi:10.1007/978-3-540-73228-0_9.

707

708

709

16 Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, *Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics*, pages 243–320. Elsevier and MIT Press, 1990. doi:10.1016/b978-0-444-88074-1.50011-1.

710

711

712

713

17 Gaspard Férey. *Higher-Order Confluence and Universe Embedding in the Logical Framework*. (*Confluence d'ordre supérieur et encodage d'univers dans le Logical Framework*. PhD thesis, École normale supérieure Paris-Saclay, France, 2021. URL: https://lmf.cnrs.fr/downloads/Perso/Ferey-thesis.pdf.

714

715

18 Michael Färber. Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. pages 225–238, 01 2022. doi:10.1145/3497775.3503683.

716

717

718

719

720

19 Guillaume Genestier. SizeChangeTool: A Termination Checker for Rewriting Dependent Types. In Mauricio Ayala-Rincón, Silvia Ghilezan, and Jakob Grue Simonsen, editors, *HOR 2019 - 10th International Workshop on Higher-Order Rewriting*, Joint Proceedings of HOR 2019 and IWC 2019, pages 14–19, Dortmund, Germany, June 2019. URL: https://hal.science/hal-02442465.

721

722

723

724

725

20 Guillaume Genestier. Encoding Agda Programs Using Rewriting. In Zena M. Ariola, editor, *5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)*, volume 167 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 31:1–31:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2020/12353, doi:10.4230/LIPIcs.FSCD.2020.31.

726

21 Yoan Géran. Stt∀ geocoq, 2021. URL: https://github.com/Karnaj/sttfa_geocoq_euclid.

727

728

22 Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. *J. ACM*, 40(1):143–184, 1 1993. doi:10.1145/138027.138060.

729

730

731

23 Robert Harper and Robert Pollack. Type checking with universes. In *2nd International Joint Conference on Theory and Practice of Software Development, TAPSOFT '89*, page 107–136, NLD, 1991. Elsevier Science Publishers B. V.

732

733

734

735

736

737

24 Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In Zena M. Ariola, editor, *5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)*, volume 167 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 35:1–35:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2020/12357, doi:10.4230/LIPIcs.FSCD.2020.35.

738

739

25 Gérard Huet. Extending the calculus of constructions with type: Type, 1988. Unpublished draft. URL: https://pauillac.inria.fr/~huet/PUBLIC/typtyp.pdf.

740

741

742

743

744

26 Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean termination tool 2. In Ralf Treinen, editor, *Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings*, volume 5595 of *Lecture Notes in Computer Science*, pages 295–304. Springer, 2009. doi:10.1007/978-3-642-02348-4\_21.

745

746

27 Zhaohui Luo. Notes on universes in type theory, October, 2012. URL: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf.

747

748

749

28 Christine Paulin-Mohring. Inductive definitions in the system coq rules and properties. In Marc Bezem and Jan Friso Groote, editors, *Typed Lambda Calculi and Applications*, pages 328–345, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg.

750

751

752

29 Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in coq. In Gerwin Klein and Ruben Gamboa, editors, *Interactive Theorem Proving*, pages 499–514, Cham, 2014. Springer International Publishing.

753

754

30 Terese. *Term rewriting systems*, volume 55 of *Cambridge tracts in theoretical computer science*. Cambridge University Press, 2003.

755

756

31 François Thiré. Sharing a library between proof assistants: Reaching out to the HOL family. In Frédéric Blanqui and Giselle Reis, editors, *Proceedings of the 13th International Workshop on*
757

758

759

760

761

762

763

764

765

766

767

768

Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018, volume 274 of EPTCS, pages 57-71, 2018. doi:10.4204/EPTCS.274.5.

32 François Thiré. *Interoperability between proof systems using the logical framework Dedukti*. (Interopérabilité entre systèmes de preuve en utilisant le cadre logique Dedukti). PhD thesis, École normale supérieure Paris-Saclay, Cachan, France, 2020. URL: https://tel.archives-ouvertes.fr/tel-03224039.

33 Vladimir Voevodsky. A universe polymorphic type system, October 22, 2014. An unfinished unreleased manuscript. URL: https://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Type_systems/UPTS_current/Universe_polymorphic_type_sytem.pdf.

34 Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. Csi: a confluence tool. volume 6803, pages 499-505, 07 2011. doi:10.1007/978-3-642-22438-6_38.