The Multiverse: Logical Modularity for Proof Assistants

Kenji Maillard

Gallinette Project-Team, Inria

Nicolas Margulies

ENS Paris-Saclay & Gallinette Project-Team, Inria

Matthieu Sozeau

Gallinette Project-Team, Inria

Nicolas Tabareau

Gallinette Project-Team, Inria

Éric Tanter

PLEIAD Lab, Computer Science Department (DCC), University of Chile

Proof assistants play a dual role as programming languages and
logical systems. As programming languages, proof assistants offer standard
modularity mechanisms such as first-class functions, type polymorphism and modules. As logical
systems, however, modularity is lacking, and understandably so: incompatible
reasoning principles—such as univalence and uniqueness of identity
proofs—can indirectly lead to logical inconsistency when used in a given
development, even when they appear to be confined to different modules. The
lack of logical modularity in proof assistants also hinders the adoption of
richer programming constructs, such as effects. We propose the multiverse, a
general type-theoretic approach to endow proof assistants with logical
modularity. The multiverse consists of multiple universe hierarchies that
statically describe the reasoning principles and effects available to define a
term at a given type. We identify sufficient conditions for this structuring
to modularly ensure that incompatible principles do not interfere, and to
locally restrict the power of dependent elimination when necessary.
This extensible approach
generalizes the ad-hoc treatment of the sort of propositions in the proof
assistant. We illustrate the power of the multiverse by describing the
inclusion of -style propositions, the strict propositions of Gilbert et
al., the exceptional type theory of Pédrot and Tabareau, and general
axiomatic extensions of the logic.

§ INTRODUCTION

Modularity is key to scalable software development  <cit.>. As the adoption of proof assistants to write certified programs <cit.> increases, software engineering aspects become crucial. Proof assistants are peculiar in that respect due to their dual role for programming and proving.

Indeed, while proof assistants such as  <cit.> and  <cit.> offer traditional mechanisms for modular programming, including functional abstraction and modules, they lack modularity at the logical level.

To illustrate, consider two logical principles which are known to be incompatible:
univalence, a principle coming from Homotopy Type Theory <cit.>, which provides a rich, computationally-relevant content to equality, and uniqueness of identity proofs (UIP), which considers two proofs of the same equality as necessarily equal. From both principles, one can derive a contradiction. But this conflict can be quite pernicious, as inconsistency can arise from seemingly harmless consequences of these principles. For instance, using univalence one can prove that there exists an equality on the type of
booleans, such that transporting $\mathtt{false}$ along this equality (noted
$e \# \mathtt{true}$ below) gives $\mathtt{false}$:

\exists \ e : \bool = \bool, e \# \mathtt{true} = \mathtt{false}.

This property does not mention univalence explicitly (in its “interface”), yet combining it with UIP yields to inconsistency. In practice, this means that developers must make global commitments to certain reasoning principles in order to be sure that the underlying logic of their development is consistent. For instance, an development that imports univalence with the pragma
<cit.> must be devoted to univalence and cannot be mixed with other incompatible extensions. Likewise, concerns about whether the use of classical principles is accepted or not must be made globally.
Therefore providing logical modularity is a whole new challenge in itself, not addressed by well-known modular programming constructs. The Curry-Howard correspondence between both words has its limits, unfortunately.

Another major consequence of the lack of logical modularity in proof assistants is that the use of effects in the programming language is typically demonized. However, software developers are well acquainted with the use of effects such as mutable state, exceptions, or control operators, and a great deal of effort involves addressing the mismatch between the pure world of proof assistants and real-world programs. Intuitively, the problem is that effects break a number of standard reasoning principles; for instance, the commutativity of addition on natural numbers is easy to prove by induction, but this induction principle is no longer valid in its full generality with effects, due to the relevance of evaluation order.
Recently, <cit.> proved that mixing general induction
principles, a.k.a. dependent elimination, substitution, and effects, leads to inconsistency.
This incompatibility has a longer history, of course. The addition of
effects to a logical system can be traced back to double-negation translations <cit.>,
although the modern standpoint can be attributed to <cit.>, as used for instance
in F$\star$ <cit.>. However, <cit.> show that defining a typed CPS
translation preserving dependent elimination is out of reach,
and similarly, <cit.> proves that the theory behind the proof
assistant is inconsistent with computational classical logic under the guise of
a  operator.

In retrospect, this incompatibility is an illustration of a very ancient issue: mixing
computational classical logic with the axiom of choice, whose intuitionistic version is a consequence of dependent elimination, is a well-known source of foundational problems <cit.>.

Is all hope lost for logical modularity in proof assistants? Is there a way to encapsulate the use of effects to well-defined parts of a development so that they do not globally break logical consistency?
We answer these questions affirmatively, building upon a couple of
approaches developed in specific settings. First, in order to address
the issue of combining univalence and UIP, <cit.> proposed the
notion of homotopy type system—later revisited as two-level type theory by <cit.>—which introduces two universe hierarchies in order to distinguish between so-called univalent types and strict types.

Second, <cit.> also propose the use of different universe hierarchies
to support consistent reasoning about effectful programs written in the Exceptional Type
Theory <cit.>.

Third, one can understand the well-known $\type$/$\prop$ distinction in under the same light:
$\prop$—which is a one-level hierarchy indeed—lives “apart” from
the $\type$ hierarchy, with a restricted elimination schema from
$\prop$ into $\type$, known as singleton

This restriction ensures that $\prop$ is compatible with proof irrelevance—a property assumed by the extraction mechanism <cit.>
to ensure computability of erased code—because otherwise
one could prove that the type of booleans in $\prop$ has two distinct inhabitants.

While all these theories share the same substrate—Martin-Löf Type Theory <cit.>—they come with their own pecularities and metatheoretical justifications, either developed on paper
<cit.> or mechanized
<cit.>, involving a great deal of human effort and repeated work.
Here, we develop a generic framework for defining, studying and combining such theories.
For example, the addition of inductive types to a specific sort can in many cases be performed in a uniform manner. We additionally build a generic logical relation model that can accommodate multiple sorts, each with different sets of logical and computational principles, generalizing prior work by <cit.>.  To achieve this, we abstract the introduction of type constructors in a given sort and their inhabitants, along with their associated computational principles.

Building upon this analysis and generalizing the idea of using a separate universe hierarchy to isolate a given reasoning principle or effect, this work develops the notion of the multiverse as a principled type-theoretic approach to endow proof assistants with logical modularity.

The multiverse is a system with multiple universe hierarchies
that statically describe which principles and effects are available to
define a term at a given type.

The multiverse permits
the controlled use of incompatible reasoning principles in a development, where such principles can be used separately to establish different results about the same object of study, without any risk of unintended interference. Likewise, the multiverse makes it possible to extend the programming language of a proof assistant with effects, by locally restricting the power of dependent elimination in accordance with the considered effects.

* We introduce , a dependent type theory parametrized by a
description of multiple universes hierarchies and computational principles in <ref>.

* We illustrate the expressivity of the framework in <ref> with a presentation of
inductive types, concrete instances providing -style propositions, the Exceptional
Type Theory as well as general axiomatic extensions of the logic,
and identify sufficient conditions for a universe to admit dependent elimination.

* We show in <ref> that  indeed provides a modular
framework: two independent parametrizations of  can be combined without
endangering the metatheoretical properties of its core.

* We prove important metatheoretical results on
that ensure consistency, canonicity and decidability of typechecking
for any valid parametrization of the theory, showing that is suitable as an idealized
theory for proof assistants implementations (<ref>).

* We briefly explain how the addition of extensionality
principles fit in our framework and use it to describe an instance of
with strict propositions ($\sprop$) <cit.> as can be found in
and , hence subsuming the theory of existing proof assistants.

Finally, <Ref> discusses related work and <Ref> concludes.

Software correctness, and in particular formal software correctness,
is gaining more and more traction; from financial considerations for
blockchain applications to lethal issues in medicine and autonomous
vehicles. Interactive theorem provers based on the correspondence
between logical systems and programming languages have shown their
effectiveness to prove correctness of important pieces of software
like a C compiler <cit.> or a software-to-hardware toolchain
<cit.>. However, they suffer from a major limitation: the lack of
modularity when considered as logical systems. Indisputably, as
programming languages, proof assistants provide a great level of
modularity with the massive use of higher-order abstractions and
modules; but as logical systems, the modular mechanisms are mostly
absent. The fact that modularity has not circulated from the
programming to the logical side through the correspondence between
them may be surprising, as the notion of modularity, as original
pioneered by Parnas, is one of the key ingredients of modern
programming languages for the conception, scalability and maintenance
of software systems. So one could legitimately wonder why this key
concept has not found its logical counterpart. Indeed, a suitable
notion of logical modularity would make it possible for instance to
assume or provide different logical principles at different places of
a formalization while carefully controlling their potential
interactions. The reason for this lack of modularity is that
traditional programming mechanisms are not enough to provide logical
encapsulation. This is because logical consistency can be endangered
not only by the direct use of incompatible principles, but also simply
by the combination of apparently harmless consequence, so preventing
the use of two incompatible principles in the same module, for
instance, is not enough to guarantee logical consistency of the
system. In practice, this prevents a developer to use e.g., libraries
based on univalence (a principle coming from Homotopy Type Theory
<cit.>) together with other libraries based on uniqueness of
identity proofs (UIP). Indeed, in this particular situation, using
univalence allows a developer to expose a proof of the following
property, saying that there exists an equality on the type of
booleans, such that transporting true along this equality (noted
$e \# true$ below) gives false:

\exists \ e : \bool = \bool, e \# \mathtt{true} = \mathtt{false}.

This property alone, which does not mention univalence, is enough to
derive inconsistency from the use of UIP. Therefore providing logical
encapsulation is much more challenging than on the programming

This paragraph is redundant with the section on “early attempts to
recover modularity”

An important consequence of this lack of logical modularity is
that each time a developer wants to use a particular principle, for
instance importing univalence in with the pragma
, then its development is devoted to
univalence and cannot be mixed with other incompatible extensions of
. And even when the principle is not necessarily inconsistent with
other ones, the use of this principle may suffer from more conceptual
repudiations, as it is the case for instance with classical principles
and constructive concerns. These tensions result in a fragmentation of
the community, between people being devoted to one principle or

*Effects and Proof Assistants.

Another manifestation of the lack of logical modularity is the absence
of effects in the programming languages implemented inside proof
assistants. Indeed, some basic programming mechanisms—such as
exceptions or mutable memory—are absent from the language of their
theory, leading to complexity and efficiency issues. Consider a simple
example, the $\mathtt{head}$ function over lists of type A as defined for example
in Haskell, where the empty list case is handled by an exception:

:     $\mathtt{\forall (l : list A), lenght l \neq 0 -> A}$

To define the similar $\mathtt{head’}$ function inside a proof assistant, the
type of the function needs to be more precise, taking the fact that
the length of the list is non-zero as an additional argument (the term
e in the definition of $\mathtt{head’}$).

This means that a developer needs to understand (in)equality in the
theory, the proof that $\mathtt{0}$ is equal to itself with
$\mathtt{refl \ 0}$ and the fact
that from a contradiction, we can conclude anything with the function
$\mathtt{absurd}$ of type $\mathtt{\forall A, \bot \rightarrow A}$.

Thus the term $\mathtt{absurd \ A \ (e \ (refl \ 0))}$ is a term of type $\mathtt{A}$ exploiting the
absurdity of the proof $\mathtt{e}$ that the size of the empty list is
non-zero. Arguably, this makes the definition of the head function
significantly harder. While this function could be defined once in a
library, hence hiding its complexity for its users, the hardest part
is in fact not the definition of the function itself, but rather its
use. Indeed, each time $\mathtt{head’}$ has to be called in a program, the
developer needs to provide a proof that it is applied to a non-empty
list. This can quickly become complex, even impossible if the
specification of the program is missing some hypothesis. This means
that there is a strong entanglement between defining a program and
proving its correctness, which prevents from testing before
proving. As a consequence, a non-expert developer is often puzzled
inside a definition, not knowing if she is unable to prove the
correctness of the program or if the program she tries to prove is
simply not correct. Taking aside the complexity and lack of
efficiency, the absence of effects forces developers to stay in the
“all programs and proofs must be fully specified and terminating”
paradigm, which prevents quick prototyping and testing before entering
the full certification process. In particular, the presence of native
exceptions in the languages is a prerequisite for the introduction of
gradual typing discipline in proof assistants.  The addition of
effects to a logical system is not a new subject and can be traced
back to double-negation translations <cit.>, although the modern
standpoint can be attributed to Moggi in his seminal paper <cit.> as used
in F* <cit.>. But Barthe and Uustalu showed that writing a typed CPS
translation preserving dependent elimination was out of reach <cit.>,
and similarly Herbelin proved that the theory behind the proof
assistant is inconsistent with computational classical logic

Retrospectively, this should not have been that surprising. This
incompatibility is the reflection of a very ancient issue: mixing
classical logic with the axiom of choice, whose intuitionistic version
is a consequence of dependent elimination, is a well-known source of
foundational problems <cit.>.

Let us explain with an example why it is
not possible to simply add effects naively to a complex logical system
using new primitives. Consider the statement “the addition on natural
numbers is commutative”:

\forall n \ m : \nat. \ n + m = m + n.

This lemma is easy to prove using a proof assistant, by induction on
natural numbers. However, the addition of natural numbers is not
commutative in the presence of effects because the result of a
computation depends on the order of evaluation, which is a well known
fact for any C, Java or Python programmer. A direct consequence is
that in an effectful proof assistant, the standard induction principle
on natural numbers is not valid anymore, at least not in its full
generality. This incompatibility has then been further investigated
recently <cit.>: mixing general induction
principles, a.k.a. dependent elimination, substitution, and effects
leads to inconsistency. Thus, because of the absence of modularity in
the logic of proof assistant, there is no hope to integrate effects in
proof assistants without sacrificing deeply its logical power,
something that most users will arguably not be ready to do.

*Early attempts to recover modularity.

It is well-known that some common principles are inconsistent
altogether. This is for instance the case of the axioms of choice and
of determinacy. The common solution to this issue is to choose upfront
one of those principles and careful avoid to use the other. That is,
once a principle is stated and used by one definition or proof, it has
to be valid in any library that makes use of it. For instance, this
prevents a developer to use libraries based on univalence on one side,
and other libraries based on uniqueness of identity proofs (UIP) on
the other side because univalence and UIP are inconsistent
altogether. In the same way, assuming a type theory with general
exceptions directly leads to inconsistency because any theorem can be
proven by raising an exception. And even when the principle is not
necessary inconsistent with other ones, the use of this principle may
suffer from more conceptual repudiations, as it is the case with
classical principles and constructive concerns although there are no
strong reasons to reject classical reasonings in a constructive
setting, as long as those reasonings are not supposed to produce
computationally relevant (proof) terms. The common problem of all
those examples is the impossibility to locally keep track of the
available principles, without imposing them to be available globally.

To solve the issue of combining univalence and UIP, Vladimir
Voevodsky has proposed the notion of homotopy type system, later
rephrased as two-level type theory by Capriotti et
al. <cit.>, with two distinct hierarchies of
universes to distinguish between univalent and strict types.

In a similar—although unrelated—way, it has been proposed to
distinguish between exceptional and pure types by using two distinct
hierarchies of universes, thus preventing the possibility of proving
propositions by simply raising an exception <cit.>. Those two
similar solutions to apparently different problems suggest that they
might both be instances of a general notion that would allow to treat
logical or computational principles more locally, preventing them from
leaking entirely to the whole logical system.

This paper provide a mechanism that brings modularity in the proof
assistant at the level of logic. The notion of modularity
permits the combined use of incompatible principles, ensuring
consistency by keeping track of them and guaranteeing that those two
principles cannot interfere. This notion of modularity also
makes it possible to add effects in proof assistants, by restricting
the power of dependent elimination locally, which is the principle
that allows to reason about dependent inductive structures; such
restriction depends on the nature of the effect.

To that end, we define a system with multiple universe hierarchies
that statically describes which effects/principles are available to
define a term at a given type. Indeed, a similar restriction is for
instance used in the Calculus of Inductive Constructions to describe
when an inductive type in the universe $\prop$ of propositions can be
eliminated to produce a term in an arbitrary type. In a way, $\prop$ can
be seen as an effectful universe, where the effect is (the
compatibility with) proof irrelevance. Thanks to this static
information, it becomes possible for instance to distinguish between
pure and effectful types, to restrict the use of elimination
accordingly, or to distinguish between univalent and strict types to
restrict the behavior of equality accordingly.

The present paper makes the following contributions:

* we introduce , a dependent type theory parametrized by a
description of multiple universes hierarchies and computational principles in <ref>;

* we describe concrete instances of  accounting for the theory
of or , but also theories that are currently out of reach of existing
proof-assistants such as ExcTT in <ref>;

* we prove in <ref> important metatheoretical results on
that ensure consistency, canonicity and decidability of typechecking
for any parametrization of the theory, showing that it is suitable as an idealized
theory for proof assistants implementations;

* we explain in <ref> how the aforementioned
metatheoretical results enforce modularity of the whole theory, and
show that the framework is expressive enough to encompass inductives and
dependent elimination under reasonable hypothesis.

§ MUTT: MULTIVERSE TYPE THEORY

After a brief introduction to type theory, we present the syntax and typing of the Multiverse Type Theory (), highlighting its parametrization, along with the expected conditions that a specific  parametrization must satisfy in order to be valid. Valid parametrizations of  yield a type theory suitable to serve as the basis for proof assistants.

Martin-Löf Type Theory () <cit.> is a
dependent type theory featuring  dependent products (functions), dependent sums
(pairs) and identity types (equality). In  there is a single sort for all types, which is left implicit. The sort is represented by a universe constructor $\univ{}$ that classifies all types, including itself (represented as $\verb|Set|$ in ). For example, a dependent function has a product type, and that product type itself has the type $\univ{}$.
More precisely, because the sort is predicative, it is structured as a stratified hierarchy of universes $\univ{}_i$, each at universe level $i$, so that $\univi{}{i}$ has type $\univi{}{i+1}$.

The Calculus of Inductive Constructions () <cit.>
generalizes  to include a schema for arbitrary inductive types and their
elimination principles.

For instance, the natural numbers can be defined in  and one
can use the natural induction principle to reason about them. , like the
Calculus of Constructions <cit.>, features an additional sort
for propositions. Terms of a type of the proposition sort have a special
status as computationally-irrelevant information that can be erased through
extraction <cit.>. Additionally, the sort of propositions is
impredicative, in contrast to the sort of types for computationally-relevant
terms, and therefore the sort is not structured as a hierarchy. In , these two sorts are called $\type$ and $\prop$, respectively.

§.§ Syntax and Typing

and parametrization

Multiverse Type Theory () is an extensible variant of  with
multiple sorts. At its core, features dependent functions and universes,
together with an extensible framework to define multiple sorts, and their
inhabitants. This means that the formal presentation of is deeply
parametrized by a pair $\mathcal{P} = (\sorts, \Sigma)$:

* is parametrized by a set of sorts, with a distinguished sort
$\Type$ (read “type”). The sort $\Type$ is primordial: it is necessarily
present, and serves as the recipient to all universes, whatever their sort. A
parametrization of can include additional sorts. To any sort $s \in
\sorts$ corresponds a hierarchy $\univi{s}{i}$ of universes, where $s$ is the
sort of the universe and $i$ its level ($i \in
\mathbb{N}$). Hierarchies in are
always predicative.

Any universe $\univi{s}{i}$ has sort $\Type$ at level $i+1$, or equivalently, has type

Additionally, the set $\sorts \setminus \Type$ comes with a predicate
$\isolated{s}$ which characterizes sorts whose information cannot be
used in $\Type$.

* To populate the sorts in , is parametrized by two
sets underlying the signature $\Sigma$: a set of constants $\Csts$
and a set of rewrite rules ,
which specify the computational aspect of the constants.

All judgments of  are relative to the well-formed signature $\Sigma$

that guarantees the well-formedness of types,
constructors and eliminators, as well as determinism of the
reductions and their completeness when the sorts involved are
not isolated.

Syntax and notations
The syntax of , which is mostly standard except for the sort annotation on binders and universes, and the constants $c$ and $d$ from $\Csts$ (explained later on):

\[
\begin{array}{llcl}
\text{Terms} & t,u,p,A, B &::=& x \mid \lambda(\ctxvar{x}{A}{s}).t \mid t~u \mid c(\overline{t})
\mid \acst{d}{\overline{t}}{u}\mid \P{}(\ctxvar{x}{A}{s})\,B  \mid \univ{s}\\
\text{Substitutions}&\sigma, \overline{t} &::=& \emptySub \mid (\sigma, t) \mid t_1, \ldots, t_n
\end{array}
\]

The empty substitution is noted $\emptySub$, and $(\sigma, t)$ is the extension
of a substitution $\sigma$ with a term $t$.

We use overlined variables $\overline{x}$ to denote a substitution as a sequence
of terms or variables $x_i$ and sometimes abuse context notations $\overline{x}
: \Gamma$ to make explicit the name of the variables bound in the context

If $\Gamma$ is a context, $\Gamma_i$ is its component at the $i$th position and
$\Gamma_{<i}$ is its prefix excluding $\Gamma_i$.

As usual, we write $A \rightarrow B$ for the
non-dependent version of the dependent product.

We use the isomorphism between typing contexts and telescopes implicitly,
i.e. if $Γ ⊢ t : Π~Δ, A$ then we can talk about $\overline{u} : Δ$ a
well-typed instance/substitution for the context/telescope $Δ$.

<Ref> collects the defining judgments of , which are all parametrized by a well-formed signature $\Sigma$.

To account for different sorts, traditional judgments have to be augmented with information about the sort.

For instance, the formation rule of dependent product should mention both the sorts and the
universe levels (Rule infrule:explicit-Pi):

Γ⊢A :^s_1i

Γ,xAs_1,i ⊢B :^s_2j
Γ⊢xAs_1,iB  :^s_2ij

Γ,xAs_1 ⊢Bs_2

Because the formal treatment of universe levels is an orthogonal
concern that would obscure the presentation of the multisorted
extension of type theory, we adopt typical
ambiguity <cit.> and do not explicitly bind
universe levels $i$ in the rest of the paper, unless it helps understand the constructions.

we simply use a presentation as in Rule infrule:implicit-Pi. This presentation
makes more salient the main
information regarding the sorted version of $\Pi$: the sort of
a $\Pi$ is the sort of its codomain.
Therefore the typing judgment is written $\vdash t :^{s} A$. Likewise, the usual judgment $\vdash A$ of  which says that $A$ is a type is annotated with its sort $\vdash \ofsort{A}{s}$. Other judgments are decorated similarly.

$\Jctx{\Gamma}$    $\Gamma$ is a well formed context with respect to signature $\Sigma$

$\Jsub{\Gamma}{\sigma}{\Delta}$     $\sigma$ is a well formed substitution from $\Gamma$ to $\Delta$

$\Jty{\Gamma}{A}{s}$    $A$ is a well formed type at sort $s \in \sorts$ in context

$\Jtm{\Gamma}{t}{A}{s}$    $t$ is a well formed term of type $A$ in context $\Gamma$

$\Jconvty{\Gamma}{A}{B}{s}$    $A$ and $B$ are convertible types at sort $s$ in context $\Gamma$

$\Jconvtm{\Gamma}{t}{u}{A}{s}$    $t$ and $u$ are convertible at
type $A$ and sort $s$ in context

$\Jpat{\Gamma}{t}{A}{s}{d}$    $t$ is a well formed pattern of type $A$ in context $\Gamma$ for destructor  $d$

Judgments of

[Ctx-Cons]ΓAsΓ, xAs infrule:ctx-cons

Γ σΔ
Γ  (σ, t)   (Δ, xAs)

[Var]ΓAsΓ, xAsxAsinfrule:var
ΓBs_2Γ, yBs_2tAs_1infrule:weak

Γ, xAs_1Bs_2ΓxAs_1Bs_2infrule:pi-wf

xAs_1tBs_2Γł(xAs_1). txAs_1Bs_2infrule:pi-intro
Γt uBuxs_2 infrule:pi-elim

[Univ-Wf]s ∈
[Univ-El]ΓAsΓsAs infrule:univ-el

K ∈Σ

K = s

ΓK(t)s infrule:inert-type

c ∈Σ

c = K(u)

d ∈Σ

Γt    d

Γud [t]d

typing rules (universe levels omitted)

<Ref> adapts the standard rules of  to account for
multiple sorts and universe hierarchies.

The rules for well-formed type environment, substitution, variables,
dependent product, conversion, and universe are all standard from , but extended with the sort information. For instance, Rule infrule:pi-intro specifies that a lambda term that takes an argument of type $A$ in sort $s_1$ can be typed in another sort $s_2$ provided its body is. Likewise, an application can happen in any sort $s_2$, even if the argument is typed in sort $s_1$.

Rule infrule:univ-wf states that all
universes are of sort $\Type$.

The other uniform choice would assign the sort $s$ to $\univ{s}$, but this rule
is not valid in general, for instance the
sort of proof-irrelevant types of has actually sort $\Type$ as
proof-irrelevant types themselves are not proof-irrelevant and cannot
be assigned sort itself.

Following Coquand's reformulation of Russell's style presentation of
universes <cit.>, Rules infrule:univ-el and
infrule:el-univ together state that a type at sort $s$ can
equivalently be seen as a term of type $\univ{s}$.

The last three rules of <Ref> deal with the parametrization of with a set of constants $\Csts$, as mentioned above.

Constants are further classified depending on whether they are inert or active,
$\Csts = \Inert{} \cup \Active{}$. An inert constant $c \in \Inert{}$ does not trigger computation
( a type, such as $\List{}$, or a constructor, such as $\consName$), while an active constant $d \in \Active{}$ must come with suitable rewrite rules that specify its computational content ( the elimination principle of an inductive type, such as $\listrecName$). We now examine each in turn, using lists as a concrete parametrization example.

Inert constants

Inert constants are used to introduce new types (Rule
infrule:inert-type), commonly noted $K$,
as well as new constructors for types (Rule infrule:inert-term).

An inert constant $c$ is described by contexts $\params{c}$ and $\dom{c}$ as
well as a type $\cod{c}$ specifying the parameters, the domain of recursive
occurences and codomain of the inert constant.

The distinction between inert types and constructors is done
relatively to the codomain c, for which there are only two possibilities:
when $\cod{c} = \univ{s}$, then $c$ is an inert type of sort $s \in \sorts$,
and when $\cod{c} = K(\overline{u})$, then $c$ is a constructor of an inert type $K$ .

An applied inert type $K(\overline{t})$ is well-typed when $K$
appears in the signature $\Sigma$ and its arguments are of type

Note that by the condition of well-formedness of $\Sigma$, we know
that $\dom{K} = \cdot$.

An applied inert term $c(\overline{p},\overline{t})$ of an inert type
$K$ has type $K(\overline{u})[\overline{p}]$ when $c$ appears in $\Sigma$, its arguments $\overline{p}$ are of type $\params{c}$,
and the recursive occurrences $\overline{t}$ are of
type $\dom{c}$.

Note that here the substitution $\overline{u}$ providing the arguments
of $K$ is used to mediate between $\params{c}$ and $\params{K}$, which
may be different, in particular when encoding inductive types with

Consider the presentation of lists
as an inert type of sort $\Type$. The type $\List{}$  is
simply given by $\cod{\List{}} = \univ{\Type}$ and
$\params{\List{}} = \ctxvar{A}{\univ{\Type}}{\Type}$ making any $\List{A}$ with
$\ofsort{A}{\Type}$ well typed.

The constructor $\consName$ is given by $\cod{\consName} =
\List{A}$, $\params{\consName} =  \ctxvar{A}{\univ{\Type}}{\Type} ,
\ctxvar{a}{A}{\Type}$ and $\dom{\consName} = \ctxvar{l}{\List{A}}{\Type}$. In that case, the substitution
$\overline{u}$ from $\params{\consName}$ to $\params{\List{}}$ is
the first projection.

Using Rule infrule:inert-term, we get that
$\consList{A}{a}{l}$ is well-typed as an inhabitant of $\List{A}$ as
soon as $A$ is a type in $\Type$, $a$ is an inhabitant of $A$ and
$l$ is a list of $A$ itself.

Similarly for $\nilName$, we define $\cod{\nilName} = \List{A}$ and
$\params{\nilName} = \ctxvar{A}{\univ{\Type}}{\Type}$, leaving
$\dom{\nilName}$ empty.

Active constants

An active constant is
described by four parameters d, d, d and

$\params{d}$ corresponds to the (possibly empty) context of parameters of $d$.

The domain $\dom{d}$ specifies the type of the scrutinee of $d$.

As for inert terms, we restrict the system to accept only two alternatives for $\dom{d}$:
either $\dom{d} = \univ{s}$, in which case we define $\domsort{d} = \Type$; or
$\dom{d} = K (\overline{t'})$ with $K \in \Sigma$ and $\cod{K} =
\univ{s}$, in which case we define $\domsort{d} = s$.

An active term $\acst{d}{\overline{t}}{u}$ is well typed (Rule
infrule:active-term) when $d$ appears in $\Sigma$,
$\overline{t}$ is of type $\params{d}$, the scrutinee $u$ is of type
$\dom{d}[\overline{t}]$. When this is the case, its return type is $\cod{d}[\overline{t},u]$.

Coming back to the list example, the eliminator $\listrecName$ is presented as a term
destructor with $\dom{\listrecName} = \List{A}$,
$\params{\listrecName} = \ctxvar{A}{\univ{\Type}}{\Type}, \ctxvar{P}{A \rightarrow
\univ{\Type}}{\Type}\ , \ctxvar{p_\nilName}{P~(\nilList{A})}{\Type} ,
\ctxvar{p_\consName}{\PTerm{\ctxvar{a}{A}{\Type} ,
\ctxvar{l}{\List{A}}{\Type}}{P~l \rightarrow
and with $\codsort{\listrecName} = \Type$ and $\cod{\listrecName} = P~u$, where $u$ is the variable
associated to the scrutinee $\ctxvar{u}{\List{A}}{\Type}$ in
Rule infrule:active-term.

§.§ Conversion, Rewrite Rules, Reduction

ΓttAs infrule:refl
ΓutAs infrule:sym
ΓtvAs infrule:trans
[Conv-Univ-El]ΓABsΓsABs infrule:conv-univ-el

Γ, xAs_1t  xu  xBs_2
ΓtuxAs_1Bs_2 infrule:eta-conv
ΓtuAs infrule:red-conv
Γt ut' u'Buxs_2

Conversion for

<ref> presents the conversion rules of .

To insist on the central role of reduction in the theory, conversion
is defined as the transitive, reflexive, symmetric closure by
congruence of reduction.

Rule infrule:app-conv illustrates the congruence rule for

Reduction is embedded inside conversion through Rule infrule:red-conv.

Conversion additionally provides a way to navigate between type and
term conversion (Rules infrule:conv-univ-el and
infrule:conv-el-univ) and also features $\eta$-conversion for
functions (Rule infrule:eta-conv).

The definition of reduction itself is parametrized
by rewrite rules <cit.> that can be added to .

<ref> describes the notion of reduction in , which
features the usual notion of $\beta$-reduction
(Rule infrule:beta-conv). Because reduction is itself typed,
one needs to add a compatibility rule with conversion at the level of
types (Rule infrule:conv-red).

Congruence rules on applications and active terms are turned into
substitution rules in order to emulate reduction to weak-head normal forms (whnfs).

Indeed, the classification between inert $c \in \Inert{}$ and active constants
$d \in\Active{}$ gives rise to well-behaved
definitions of whnfs and neutral forms, two key notions to establish the

\[
\begin{array}{l@{\qquad}lclr}
\whnf{t}& w &::=& ne \mid \P{}(\ctxvar{x}{A}{s})\,B \mid
\l(\ctxvar{x}{A}{s}).\,t\mid \univ{s} \mid c(\overline{p},\overline{t}) & \\
\neutral{t}& ne &::=& x \mid ne~t \mid \acst{d}{\overline{t}}{ne} \mid \acst{d}{\overline{t}}{c(\overline{p},\overline{u})} &
\hspace{3em} \lnot \react{d}{c}
\end{array}
\]

These notions are at the heart of the logical relation given
in <ref>.

For now, it is enough to know that weak-head normal forms correspond to terms
that can not be head-reduced, of which neutral terms are the particular
cases where the term may not stay in weak-head normal form after substitution.

An inert type or inert term is always a whnf.

An active term is neutral when its scrutinee is in whnf and there is
no rewrite rule in  that can be fired, as expressed by the
following definition:

\react{d}{c} \quad \eqbydef \quad
\exists
\rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r} \in \RewRules{} , \quad
pat = c~q
% \exists
% \rho , \quad
% %\Jsub{\Gamma}{\rho}{\Delta},\quad
% \overline{t} = \overline{x}[\rho] \wedge u = \erasepat{pat}[\rho].

So to achieve whnf reduction, we need to add a substitution rule
(Rule infrule:app-subs) that
reduces the left-hand side of an application and the
scrutinee of an active term until it reaches a whnf.

Finally, each rewrite rule in  is turned into a reduction
rule using rule infrule:rew-red, which basically considers
any correct (linear) instantiation of a rewrite rule.

Γ(ł(xAs_1). t) utuxBuxs_2 infrule:beta-conv
ΓtuBs infrule:conv-red
Γt ut' uBuxs_2
[Active-Subs] Γpd

(t, a) = (x,  pat) [σ']

Γd(t, a)d[t,

a]d infrule:rew-red

Reduction Rules for

\begin{align}
\label{eq:pattern}
p\enspace &::=\enspace c(q_1,\ldots, q_n) \mid \P{}^s~q_1~q_2 \tag{pattern}\\
q\enspace &::=\enspace \metavar{x} \mid {\metavarrec{z}{\sigma}}
\tag{meta-variable}
\end{align}

$\Jpat{\Gamma}{p}{A}{s}{d}$ Pattern typing.

xAs ∈Γ
infrule:metavar-pat [Sub-Pat]
Γ σΔd
Γ  (σ, t)   (Δ, xAs) d
Γq_1s_1d  Γq_2q_1 → s_2d
Γ^s_1 q_1 q_2s_2d

zd[σ]s ∈Γ

$\erasepat{pat}, \occrec{d}{pat}, \occrecsub{d}{pat}$
erasure to terms, context and substitution of recursive hypothesis.

\[\arraycolsep=1pt
\begin{array}{lcl}
\erasepat{\metavar{x}} & := & x
\\
\erasepat{\metavarrec{z}{\sigma}} &:=& z
\\
\erasepat{\P{}^s\,q_1\,\metavar{x}} &:=&
\P{}(\ctxvar{y}{\erasepat{q_1}}{s})\,(x~y)
\\
\erasepat{\P{}^s\,q_1\,\metavarrec{z}{\sigma}}&:=&
\P{}(\ctxvar{y}{\erasepat{q_1}}{s})\,(z~y)
\\
\erasepat{c(q_1, \ldots, q_n)} &:=& c(\erasepat{q_1},\ldots, \erasepat{q_n})
\end{array}
\begin{array}{lcl}
\occrec{d}{\metavar{x}} &:= & \emptyContext
\\
\occrec{d}{\metavarrec{z}{\sigma}} &:=&z^{\rec} : \cod{d}[\sigma,z]
\\
\occrec{d}{\P{}^s\,q_1\,\metavar{x}} &:=& \occrec{d}{q_1}
\\
\occrec{d}{\P{}^s\,q_1\,\metavarrec{z}{\sigma}} &:=& z^{\rec} :
\P{}(\ctxvar{y}{\erasepat{q_1}}{s})\,
\cod{d}[\sigma,z~y]
\\
\occrec{d}{c(q_1, \ldots, q_n)} &:=& \occrec{d}{q_1}, \ldots, \occrec{d}{q_n}
\end{array}
\]

\[
\begin{array}{lcl}
\occrecsub{d}{\metavar{x}} &:=& \emptySub \\
\occrecsub{d}{\metavarrec{z}{\sigma}}&:=& \acst{d}{\sigma}{z}\\
\occrecsub{d}{\P{}^{s}\,q_1\,\metavar{x}} &:=& \occrecsub{d}{q_1}\\
\occrecsub{d}{\P{}^{s}\,q_1\,\metavarrec{z}{\sigma}} &:= &
\left( \occrecsub{d}{q_1}, \l{}(y : \erasepat{q_1}).\,d(\sigma,
\occrecsub{d}{c(q_1, \ldots, q_n)}&:=& \occrecsub{d}{q_1},\ldots, \occrecsub{d}{q_n}
\end{array}
\]

[Patterns typing]Syntax, typing rules and functions on

Patterns and Rewrite Rules
Active constants are interesting when associated to rewrite rules,
which make it possible to extend the conversion of .
A rewrite rule

$$\rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r} \in \RewRules{}$$

is given by a left-hand side,
characterized by its head symbol
$d$, which must be an active constant, a renaming
$\overline{x}$, and a pattern $pat$ for its scrutinee, and a
right-hand side $r$, which is simply a term.

It ensures that its left- and right-hand sides are convertible for
any instance of the (linear) context $Δ_{\lin{}}$ for which the
left-hand side is well-typed (infrule:rew-red in <ref>).

However, in general, the use of a linear context is not enough to
guarantee that the right-hand side is well typed, because this may
rely on some auxiliary conversions ensured by typing.

On the other hand, the use of a non-linear context alone is not
sufficient either because the reduction rule
infrule:rew-red would require a prohibitive use of conversion in the definition of

To remedy to this tension, a rewrite rule has two contexts $\Delta$ and $\Delta_{\lin{}}$ with
a renaming $\sigma$ (a substitution with only variables).

The point of the context $\Delta$ and substitution $\sigma$ is to
provide a non-linear version of the rewrite rule, which can be used for
typing purposes, with a side condition that every well-typed linear
occurrence of the rule is actually well-typed as a non-linear

When the rewrite rule is linear, that is when $\Delta = \Delta_{\lin{}}$
and $\sigma = id$,
we simply write $\rewrulelin{\Delta}{d}{\overline{x}}{pat}{r}$.

The syntax and typing rules of patterns are described in <ref>. A pattern
consists either of an inert constant $c \in \Csts$

or a $\Pi$ applied to metavariables, while a metavariable can be either a variable $\metavar{x}$ or
a recursive occurrence $\metavarrec{z}{\sigma}$.

The purpose of recursive occurrences is twofold. When typing a
pattern, a recursive occurrence has the type of the domain head
symbol $\dom{d}$, when its substitution $\sigma$ is a correct
substitution for the parameters of $d$ (Rule
infrule:metavarrec-pat-term). It additionally enforces that
the recursive occurrences $\metavarrec{z}{\sigma}$ correspond to
a variable $z$ with the same type in the context, which may be used in
the right-hand side of a rewrite rule.

Apart from these two rules, the typing rules of patterns just mimic the
typing rules for terms and substitutions.

From the pattern $pat$, we define three functions: a telescope
$\occrec{d}{pat}$ extending the context $\Delta$, collecting the recursive occurrences in
the pattern, which is used to typecheck the recursive calls to \(d\) in the
right-hand side of the rewrite rule; a substitution
$\Jsub{\Delta}{\occrecsub{d}{pat}}{\occrec{d}{pat}}$ instantiating all
occurrences of $\metavarrec{z}{\sigma}$ with the corresponding intended instance
of $d$; and an erasure function $\erasepat{pat}$ computing the underlying term
of a pattern.

A[σ] = d[x][σ]

Typing for rewrite rules

Finally, Rule infrule:rew-typing-term specifies when a
rewrite rule is valid (<ref>).

The rule checks that: (i) the renaming $\sigma$ is well-typed,
(ii) the rewrite rule is linearizable
(iii) the parameters $\overline{x}$ form a well-typed renaming to
$\params{d}$ in context
(iv) the pattern $pat$ is a well-typed pattern in context
(v) and that the right-hand side $r$ is a well-typed term, in the
context $\Delta$ extended with the information that the recursive occurrences
appearing in $pat$ are now seen as variables living in the codomain
of $d$ (modulo the renaming $\sigma$).

In the rule, the context $\Delta_{\lin{}}$ is used to typecheck separately the
arguments $\overline{x}$ and $pat$ of the left-hand side linearly, ensuring that
weak-head reduction is enough to detect when a rewrite rule can fire.

However, we need to allow non-linearity (described by the renaming $\sigma$) in
order to enforce that the types in the left-hand side agree up to the renaming
and to type-check the right hand-side, this even for the simple
example of lists (see <ref>).

To guarantee a posteriori that linear and non-linear matching are
equivalent, we introduce the notion of a linearizable rewrite rule.

A rewrite rule
$\rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r} $
is linearizable, noted
\linear{\rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r}}
$, when

(a) every variable in $\Delta_{\lin{}}$ occurs exactly once
in $(\overline{x},\erasepat{pat})$
and either

(b) $\dom{d} = \univ{s}$ and the
rewrite rule is linear; or

(b')  $\dom{d} = K(\overline{u_d})$ and the
following holds where $pat = c(\overline{q})$ and $\cod{c} = K(\overline{u_c})$:

% \left \{
%   \begin{array}{l}
% \dom{d} = \univ{s} \implies \Delta = \Delta_{\lin{}} \wedge \sigma = id \\[0.5em]
% \dom{d} = K(\overline{u_d}) \implies
\Jconvsub{\Delta_{\lin{}}}{\overline{u_c}[\overline{q}]}{\overline{u_d}[\overline{x}]}{\params{K}}
\Rightarrow \exists \tau , \, % : \Delta_{\lin{}} \hookrightarrow \Delta,
% \Jconvsub{\Delta_{\lin{}}}{\sigma \circ \tau}{id}{\Delta_{\lin{}}}
\tau[\sigma] = \id_{\Delta}  \wedge \Jconvsub{\Delta_{\lin}}{\sigma[\tau]}{\id_{\Delta_{\lin}}}{\Delta_{\lin}}.
% \end{array}
% \right.

The condition $(b)$ says that every eliminator on a universe must
be linear. The condition $(b')$ says that using the conversion
constraints collected from the fact that the left-hand side
type-checks, one can show that actually the renaming $\sigma$ admits an inverse,
in other word, linear and non-linear matching coincides up to conversion.

The precise type for the recursive occurrences is computed by the
function $\occrec{d}{pat}$.

Thus, when typing a rewrite rule, a recursive occurrence
$\metavarrec{z}{\sigma}$ of a pattern is seen as variable $z$ of
type $\dom{d}[\sigma]$ when typing both sides, and additionally as a variable
$z^{\rec}$ of type $\cod{d}[\sigma,z]$, representing the result of applying
$d$ to the variable, when typing the right-hand side.

This allows us to encode recursive calls to $d$ that may occur on the
right-hand side of a rewrite rule, as illustrated by the following example.

Coming back to the representation of lists, the two rewrite rules
for $\listrecName$ are:

$$\RewRules{\List{}} \enspace \eqbydef \enspace
\left |
\begin{array}{l}
\rewtyping{.}{\Delta}{\overline{p},A}{(\Delta,B:\univ{\Type})}{\listrecName}{\overline{p}}{\nilList{\metavar{B}}}{p_\nilName} \\
\rewtyping{.}{\Delta_{\mathrm{cons}}}{\overline{p},A,a,l}
\end{array}
\right.

with $\overline{p} = A, P, p_\nilName, p_\consName$ and

% \left \|
%   \begin{array}{l}
\Delta =
\overline{p} :\params{\listrecName} \quad
\Delta_{\mathrm{cons}} =
\Delta,\ctxvar{a}{A}{\Type},\ctxvar{l}{\List{A}}{\Type} \quad
\Delta_{\lin{}} =
\Delta,B:\univ{\Type},\ctxvar{a}{B}{\Type},\ctxvar{l}{\List{B}}{\Type}.
% \end{array} \right.

The first rewrite rule is valid because as the right-hand side
$p_\nilName$ has type $P~(\nilList{A})$, and the linearizability
condition amounts to show that $\overline{p},A$ has a retraction,
knowing that $A \equiv B$, which is direct by mapping $B$ to $A$.

The second rule makes use of a recursive occurrence
$\metavarrec{l}{\overline{p}}$, which corresponds both to the variable $l$ of
type $\List{A}$ and, for the right-hand side, to the variable
$l^{\rec}$ of type $P~l$ representing the recursive call on $l$.
Therefore, the right-hand side is well-typed, with type

Linearizability of the rule is similar to the case of $\nilList{}$.

§.§ Well-formed Signature

We now turn to the definition of a well-formed signature.

The signature imposes constraints on each inert and active constant that
structure their global behavior and interaction with the whole system.

Inert constants $K$ building types are then classified as positive if they come
with a set $\Inert{K}$ of inert constant called constructors to introduce them,
or negative if they come with a set $\Active{K}$ of active constants
called observations.

An active constant defined on a positive type is then called an
eliminator, whereas an inert constant inhabiting a negative type is
called a builder.

Universes are treated as positive types, with the exception that their
constructors are open-ended and consist of any type constant of the adequate sort.

A well-formed signature

is either the empty signature $\emptySig$, a well-formed signature $\Sigma$
extended with a well-formed positive type $(K, \Inert{K})$, negative type $(K,
\Active{K})$, an eliminator $(d, \RewRules{d})$ on a universe or positive type,
or a builder $(c, \RewRules{c})$ on a negative type.

We say that a constant or a rewrite rule $\kappa$ belongs to a well-formed signature
$\Sigma$, noted $\kappa \in \Sigma$, if it appears in one of its components.
Well-formedness for rewriting relies on three key properties—determinism of the
set of rewrite rules, progress and isolation—detailed next.

Deterministic rewrite rules

The first property ensures that the notion of whnf reduction defined
in <ref> is deterministic, which is crucial to
easily get confluence of the system.[We could adopt a
more permissive condition for confluence <cit.>, but this is not central here.]

A set of rewrite rules $\RewRules{}$ is deterministic, noted $\determine{\RewRules{}}$, if any two
rewrite rules from $\RewRules{}$
with common head symbol and common head-constant in their
patterns have the same right-hand sides:

\begin{align*}
\determine{\mathcal{R}} \enspace\eqbydef\enspace
\forall \rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r} ,
\rewrule{\Delta'}{\sigma'}{\Delta'_{\lin{}}}{d'}{\overline{x'}}{pat'}{r'} \in
\RewRules{},\\
d = d' \enspace \wedge \enspace
pat = c~q \enspace\wedge\enspace pat' = c ~ q'
\enspace\Rightarrow\enspace r = r'
\end{align*}

*Rewrite progress

The second notion that helps us characterize well-formed signatures is
progress between a set of inert terms and a set of active terms with respect to a set of
rewrite rules.

A set of inert constants $I$ and a set of active constants $A$ satisfy rewrite progress with respect to a set of rewrite rules
$\RewRules{}$, noted $\progress{I, A, \RewRules{}}$,

if every active constants in $A$ reacts to every constant in $I$ according to $\RewRules{}$:

\begin{align*}
\progress{I,A,\RewRules{}}\quad \eqbydef \quad \forall c \in I, d \in A, \enspace \reactR{d}{c}{\RewRules{}}
% \Jtm{\Gamma}{d(\overline{t};u)}{A}{s} &\enspace\wedge\enspace \whnf{u} \enspace \wedge\enspace
% \lnot \neutral{u} \quad\Rightarrow \quad \react{d(\overline{t}, u)}
% add react here
\end{align*}

When $I = \{c\}$ or $A = \{d\}$ are singleton, we note
respectively $\progress{c,A,\RewRules{}}$ and $\progress{I,d,\RewRules{}}$.

Isolated sorts

When there exists an active term $d$ for which rewrite progress does
not hold (with respect to its associated inert constants and rewrite
rules), the notion of canonicity, as defined in <ref>, is in danger.

To guarantee that in this case, canonicity in $\Type$ is still valid,
we rely on the notion of isolated sort, which ensures that
there is no “leak” from the sort hosting $d$ into $\Type$.

In counterpart, well-formedness condition on eliminators from isolated
sorts needs to ensure that isolation is preserved.

In a well-formed signature $\Sigma$ the following invariant will be maintained:

\begin{align*}
d \in \Sigma\enspace \wedge\enspace \isolated{s} \quad\implies\quad \isolated{s'}
% \isolated{s} &\overset{\text{coind}}{=}
% s \neq \Type \wedge \forall d\in \Active{}, \dom{d} = \univ{s} \vee \domsort{d} =
%                s \Rightarrow\\
% &\hspace{2cm}\exists s' : \sorts. \isolated{s'} \wedge (\cod{d} = \univ{s'} \vee \codsort{d} = s')
\end{align*}

where $d$ is an active constant and $\dom{d} = \univ{s} \vee \domsort{d} = s$ and $\cod{d} = \univ{s'} \vee \codsort{d} = s'$.

We can now turn to the definition of well-formed positive types,
negative types, eliminators (of positive types) and builders (of
negative types).

An inert constant $K$ building a type of sort $s$, $\cod{K} = \univ{s}$,
together with its constructors $\Inert{K}$ is
a well formed positive type in the signature $\Sigma$ when

* There is no active constant $d \in \Sigma$ defined on $\univ{s}$

\[\forall d \in \Active,\quad d \in \Sigma\enspace \Rightarrow\enspace \dom{d} \neq \univ{s}\]

* Its parameters are well-formed $\Jctx{\params{K}}$ and domain is empty
$\dom{K} = \emptyContext$

* Any inert constant $c \in \Inert{K}$ building a term in $K$, $\cod{c} = K (\overline{u})$, has
parameters, domain and codomain well-formed in $\Sigma$:

∀i, c_i = K(t) ∧ctK

Rule (1) forces new type constructors of a sort to be checked before
eliminators on the universe. Rule (2) says that an inert type has only
well-formed parameters. Rule (3) checks that every inert constant
populating $K$ have well-formed parameters and strictly positive
occurrences of arguments in $K$.

An inert constant $K$ building a type of sort $s$, $\cod{K} = \univ{s}$,
together with its observations $\Active{K}$ is a
well formed negative type in the signature $\Sigma$ when

* There is no active constant $d \in \Sigma$ defined on $\univ{s}$

\[\forall d \in \Active,\quad d \in \Sigma\enspace \Rightarrow\enspace \dom{d} \neq \univ{s}\]

* Its parameters are well-formed $\Jctx{\params{K}}$ and domain is empty
$\dom{K} = \emptyContext$

* $\Active{K}$ is an ordered set of active constant
$\overline{d}$ that share the same parameters as $K$,
$\forall i, \params{d_i} = \params{K}$.
Any $d_i \in \Active{K}$ has domain $K$, $\dom{d} = K(\id_{\params{K}})$,
and well-formed codomain in $\Sigma$ that can depend on the result of
previous $\overline{d}_{<i}$:

\[
\begin{dcases*}
\enspace\Jsub{\params{K}, \overline{\cod{d}}_{<i}}{\overline{t}}{\params{K}}& if $\cod{d_i} = K(\overline{t})$ \\[0.1cm]
\enspace\Jty{\params{K}, \overline{\cod{d}}_{<i}}{\cod{d_i}}{\codsort{d_i}} & otherwise
\end{dcases*}
\]

* If $s$ is isolated then any $d \in \Active{K}$ land in an isolated sort:

\[\forall s' \in \sorts, d \in\Active{d}, \isolated{s} \wedge (\cod{d} = \univ{s'} \vee
\codsort{d} = s') \Rightarrow \isolated{s'}
\]

The two first rules are the same as for positive types, and
the last rule dually checks active constants.
More specifically, the condition that all active constants shares the
same set of parameters $\params{K}$ ensures that those active
constants actually define observations of inhabitant of $K$.

An active constant $d \in \Active{}$ together with rewrite rules
$\RewRules{d}$ is well-formed in signature $\Sigma$ when
the following conditions hold, where

\[
\begin{dcases*}
s_d = s,\enspace \Inert{d} = \{\Pi\} \cup \{ K \in \Sigma \mid \cod{K} = \univ{s}\} &
if $\dom{d} = \univ{s}$ is a universe \\
s_d =
\domsort{d},\enspace \Inert{d} = \Inert{K}& if $\dom{d} = K(\overline{u})$ is a
positive type in $\Sigma$
\end{dcases*}
\]

* If $s_d$ is isolated, $d$ must land in an isolated sort, otherwise it
must satisfy progress:

\[
\begin{dcases*}
(\cod{d} = \univ{s'} \vee \codsort{d} = s') \wedge \isolated{s'} & if~
\progress{d,\Inert{d},\RewRules{d}}&otherwise
\end{dcases*}
\]

* Its parameters, domain and
codomains are well-formed in $\Sigma$

d, d, d∨s_d

* The rewrite rules in $\mathcal{R}_d$ are deterministic $\determine{\RewRules{d}}$, have head symbol $d$ and are well-typed

\begin{align*}
\forall \rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r} \in
\RewRules{d},\quad{}
\rewtyping{\Sigma}{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r}
\end{align*}

An inert constant $c \in \Inert{}$ building a term of negative type $(K,
\Active{K}) \in \Sigma$, that is $\cod{c} = K (\overline{u})$, together with
rewrite rules $\RewRules{c}$ is well-formed
in $\Sigma$ when:

* It satisfies progress or belongs to an isolated sort and its parameters, domain and codomains are well-formed in $\Sigma$:

d, c, c ∨c
∀i, c, c_<ic_i c_i

* The rewrite rules in $\RewRules{c}$ are deterministic
$\determine{\RewRules{c}}$, have patterns with head-constant $c$ and are well-typed

\begin{align*}
\forall \rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{c(\overline{q})}{r} \in
\RewRules{c},\quad
\rewtyping{\Sigma}{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{c(\overline{q})}{r}
\end{align*}

The type of lists, as other inductive types, is a positive
type. Thus, to check that it can be added to a well-formed
signature $\Sigma$, one need to check that $(\List{}, \{ \nilName,
\consName\})$ is a well-formed positive types in $\Sigma$, and that
$(\listrecName, \RewRules{\List{}})$ is a well-formed active
constant in $\Sigma , (\List{}, \{ \nilName,
\consName\})$.

The typing conditions for well-formation of
$(\List{}, \{ \nilName, \consName\})$ and
$(\listrecName, \RewRules{\List{}})$ can be simply checked in
general, as they are independent of $\Sigma$ in this specific situation,
and have already been discussed in the presentation of this example.

The last points to check are progress and determinism.

This is fairly straightforward as it amounts to check that there is
exactly one rule in $\RewRules{\List{}}$ for the eliminator
$\listrecName$ and the constructors $\nilName$ and $\consName$.

§.§ Metatheoretical properties of

We will prove in <ref>
that the well-formedness of a signature is sufficient to prove that  enjoys the
following metatheoretical properties for any valid parametrization $\mathcal{P} =
(\sorts, \Sigma)$, making it well-suited as the underlying theory
of a proof assistant.

* If $A$ is a closed type of sort $\Type$, $\Jty{}{A}{\Type}$, then $A$ is
convertible to either a universe $\univ{s}$, a dependent product
$\P{}(\ctxvar{x}{X}{s})Y$, or an inert constant $K(\overline{t})$.

* If $t$ is a closed term of a positive constant type $K(\overline{a})$ in ,

$\Jtm{}{t}{K(\overline{a})}{\Type{}}$ with $(K, \Inert{K}) \in \Sigma$, then
$t$ is convertible to a
constructor $c(\overline{p},\overline{v})$ with $c \in \Inert{K}$.

Assuming that $\Sigma$ provides an empty type in $\Type{}$, that is a positive
type $\ofsort{\bot}{\Type{}}$ with no introduction $\Inert{\bot} = \varnothing$,
we also obtain the logical consistency of $\Type{}$ for any parametrization.

There is no closed proof term $e$ of the empty type $\Jtm{}{e}{\bot}{\Type}$.

* If $\Jty{\Gamma}{A}{s}$ and $\Jty{\Gamma}{B}{s}$, it is decidable
whether $\Jconvty{\Gamma}{A}{B}{s}$ is derivable.

* If $\Jty{\Gamma}{A}{s}$, it is decidable whether $\Jtm{\Gamma}{t}{A}{s}$.

§ EXPRESSIVITY AND INSTANCES OF THE MULTIVERSE TYPE THEORY

This section develops several instances of parametrization of , building
upon the formal framework described in <ref>: inductive types
(<ref>), a -style sort of propositions (<ref>),
Exceptional Type Theory (<ref>), axioms
(<ref>), and dependent elimination (<ref>).

§.§ Inductive and Record Types

Section <ref> used lists to illustrate the definition of an inductive type;
one can easily infer the definition of natural numbers $\Nat$ as a non-decorated version of lists.
We now show that standard $\Sigma$-types and identity types can also be
represented faithfully in .

Σ types
$\Sigma$ types represent dependent pairs. They are, like $\Pi$-types,
a negative type constructor, defined by its two observations, the first and second projection.

* The type constructor $\SigmaName$ in
is given by: $\params{\SigmaName} = \ctxvar{A}{\univ{\Type}}{\Type}_i,
\ctxvar{B}{A → \univ{\Type}}{\Type}_j$,

* The projections are active constants $\fstName$ and $\sndName$ with
$\params{\fstName} = \params{\sndName} = \params{\SigmaName}$,
$\dom{\fstName} = \dom{\sndName} = \SigmaName~A~B$ and
$\cod{\fstName} = A$. For the second projection, $\cod{\sndName} = B~fst$,
where $fst : A$ (see definition <ref>, item 3).
This is an example where later projections depend on former ones.

* The default builder constant $\pairName$ is an inert constant
presented by $\cod{\pairName} = \SigmaName~A~B$ and $\params{\pairName} = \params{\SigmaName}, \,
\ctxvar{a}{A}{\Type} \ ,
\ctxvar{b}{B~a}{\Type}$

* We set $Δ = \params{\pairName}$ and

$\Delta_{\lin} = \params{\SigmaName}, \ctxvar{C}{\univ{\Type}}{\Type},
\ctxvar{D}{A → \univ{\Type}}{\Type}, \ctxvar{c}{C}{\Type}, \ctxvar{d}{D~c}{\Type}$

Ensuring progress we define the projection rewrite rules (deterministic because no overlap):

\[\begin{array}{l}
\rewtyping{\SigmaName,\fstName,\sndName}{\Delta}{A, B, A, B, a, b}
{\Delta_{\lin}}{\fstName}{\metavar{A}, \metavar{B}}{\pairName(\metavar{C}, \metavar{D}, \metavar{c}, \metavar{d})}{c} \\
\rewtyping{\SigmaName, \fstName, \sndName}{\Delta}{A, B, A, B, a, b}
{\Delta_{\lin}}{\sndName}{\metavar{A}, \metavar{B}}{\pairName(\metavar{C}, \metavar{D}, \metavar{c}, \metavar{d})}{d}
\end{array}\]

* For typing purpose of the second rewrite rule: observe that (after the action of the $Δ_{\lin}$ to $Δ$ substitution)
$b$ has type $B~a$ according to the typing rule for .
This type is convertible to $B~(\fstName(A,B\rewcomma\pairName(A,B,a,b)))$
thanks to the rewrite rule for $\fstName$.

Identity types

Illustrating the expressivity of our framework, we can also define standard Martin-Löf
identity types with the elimination rule of <cit.>.

* $\params{\Id} = \ctxvar{A}{\univ{\Type}}{\Type}_i,\> \ctxvar{a}{A}{\Type},\> \ctxvar{x}{A}{\Type}$
and $\cod{\Id} = \univ{\Type}_{i}$

* The unique constructor is $\Refl$, with $\params{\Refl} = \ctxvar{A}{\univ{\Type}}{\Type}_i, \ctxvar{a}{A}{\Type}$ and $\cod{\Refl} = \Id(A,a,a)$

* The elimination principle is an active constant $\J$ with $\dom{\J} = \Id(A,a,x)$,
$\cod{\J} = P~x~e$, and

\[
% \begin{array}{lcl}
\params{\J}  =  \params{\Id},\> \ctxvar{P}{Π (\ctxvar{x}{A}{\Type})~\Id(A,a,x){\to}\univ{\Type}}{\Type}, \>
\ctxvar{\metavar{pr}}{P~a~(\Refl(A,a))}{\Type}
% \dom{\J} & = & \Id~a~x \\
% \cod{\J} & = & P~x~e
% \end{array}
\]

* To define the rewrite rule for we set:

\[\begin{array}{lcl}
\Delta_{{\lin}} & = & \params{\J},\> \ctxvar{B}{\univ{\Type}}{\Type},\> \ctxvar{b}{B}{\Type} \\
\Delta & = & \ctxvar{A}{\univ{\Type}}{\Type},\> \ctxvar{a}{A}{\Type},\>
\ctxvar{P}{Π (\ctxvar{x}{A}{\Type})~\Id(A,a,x){\to}\univ{\Type}}{\Type},\> \ctxvar{pr}{P~a~(\Refl(A,a))}{\Type}
\end{array}\]

Then we can introduce a well-typed rule:

\[\begin{array}{l}
\rewtyping{\Id,\Refl}{\Delta}{A, a, a, P, pr, A, a}
{\Delta_{{\lin}}}{\J}{\metavar{A}, \metavar{a}, \metavar{x}, \metavar{P}, \metavar{pr}}{\Refl(B,b)}{\metavar{pr}}
\end{array}\]

Note here that the rewrite rule is highly non-linear: all the endpoints of
equalities $a, x, b \in \Delta_\lin$ are enforced to coincide through typing.

Using propositional equality, other inductive families can be defined in the so-called “Ford” style
<cit.>, where proper indices are simulated by parameters and

For example, to define vectors, we would have a type family with two parameters
$\ctxvar{A}{\Type}{\Type}, \ctxvar{n}{\Nat}{\Type}$ and the two constructors
would respectively be guarded by proofs of $\Id(\Nat,n,\Zero)$ and

A more categorically inspired, equivalent presentation of inductive families can
be found in <cit.> using Σ-types and identity
types to define proper indexed sums.

We expect higher-order recursive types like $W$-types could also fit in this
framework with a more elaborate handling of recursive occurrences
($\metavarrec{n}{p}$); we leave this as future work.

Beyond record types, generic coinductive types such as streams defined by
co-pattern matching <cit.> are almost within reach of , in
particular the logical relation developed in <ref> readily
accommodate them.

This would however require to dualize the treatment of reduction rules <ref> and their
typing (Rule infrule:rew-typing-term) to take into account co-recursive occurrences.

§.§ Prop

The proof assistant features a sort  () of propositions compatible with
a proof erasure semantics, a key property for extracting formally verified programs from developments.

This compatibility is obtained through a restricted elimination schema from
$\prop$ into $\type$, known as singleton elimination, that enforces that
is compatible with proof-irrelevance but does not impose that axiom

Singleton elimination, first studied explicitly by <cit.>, restricts
elimination on inductive types from to  to those inductives that have
syntactically at most one constructor and whose arguments are all in the sort .

As a consequence, the standard proof to distinguish the constructors of an
inductive type, e.g. to distinguish  from  in $\bool{}$, cannot
be reproduced for types in , e.g. $\boolProp{}$: the first step of the
proof builds a predicate $P : \boolProp{} \to \univ{\Type{}}$ such that
$P\,\true$ is inhabited and $P\,\false$ is empty, a step that requires the
forbidden elimination of $\ofsort{\boolProp{}}{\Prop}$ into the universe

Putting aside the peculiar aspects attached to impredicativity, that indeed turn
into a hierarchy on its own, it is relatively straightforward to encode a
predicative variant of -style  in .

We consider a fresh sort , and populate it with inductive type formers
$\I(\overline{p})$ and constructors $\ccst(\overline{x}) :
\I(\overline{p})$ as described in <ref> but restrict the usual
eliminators $\cstface{IRec}$ to -valued families, that is predicates $P :
\I(\overline{p}) \to \univ{\Prop}$.

Eliminators $\cstface{singletonRec}_{\I}$ for $\Type$-valued families are added only for
inductives $\I(\overline{p})$ that do satisfy the singleton criterion.

§.§ Exceptions

Exceptional Type Theory () of <cit.>
extends  with the ability to raise exceptions at any type.

This theory is further refined in <cit.> in order to reason on
exceptional terms in a consistent context.

This is achieved by introducing two sorts: a sort of pure types embedding standard
and a sort  for the exceptional hierarchy.

The use of exceptions is confined to types residing in the exceptional
hierarchy, which is explicit in the typing rule for the operator
raising those exceptions:

\[
\inferrule %[Raise]
\]

The eliminator for inductive types in  must then account for these
exceptions, requiring a special catch clause.

For instance, the eliminator from exceptional booleans to a sort
\(\elimsort\) takes the following form:

\[
\inferrule %[\catch{}-\(\bool\)]
{\Jtm{\Gamma}{P}{\boolE \to \univ\elimsort}{\Type}\\
\Jtm{\Gamma}{b}{\boolE}{\exc}\\
\Jtm{\Gamma}{h_{t}}{P~\true}{s}\\
\Jtm{\Gamma}{h_{f}}{P~\false}{s}\\
\Jtm{\Gamma}{h_{r}}{P~(\raiseFull{\boolE})}{s}}
\]

The specification of this eliminator is completed with the reduction rules where
$\overline{p} = P,b,h_{t},h_f,h_r$:

\begin{align}
\label{eq:catchB-rew}
\acst{\catchB}{\overline{p}}{\true} &\Rightarrow h_t&
\acst{\catchB}{\overline{p}}{\false} &\Rightarrow h_f&
\acst{\catchB}{\overline{p}}{\raiseFull{\boolE}} &\Rightarrow h_r
\end{align}

We can present as an instance of , reusing the sort  for pure
types plus a fresh sort $\exc{} \in \sorts$ populated with the inert constants
$\boolE, \true, \false, \boolexn$ and the active constants $\catchB$ and

The exceptional booleans $\boolE$ with $\cod{\boolE} = \univ\exc$ have as
constructors, beside the standard and constructors, a new
constructor $\boolexn$, all without parameters.

This makes \(\boolE\) a well-formed positive type in the empty signature and
\(\catchB\) is introduced as an eliminator on this well-formed type with:

= P→,
h_tP , h_fP ,

= ,b
= P b

together with the linear equations presented in (<ref>).

Again, \(\catchB\) is well-formed in the signature \(\boolE\) because

it is deterministic, as all patterns have different head symbols, and

satisfies rewrite progress, as all non-neutral weak-head normal
forms of type $\boolE$ ( \(\true, \false\) and \(\boolexn\)) do
react. Also, parameters, domain, codomain and rewrite
rules are well-typed  with respect to the signature \(\boolE\).

Finally, \(\raiseC\) is presented as an eliminator with \(\params{\raiseC} =
\emptyContext\), hence abbreviated $\raiseC(A)$ instead of
$\raiseC(\cdot\rewcomma A)$, defined on the universe \(\dom{\raiseC} := \univ\exc\), with codomain
\(\cod{\raiseC} = A, \codsort{\raiseC} = \exc\) where
$\oftype{A}{\univ\exc}{\Type}$ is the variable provided by the domain.
then comes with a rewrite rule for \(\P\)-types and another one for

The well-formedness of \(\raiseC\) is established as follows.

Determinism comes from the fact that all rewrite rules have a distinct head
symbol in their pattern.

All non-neutral weak-head normal forms in \(\univ\exc\) (\(\boolE\) and \(\P
A~B\)) do react.

The parameters, domain and codomain of \(\raiseC\) are well-typed.

Regarding the typing of the rewrite rules, the first one is easily well-typed.
As for the second, the \(\P\) pattern is indeed well-typed given the context,
and the variable \(B^{\rec}\) comes from \(\occrec{\raiseC}{\P^{s_1} \metavar{A}
\metavarrec{B}{\emptySub}}\) and has type \(\P(\ctxvar{y}{A}{s_1}) (B~y)\).

Note that, if we wanted to extend a base signature with additional type
constructors from <ref> like $\Sigma$-types or identity types,
the framework would require to consider these type constructors as
additional inert constants on which $\raiseC$ should react.

§.§ Axioms, locally

By parametrizing adequately , it is possible to add and work with a new
axiom inhabiting any chosen type \(Ax\) without compromising the
canonicity of $\Type$.

This is achieved by creating a new isolated sort \(\Ax\) which is a fresh
copy of \(\Type\), except that eliminations are restricted to \(\Ax\).

Then, the axiom can be realized by adding an active term
\(\oftype{\axiomTm}{Ax}{\Ax}\)
with no parameters ($\params{\axiomTm} = \emptyContext$) and $\dom{d} =
\Unit$, the trivial inductive type (or equivalently, no argument at all).

We do not attach any rewrite rule to $\axiomTm$ as this would amount
to realizing the axiom itself, breaking progress and therefore, $\axiomTm$ is well-formed only
because $\Ax$ is isolated, which precisely prevents leaking the axiom
into $\Type$.

However, the isolation property does not prevent us from defining a
boxing mechanism from $\Type$ into $\Ax$ with elimination into $\Ax$
that allows us to prove properties on inhabitants of $\Type$ using
$\axiomTm$, but only in the axiomatic sort $\Ax$.

Then, depending on the design choice, one can define one axiomatic
sort per axiom to encapsulate clearly which axiom has been used
directly in the type information, or consider an axiomatic sort
where any axiom can be postulated, thus encapsulating in the types
that an unsafe version of $\Type$ has been used.

This provides a type-theoretic, local and modular alternative to the
pragma of , or the  checker of .

Also, it allows users to make use of several incompatible axioms in the same
development, as long as they are postulated in different isolated

§.§ Dependent elimination through universe unboxing

A sort $s \in \sorts$ has booleans if it is equipped with a type
$\ofsort{\bool_s}{s}$, terms $\oftype{\true_s,\false_s}{\bool_s}{s}$ and an
induction principle

\[\ind_{\bool_s} : (\ctxvar{P}{\bool_s \to
\univ{s}}{\Type{}})(\ctxvar{p_t}{P\,\true_s}{s})(\ctxvar{p_f}{P\,\false_s}{s})(\ctxvar{b}{\bool_s}{s})
\to P\,b.
\]

As explained in <ref>, this data is however not enough to show
expected properties of booleans, for instance to derive that $\true_s \not\equiv
\false_s$.

In order to recover the full power of large elimination on booleans of sort
$s$, we need the ability to define predicates taking value in $\univ{s}$ by case analysis:

\[
\inferrule{\Jtm{\Gamma}{P_{t}}{\univ{s}}{\Type{}}
\and \Jtm{\Gamma}{P_{f}}{\univ{s}}{\Type{}}
\and \Jtm{\Gamma}{b}{\bool_s}{s}}
\]

Note that this induction principle $\ind^{\univ{s}}_{\bool_s}$ specialized to
$\univ{s}$ is not an instance of $\ind_{\bool_s}$ because
$\univ{s}$ resides in the sort $\Type{}$.

Rather than requiring for each inductive type in sort $s$ to come equipped with
two elimination principles, it is actually enough to have a reflection of
$\univ{s}$ in sort $s$, that is a type $\ofsort{\BoxInd\,\univ{s}}{s}$ equipped
with terms $\Jtm{}{\boxC}{\univ{s} \to \BoxInd\,\univ{s}}{s}$ and
$\Jtm{}{\unbox}{\BoxInd\,\univ{s} \to \univ{s}}{\Type{}}$ such that
$\Jconvtm{\Gamma}{\unbox \,(\boxC\,A)}{A}{\univ{s}}{\Type{}}$ for any type $\oftype{A}{\univ{s}}{\Type{}}$.

Given such a reflection, we can derive the induction principle
$\ind^{\univ{s}}_{\bool_s}$ from the standard induction principle as follows:

\[\ind^{\univ{s}}_{\bool_s}~P_t~P_f~b\eqbydef \oftype{\unbox \left (\ind_{\bool_s} (\lambda
(x : \bool_s).\,\BoxInd\,\univ{s})~(\boxC\,P_t)~(\boxC\,P_f)\,b \right )}{\univ{s}}{\Type{}}\]

Of course, such a reflection does not always exist for an arbitrary
sort $s$, in particular in the case of $\Prop$. But it exists for
instance for $\exc$ which justifies why dependent elimination is valid
in . The term $\ofsort{\BoxInd\,\univ{\exc}}{\exc}$ is basically
obtained as $\univ{\exc}$ plus a default type $\deamon$ in $\exc$ for the exception in
$\BoxInd\,\univ{\exc}$, $\raiseFull{\BoxInd\,\univ{\exc}} \equiv \deamon$.

§ MODULARITY OF

As formalized and illustrated previously, is extensible by means of its parametrization.
We now show that delivers on the modularity front: two parametrizations
of can be merged seamlessly, preserving the metatheoretical results of each independent parametrization.
As explained in the introduction, modularity is key to allow developments to
locally rely on extensions such as exceptions or axioms, without interfering
with each other, i.e. the metatheoretical properties in <ref>
are always preserved.

A parametrization $\mathcal{P}' = (\sorts', \Sigma')$ is a proper extension of
$\mathcal{P} = (\sorts, \Sigma)$, noted $\mathcal{P} \extendMuTT{}
\mathcal{P}'$, when $\sorts \subseteq \sorts'$, each component of $\Sigma$ are
in $\Sigma'$, isolation is preserved and any active constant $d \in \Sigma'$ defined on a universe $s$ is
either already in $\Sigma$ or occurs on a sort not appearing in :

\[\forall d \in \Sigma',\qquad \dom{d} = \univ{s} \quad \Rightarrow\quad d \in \Sigma \vee s
\notin \sorts\]

For any parametrization $\mathcal{P}$, the identity is a proper extension $\mathcal{P} \extendMuTT{} \mathcal{P}$
and proper extensions compose, forming a preorder with initial object
$\mathcal{P}_\Type = (\{\Type\}, \emptySig{})$.

All typing judgments of  presented in <ref> are
functorial with respect to proper extensions, that is, if $(\sorts, \Sigma)
\extendMuTT{} (\sorts', \Sigma')$ and $\Sigma ; \Gamma \vdash \mathcal{J}$ is
a derivable judgment then $\Sigma'; \Gamma \vdash \mathcal{J}$ is also derivable.

By induction on the derivation of the judgment $\Sigma ; \Gamma \vdash
\mathcal{J}$ noting that typing derivations only use that constants belongs to
$\Sigma$, a property preserved by proper extensions.

Importantly, well-formed signature extensions, as defined in
are compatible with proper extensions, with the exception of active constants
defined on universes:

Suppose $(\sorts, \Sigma) \extendMuTT{} (\sorts', \Sigma')$.

Positive type extension If $\Sigma, (K, \Inert{K})$ is a well-formed signature then so is $\Sigma', (K, \Inert{K})$;

Negative type extension If $\Sigma, (K, \Active{K})$ is a well-formed signature then so is $\Sigma', (K, \Active{K})$;

Eliminator extension If $\Sigma, (d, \RewRules{d})$ is a well-formed
signature with $\dom{d} = K(\overline{u})$ then so is $\Sigma',
(d, \RewRules{d})$;

Builder extension If $\Sigma, (c, \RewRules{c})$ is a well-formed signature then
so is $\Sigma', (c, \RewRules{c})$.

Suppose $(K, \Inert{K})$ is a well-formed positive type in $\Sigma$ with
$\cod{K} = \univ{s}$, we show that it is a well-formed positive type in $\Sigma'$.

By functoriality of judgments, all conditions but the first are satisfied.

Suppose $d \in \Sigma'$ has domain a universe $\univ{s'}$ then either $d \in
\Sigma$ and, by well-formedness of $K$, $s' \neq s$, or $s' \notin \sorts$ so
$s' \neq s$.

A similar argument applies for well-formed negative types.

Suppose $(d, \RewRules{d})$ is a well-formed eliminator on a positive constant,
$\dom{d} = K(\overline{u})$ in $\Sigma$, we show that it is well-formed as well in $\Sigma'$.

Since $(K, \Inert{K}) \in \Sigma$ and proper extensions preserve components,
$(K, \Inert{K}) \in \Sigma'$.

$\determine{\RewRules{d}}$ and $\progress{\Inert{K},d,\RewRules{d}}$ are
independent from the signature and all the typing conditions are consequences of
functoriality along proper extensions.

If $\domsort{d}$ is isolated in $\Sigma$ then $\codsort{K}$ is isolated in
$\Sigma$, and they are both isolated in $\Sigma'$ because
proper extensions preserve isolation.

Again, a similar argument applies for well-formed builders.

Let $\mathcal{P} = (\sorts, \Sigma)$ be a parametrization of  and
$\mathcal{P}_1 = (\sorts_1, \Sigma_1)$, $\mathcal{P}_2 = (\sorts_2, \Sigma_2)$
two proper extensions of $\mathcal{P}$. There exists a well-formed
signature $\Sigma_\cup$ on $\sorts_{\cup} = \sorts_1 \uplus_\sorts \sorts_2$
such that $\mathcal{P}_\cup = (\sorts_{\cup}, \Sigma_\cup)$ is a proper
extension of both $\mathcal{P}_1$ and $\mathcal{P}_2$.

Without loss of generality, we can assume that $\Sigma$ is a prefix of $\Sigma_1
= \Sigma \Sigma'_1$.

The construction of $\Sigma_\cup$ then proceeds by induction on $\Sigma'_1$,
extending inductively the proper extension $\mathcal{P} \extendMuTT{}
\mathcal{P}_2$.

All cases are covered by <ref>, except for the case of a well-formed
active constant with domain a universe, which we now discuss.

Assume that $(d, \RewRules{d})$ is well-formed in $\Sigma \Sigma'_1$, $\dom{d} = \univ{s}$.

The induction hypothesis states that we have well-formed signatures
$(\sorts_1,\Sigma\Sigma'_1) \extendMuTT{} (\sorts_{\cup},
\Sigma_2 \Sigma'_1)$ together with the indicated proper extension.

Since $d \in \Sigma_1$ is not part of the prefix $\Sigma$, by properness of $\mathcal{P}
\extendMuTT{} \mathcal{P}_1$, $s \notin \sorts$ so $s \notin \sorts_2$ and the
signatures $\Sigma\Sigma'_1$ and $\Sigma_2\Sigma'_1$ introduce the same
constants in the universe $\univ{s}$. Therefore, if $\progress{\Inert{d},d,\RewRules{d}}$
holds for $\Inert{d}$ computed in $\Sigma\Sigma'_1$
it also holds for $\Inert{d}$ computed in $\Sigma_2\Sigma'_1$.

The other conditions to show that $(d,\RewRules{d})$ is well formed in
$\Sigma_2\Sigma'_1$ hold by functoriality of typing judgments, preservation of
isolation and independence with respect to the signature for
$\determine{\RewRules{d}}$ thus concluding the inductive step.

By construction, we have both $(\sorts_2,\Sigma_2) \extendMuTT{}
(\sorts_{\cup}, \Sigma_{\cup})$ and $(\sorts_1,\Sigma_1) \extendMuTT{}
(\sorts_{\cup}, \Sigma_{\cup})$.

As a crude
application of <ref>, we can combine almost disjoint
parametrizations that agree on the sort $\Type$:

If $\mathcal{P}_1 = (\sorts_1,\Sigma_\Type\Sigma_1)$
and $\mathcal{P}_2 = (\sorts_2, \Sigma_\Type\Sigma_2)$ are
parametrization that only share $\sorts_1 \cap \sorts_2 = \{\Type\}$, and
agree on a common signature $(\{\Type\}, \Sigma_\Type)$, then $(\sorts_1\cup
\sorts_2,  \Sigma_\Type\Sigma_1\Sigma_2)$ is a valid

In other words, combined with the metatheoretical results presented in
<ref>, this corollary shows that addresses
the logical modularity issue depicted in the introduction of this

Combining two valid parametrizations yields to a consistent type
theory, even if the logical principles provided in those theories
are not compatible altogether.

This logical frontier has been achieved by the multiverse setting that
allows to localize in a sort the use of new logical principles, and
also the use of their consequences, which may not even mention
explicitly those new principles.

§ METATHEORY OF

In this section, we show the metatheoretical properties of claimed in
<ref> by adapting and extending the mechanized logical relation proof
of <cit.>.

The high-level idea of the proof is standard: we carefully define a logical
relation exhibiting for each derivable judgments of  a canonical standard
shape for its derivation, show that the resulting logical relation satisfies a
variety of properties then prove the fundamental lemma by induction on typing

Finally we derive the actual metatheoretical properties as consequences of the
fundamental lemma.

§.§ Logical relation

$\LRctx{\Gamma}{\Delta}$     $\Delta$ is a reducible telescope on top of $\Gamma$ with respect to signature $\Sigma$

$\LRsub{\Gamma}{\sigma}{\Delta}{[\Delta]}$     $\sigma$ is a reducible substitution to the extension $\LRarg{[\Delta]} : \LRctx{\Gamma}{\Delta}$

$\LRty{\Gamma}{A}{s}$    $A$ is a reducible type at sort $s \in \sorts$ in context $\Gamma$

$\LRtm{\Gamma}{t}{A}{s}{[A]}$    $t$ is a reducible term of reducible type $\LRarg{[A]} : \LRty{\Gamma}{A}{s}$

$\LRconvty{\Gamma}{A}{B}{s}{[A]}$    $B$ is convertible to the reducible type $\LRarg{[A]} : \LRty{\Gamma}{A}{s}$

$\LRconvtm{\Gamma}{t}{u}{A}{s}{[A]}$    $t$ and $u$ are convertible at reducible type $\LRarg{[A]} : \LRty{\Gamma}{A}{s}$

$\LRneutraltm{\Gamma}{t}{A}{s}$     $t$ is a reducible neutral term of type $A$

Components of the logical relation for

The logical relation defines families of types, the reducibility
relations $\Vdash$ described in <ref>, corresponding to
each judgment of  (<ref>).

The definition of these relation proceed first by induction on the well-formed
signature $\Sigma$, collecting inductively proof of reducibility data employed
to define the reducibility relation at types introduced by inert constants $K$

We use the notation $\LRarg{[x]}$ for the proof of reducibility associated to a
type, term, context or substitution $x$.

We abuse application notation $\LRarg{[A]~[t]}$ to substitute a reducibility proof $[t]
: \LRtm{\Gamma}{t}{X}{s}{[X]}$ in $\LRarg{[A]} : \Sigma; \Gamma,
\oftype{x}{X}{s} \Vdash \mathcal{J}$, omitting the required substitutions and
providing only the main arguments.

A positive type constant $(K, \Inert{K})$ is reducible in signature $\Sigma$ if

* its parameters are reducible $\LRarg{[\params{K}]} : \LRctx{\emptyContext}{\params{K}}$

* for each inert constant $c \in \Inert{K}$, $\cod{c} =
K(\overline{u})$, $\params{c}$, $\dom{c}$ and $\overline{u}$ are reducible

[c] : c
[u] : cuK[K]
∀i, c_i = K(t) ∧[c_i] : ctK[K]

A negative type constant $(K, \Active{K})$ is reducible in signature $\Sigma$ if

* its parameters are reducible $\LRarg{[\params{K}]} : \LRctx{\emptyContext}{\params{K}}$

* for each active constant $d_i \in \Active{K} = \overline{d}$, , $\cod{d_i}$ is reducible

\[
\begin{dcases*}
\enspace
\LRarg{[\cod{d_i}]} : \LRsub{\params{K}, \overline{\cod{d}}_{<i}}{\overline{t}}{\params{K}}{[\params{K}]}
& if $\cod{d_i} = K(\overline{t})$ \\[0.1cm]
\enspace
\LRarg{[\cod{d_i}]} : \LRty{\params{d},  \overline{\cod{d}}_{<i}}{\cod{d_i}}{\codsort{d_i}}
& otherwise
\end{dcases*}
\]

A rewrite rule
$\rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r}$ is
reducible in signature $\Sigma$ if its contexts, substitutions and
right hand side are reducible:

[Δ] : Δ
[Δ_] : Δ_
Δ, dpat[σ]rd[x, pat][σ]d[d] …

Assuming by induction hypothesis that we have the reducibility datum $\LRarg{[\Sigma]}$
corresponding to a well-formed signature $\Sigma$, we can now describe the
defining cases of the logical relation.

In all cases, the general methodology is to first reduce the subject of the
judgment to a whnf, and then characterize the canonical forms at each type and

The definition is complicated by two aspects exposed in <cit.>: first,
universes introduce a seemingly circular definition of reducibility at terms and
types; second, negative occurrences of the reducibility relation appears in the
definition, e.g. for reducibility of terms at dependent products.

The circularity induced by universes actually disappears once we take into
account the (implicit) universe levels.

The problem induced by negative occurrences is solved by defining inductively the
reducibility relation on types, and then defining the other relations by
recursion on the proofs of reducibility on types.

Since the definition of all these relations are mutual, we obtain a
well-founded albeit complex inductive recursive definition.

<Ref> describes the inductive part of reducibility of types with
a case for universes of each sorts, neutral types, $\Pi$-types that use the
context reducibility from <ref> and constant introduced from
the signature $\Sigma$.

<Ref> then dispatches reducibility of terms to auxiliaries
definitions according to the reducibility proof of its type.

We omit most of these auxiliary definitions, focusing on the components proper to
and absent from <cit.>.

<Ref> describes the reducibility of terms at types introduced
with a constant $K$ drawn from the signature $\Sigma$.

The rule infrule:constant-reducible is the entry point and closes the
other judgments by weak head reduction, while the other

rules apply depending on the positive or negative character
of the type $K$ as described by the signature $\Sigma$.

When $(K,\Inert{K})$ is a positive type constant according to $\Sigma$, a whnf
is reducible at $K(\overline{a})$, if it is neutral using
infrule:neutral-reducible, or if it consists of an inert constant $c
\in \Inert{K}$, one of the canonical introduction form of $K$, its parameters
and recursive arguments are inductively reducible and the arguments of $K$ computed from its
parameters are convertible to $\overline{a}$, using rule

When $(K, \Active{K})$ is a negative type constant according to $\Sigma$, a whnf
$t$ is reducible at $K(\overline{a})$, rule
infrule:inert-constant-negative-reducible, if all its possible
observations $d(\overline{a},t)$ for $d \in \Active{K}$ are
coinductively reducible at their corresponding type.

In both of these cases, the definitions make a crucial use of the reducibility
data $\LRarg{[\Sigma]}$ obtained by induction hypothesis on $\Sigma$.

The so-defined logical relation verifies a handful of properties:

* it is stable under weakening, substitution by reducible substitution;

* the relations induced by conversion are reflexive, symmetric, transitive
and congruent with respect to all type and term formers;

* all reducibility relations are stable by judgmental conversion;

* a reducible type or term reduces to a whnf that is itself reducible;

* reducibility is closed by anti-reduction;

* well-typed neutrals are reducible.

We highlight two key properties: the reducibility relations are irrelevant,
so that being reducible is a mere property; and all judgments satisfy the so
called escape lemma that allows to recover derivability of a  judgment
out of its reducible counterpart.

If $\LRarg{[A]}, \LRarg{[A']} : \LRty{\Gamma}{A}{s}$ are two proofs of
reducibility of the type $A$, $\LRtm{\Gamma}{t}{A}{s}{[A]} \Rightarrow
\LRtm{\Gamma}{t}{A}{s}{[A']}$.

The key property of  needed to prove irrelevance of the reducibility witnesses
is the determinism of rewrite rules, ensuring uniqueness of the head of a weak head normal form.

For any judgment form $\mathcal{J}$ of , if $\Sigma ; \Gamma \Vdash
\mathcal{J}$ then $\Sigma ; \Gamma \vdash \mathcal{J}$.

The escape lemma reconstructs a canonical derivation of a judgment out of a
reducibility proof.

Irrelevance is used pervasively to “realign” reducibility judgments that only
differ in the reducibility proof.

$\LRctx{\Gamma}{\Delta}$ reducibility of telescopes.

[Δ] : ΓΔ

Γ, Δ[Δ]As

ΓΔ, xAs

\[
\begin{array}{rcr}
\LRty{\Gamma{}, \LRpair{\Delta}{[\Delta]}}{A}{s} &\eqbydef&
\forall \Gamma{}' \supseteq \Gamma{},\enspace
\LRsub{\Gamma{}'}{\sigma{}}{\Delta{}}{[\Delta{}]}\to
(\LRarg{[A\sigma]} : \LRty{\Gamma{}'}{A[\sigma]}{s} \enspace \wedge\\
\enspace{}\LRconvtm{\Gamma{}'}{\sigma{}}{\sigma{}'}{\Delta{}}{}{[\Delta{}]}\to\\
\Delta \supseteq \Gamma&\eqbydef & \exists \rho, \Delta \vdash \rho \Gamma
\wedge \rho \text{ is a monotone renaming}\hfill{}

\end{array}
\]

$\LRsub{\Gamma}{\sigma}{\Delta}{[\Delta]}$ reducibility of substitutions.

[σ] :ΓσΔ[Δ]

ΓtA[σ]s([A] id_Γ [σ]).1
Γ(σ, t)Δ, xAs[Δ], [A]

Reducibility of context and substitutions

s : ΓA

: ΓAs
ΓA(xXs_1) Ys_2

Γ, xXs_1Ys_2

Γ(xXs_1) Y(xXs_1) Ys_2

K ∈Σ

Reducibility for types

\[
\begin{array}{lcl}
\LRtm{\Gamma{}}{t}{A}{\Type{}}{\LRRedTyUniv{s}}
& \LRty{\Gamma}{t}{s}\qquad \text{\color{gray} (universe level decreases)}\\
\LRtm{\Gamma{}}{t}{A}{s}{\LRRedTyNe{}}
& \LRneutraltm{\Gamma}{t}{A}{s} \\
\LRtm{\Gamma{}}{t}{A}{s}{\LRRedTyPi~\ldots}
& \text{(omitted)} \\
\LRtm{\Gamma{}}{t}{A}{s}{\LRRedTyK{}~K~\overline{a}~\ldots}
& \LRredK{\Gamma}{t}{K(\overline{a})}{s}
\end{array}
\]

Reducibility for terms

[Neutral-Reducible]ΓnK(a)s ΓnK(a)s
(K, K) ∈Σ

c ∈K

∀i, [v_i] : Γv_ic_i[p]s

c = K(u_c)
(K, K) ∈Σ,K = d

[d]_i :Γd_i(a, t)K(t[a,d(a,t)_<i])s
if $\cod{d_i} = K(\overline{t})$

[d]_i :Γd_i(a,t)d_i[a,d(a,t)_<i]d_i[d_i] [a] [d]_<i

Reducibility of terms at constant types

§.§ Fundamental lemma

At a high level, the fundamental lemma states that derivable judgments are

More precisely, it consists of a family of lemmas for each judgments of
Let $\Sigma$ be a well-formed

* If $\Jctx{\Gamma}$ then $\LRctx{\Gamma}$;

* If $\Jty{\Gamma}{A}{s}$ then there is a proof $\LRarg{[A]} : \LRty{\Gamma}{A}{s}$;

* If $\Jtm{\Gamma}{t}{A}{s}$ then $\LRtm{\Gamma}{t}{A}{s}{[A]}$

* If $\Jconvty{\Gamma}{A}{B}{s}$ then $\LRconvty{\Gamma}{A}{B}{s}{[A]}$

* If $\Jconvtm{\Gamma}{t}{u}{A}{s}$ then $\LRconvtm{\Gamma}{t}{u}{A}{s}{[A]}$

The proof of the fundamental lemma proceed by induction on the typing
derivation, generalizing the result to be proved by uniformly closing
reducibility under substitution and extensionality (see the definition of
$\LRty{\Gamma{}, \LRpair{\Delta}{[\Delta]}}{A}{s}$ in <ref>)
and proving the result mutually for all judgments.

The case of reducibility of universes, constant types, introduction of inert
constants for positive types and introduction of active constants for negative
types are mostly straightforward: we organized the logical relation so that
there is already a case available for these forms.

The challenging and interesting cases are thus the dual ones that are not
explicitly mentioned in the logical relation: the introduction of
active constants for positive types and universes and the introduction of inert
constants for negative types.

We sketch the proof for the first case, highlighting some required properties of
participating to its  design.

Consider a typing derivation ending with the rule infrule:active-term,
with conclusion
$\Jtm{\Gamma}{d(\overline{t},u)}{\cod{d}[\overline{t},u]}{\codsort{d}}$ where
$\cod{d} = K(\overline{u_d})$ and $(K, \Inert{K})$ is a positive type according
to $\Sigma$.

By induction hypothesis, we have that $d \in \Sigma$, so that the parameters,
domain and codomain of $d$ are reducible and

\begin{align*}
\LRarg{[\overline{t}]} &: \LRsub{\Gamma}{\overline{t}}{\params{d}}{[\params{d}]},&
\LRarg{[u]} &: \LRtm{\Gamma}{u}{\dom{d}[\overline{t}]}{\domsort{d}}{[\dom{d}]~[\overline{t}]}
\end{align*}

Since $u$ is reducible, it reduces to a weak head normal form $w$, reducible at
the same type, that is $\LRarg{[w]}

By anti-reduction, it is enough to show that $\acst{d}{\overline{t}}{w}$ is
reducible, which we do by induction on $[w]$, generalizing over the reducible
parameters $\overline{t}$.

By inversion, $\LRarg{[w]}$ is necessarily produced with an instance
of infrule:constant-reducible, and is either a neutral or of the shape
$w = c(\overline{p},\overline{v})$ for $c \in \Inert{K}$ (by infrule:inert-constant-positive-reducible).

If $w$ is neutral or $\neg\react{d}{c}$ holds, then $\acst{d}{\overline{t}}{w}$ is
neutral, can be shown to be well-typed using the escape lemma, so it is

Otherwise, $\react{d}{c}$ ensures that there exist a rewrite rule
$\rewrule{\Delta}{\sigma}{\Delta_{\lin{}}}{d}{\overline{x}}{pat}{r} \in
\RewRules{}$ such that $\acst{d}{\overline{x}}{pat}$ unifies with
$\acst{d}{\overline{t}}{w}$ thanks to linearity, yielding a reducible
substitution $\LRsub{\Gamma}{\rho}{\Delta_\lin}{[\Delta_{\lin}]}$.

Using the premise of infrule:inert-constant-positive-reducible
obtained from $[w]$, we have that $w = c(\overline{p}, \overline{v})$, $\cod{c}
= K(\overline{u_c})$ and

By linearizability of the rewrite rule (<ref>), we obtain a
renaming $\tau$ that is an inverse of $\sigma$ up to conversion.

The composed substitution $\tau[\rho]$ is reducible,
$\LRsub{\Gamma}{\nu[\rho]}{\Delta}{[\Gamma]}{[\Delta]}$,  because $\rho$ is
reducible and $\tau$ is a renaming.

By substitution into the reducibility proof of the right hand side $r$ obtained
from the reducibility of the signature $[\Sigma]$ together with the induction
hypothesis on $\LRarg{[w]}$ for recursive occurrences from the pattern, we have
that $r[\tau[\rho], \occrecsub{d}{pat}[\tau[\rho]]]$ is reducible at type

\[\cod{d}[\overline{x}, \erasepat{pat}][\sigma{}][\tau[\rho]] \enspace\conv\enspace
\cod{d}[\overline{x},\erasepat{pat}][\rho] \enspace\conv\enspace \cod{d}[\overline{t},u].\]

Finally, by anti-reduction $\acst{d}{\overline{t}}{w}$ is reducible at the adequate type.

The case of an eliminator over a universe follows the same pattern, the
main modification being the organisation of the inductive hypothesis coming from
the signature.

For the case of a builder of negative type, the general case builds a
reducibility proof now by coinduction.

§.§ Consequences

Using the fundamental lemma and the definition of the logical relation on
positive inert types, we obtain as a direct consequence that any term
$\Jtm{\emptyContext}{t}{K(\overline{u})}{\Type{}}$ of positive type is convertible to
an inert constant introducing $K$ or a neutral term.

The following lemma ensures that there is no neutral term in $\Type$, so
<ref> and its immediate corollary <ref> follow.

Closed neutrals belong to isolated sorts:

\[
\Jtm{\emptyContext}{n}{A}{s} \wedge \neutral{n} \implies \isolated{s} \vee (A = \univ{s'} \wedge \isolated{s'})
\]

The proof proceed by induction on the neutrality of $n$.

The variable case is impossible since the context is empty, and the application
case $n = n'~t$ proceed by induction on $n'$ using inversions on the typing
derivation to show that $n'$ is typed with a $\Pi$ type in the empty context,
at the same sort $s$ as $n$, hence $s$ is isolated.

The important case $n = \acst{d}{\overline{p}}{w}$ consider two cases depending on the
neutrality of $w$.

If $w$ is not neutral, $d \in \Sigma$ does not satisfy progress, so its
codomain must satisfy the conclusion of the lemma.

If $w$ is neutral, it is again well-typed in an empty context by inversion on
the typing derivation, so the type of $w$ satisfies the conclusion of the lemma by
induction hypothesis, and we conclude because the active constant $d \in \Sigma$
must preserve isolation.

Decidability of conversion is proven by defining an algorithmic
version of the conversion of two terms $t$ and $u$ which basically
amounts to computing the whnf of $t$ and $u$, compare their head, and
apply the algorithm recursively if necessary.

Correctness of algorithmic conversion is easy as the rules used are
particular cases of typed conversion (<ref>).

Then, it is shown that this algorithmic conversion is also complete by
replaying <ref> with a definition of the
logical relation using algorithmic conversion instead of typed

Actually, the formalization of <cit.> factorizes the two
proofs of the fundamental lemma by defining an abstract interface to both
algorithmic conversion and typed conversion and use this interface
in  the definition of the logical relation instead.

Then, to get decidability of type checking, we can simply rely on the
work of <cit.> on bidirectional type-checking,
which defines an algorithmic version of type-checking provided
that the theory enjoys subject reduction and decidability of conversion.

§ EXTENSIONALITY

Our parametrization of in <ref> only
allows us to extend conversion through the introduction of new rewrite

However, some extensions of conversion such as extensionality principles
are inherently undirected and cannot be specified with reduction rules,
but must directly extend conversion.

In this section, we do not provide a generic mechanism to enrich conversion with
extensionality principles, a challenging goal that we leave for future work,
but we remark that the logical relation naturally justifies them on two
compelling examples.

Primitive projections

The definition of negative dependent sum in <ref> (and
more generally, any record type) can be equipped with the following
extensionality principle:

\begin{align*}
\inferrule{\Jtm{\Gamma}{t}{\SigmaName~A~B}{\Type}}{\Jconvtm{\Gamma}
{\pairName ( A , B , \fstName (A , B,  t) , \sndName ( A , B ,  t))} {t}{\SigmaName~A~B}{\Type} }
\end{align*}

This conversion rule can be added to the system by postulating it when
$t$ is neutral.

The logical relation framework then straightforwardly shows that the
conversion is valid on any term, as any term of type $ \SigmaName~A~B$
reduces to a whnf which is either a $\pairName$, in which case the equality
holds by computation of  $\fstName$ and $\sndName$; or it is a neutral
term, in which case the equality holds with the new conversion rule.

Then, it suffices to remark that algorithmic conversion can also be
extended with this new conversion rule on neutral terms without
compromising decidability.

Strict Propositions

<cit.> propose the introduction of a new sort  of
strict propositions to [<https://agda.readthedocs.io/en/v2.6.0/language/prop.html>]
and [Since 8.10: <https://coq.inria.fr/doc/addendum/sprop.html>].

The characteristic feature of  is its definitional proof irrelevance,
e.g. any two inhabitants $p,q$ of a type $P$ in  are convertible:

\begin{align*}
\label{eq:sprop-definitional-pi}
\inferrule{\Jtm{\Gamma}{p}{P}{\SProp}\\\Jtm{\Gamma}{q}{P}{\SProp}}{\Jconvtm{\Gamma}{p}{q}{P}{\SProp}}
\end{align*}

As explained by <cit.>, to encode such a sort of strict
proposition in , it is enough to introduce a new sort  with a
single empty inductive type $\Jty{}{\bot}{\SProp}$ and its eliminator to
$\Type{}$, together with a conversion rule equating any two neutral terms at
this type.

§ RELATED WORK

Extending type theories
Pure Type Systems (PTS) <cit.> is a general framework for defining type
theories based on $\lambda$-calculus extended with additional sort constants.

Metatheoretical results such as consistency, subject reduction and normalisation
have been established for classes of PTS and their extensions, for instance with
cumulativity  <cit.> but the computational content is usually entirely
defined from $\beta$-reduction.

<cit.> extend conversion with a fixed set of additional equations
between neutral terms for a simply typed language, with type theory left as a
future work goal.

Their work use a similar methodology with a logical relation to show that
conversion can be reduced to a standard reduction path.

<cit.> propose a type theory with a generic scheme to define inductive
and coinductive types uniformly.

develops beyond their treatment in two orthogonal directions, supporting
universes and allowing types that are not necessarily inductive or coinductive.

Rewriting in type theory

Our setting to define rewrite rules is based on the recent work of
<cit.> but combining rewrite systems and type systems stems
from the work of <cit.>, extending simply typed
lambda-calculus with higher-order rewrite rules.

This framework was later taken to dependent type theory by <cit.>.

They extend the Calculus of Constructions with first- and
higher-order rewrite rules, provided the higher-order rules do not
introduce any critical pairs.

<cit.> prove subject reduction
for another variant of the Calculus of Constructions with a more
general notion of higher-order rewrite rules

completeness and consistency of this
system has been studied in <cit.>.

The Calculus of Algebraic Constructions <cit.> is another
extension of the Calculus of Constructions with a restricted form of
higher-order rewrite rules. It also provides criteria for checking
subject reduction and strong normalization.

All those work serves as the base to our present work, and we do not
claim any originality with respect to our termination criteria which
is basically enforced by typing conditions in the definition of a well-formed signature (<ref>).

Modal type theories

Modalities have recently gained traction to extend type theory in a variety of
directions <cit.>, supporting
the addition of new logical principles and constraints on the structure of type
theoretical judgments.

In order to accommodate the zoo of modalities required for different
applications, general frameworks parametrized by a $2$-category of modes have
been proposed, first in a simply typed setting <cit.>, and gradually
being adapted to a dependent setting

Modalities, in particular non-lex comonads that modify the action of
substitutions, encompass a wider setting than what we present in this work at
the cost of a more complex metatheory.

To this day, beyond state-of-the-art experiments, no proof assistant
implementation support parametrized modalities.

Our approach assumes standard context management and substitution propagation so
should be more readily compatible with existing mainstream proof assistant such
as Coq or Agda for an implementation.

Logical relations, type theory and categorical models
Since Plotkin's seminal work <cit.>, logical relations have been used
pervasively to prove metatheoretical properties of programming languages and
type theory <cit.>.

A categorical perspective on these techniques have been developed over the last
decades <cit.>,
providing efficient but rarely effective methods to prove normalization.

<cit.> apply these techniques to dependent type type theory, while
<cit.> uses a so-called reduction-free variant of logical

<cit.> provide the first mechanization of logical relations to prove
decidability of type checking of type theory in itself, on which we build.

Such mechanized developments remain to date a difficult task as
witnessed by the recent POPLMark reloaded challenge <cit.>.

§ CONCLUSION

We have presented a generic multiverse type theory in which multiple,
possibly incompatible type universes can safely cohabit without endangering its
meta-theoretical properties.

This new sort system provides a type-theoretic mechanism to separate
incompatible computational or logical features, which can further be used to
mediate between universes, using specific new constants that make bridges
between universes.

Beyond the simple instances that we present here, we expect that many models of
<cit.> have interesting presentations in  capturing their
computational behaviour.

Parametrized extensions of conversion as presented in <ref>
is an important future milestone to that endeavour.

A natural next step is to make the theory sort-polymorphic, so that
sort-agnostic definitions can be shared more easily between universes, extending
the existing universe-level polymorphism that is implemented in today's proof
assistants <cit.>.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abel, Aehlig, and DybjerAbel
et al2007]
authorpersonAndreas Abel, personKlaus
Aehlig, and personPeter Dybjer.
Normalization by Evaluation for Martin-Löf
Type Theory with One Universe. In booktitleProceedings of
the 23rd Conference on the Mathematical Foundations of Programming Semantics,
MFPS 2007, New Orleans, LA, USA, April 11-14, 2007
(seriesElectronic Notes in Theoretical Computer Science,
Vol. volume173), editorpersonMarcelo
Fiore (Ed.). publisherElsevier, pages17–39.

[Abel, Allais, Hameer, Pientka, Momigliano,
Schäfer, and StarkAbel et al2019]
authorpersonAndreas Abel, personGuillaume
Allais, personAliya Hameer, personBrigitte Pientka,
personAlberto Momigliano, personSteven Schäfer,
and personKathrin Stark. year2019.
POPLMark reloaded: Mechanizing proofs by logical
journalJ. Funct. Program.  volume29
(year2019), pagese19.

[Abel, Pientka, Thibodeau, and SetzerAbel
et al2013]
authorpersonAndreas Abel, personBrigitte
Pientka, personDavid Thibodeau, and personAnton
Setzer. year2013.
Copatterns: programming infinite structures by
observations. In booktitleThe 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
'13, Rome, Italy - January 23 - 25, 2013,
editorpersonRoberto Giacobazzi and
personRadhia Cousot (Eds.). publisherACM,

[Abel, Öhman, and VezzosiAbel
et al2018]
authorpersonAndreas Abel, personJoakim
Öhman, and personAndrea Vezzosi.
Decidability of conversion for type theory in type
journalProc. ACM Program. Lang.
volume2, numberPOPL (dateJan.
year2018), pages23:1–23:29.

[Allais, McBride, and BoutillierAllais
et al2013]
authorpersonGuillaume Allais, personConor
McBride, and personPierre Boutillier.
New equations for neutral terms: a sound and
complete decision procedure, formalized,
editorpersonStephanie Weirich (Ed.).
publisherACM Press, addressBoston, Massachusetts,
USA, pages13–24.

[Altenkirch, Boulier, Kaposi, and
TabareauAltenkirch et al2019]
authorpersonThorsten Altenkirch, personSimon
Boulier, personAmbrus Kaposi, and personNicolas
Tabareau. year2019.
Setoid Type Theory - A Syntactic Translation. In
booktitleMathematics of Program Construction - 13th
International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume11825), editorpersonGraham
Hutton (Ed.). publisherSpringer, pages155–196.

[Altenkirch, Capriotti, and KrausAltenkirch
et al2016]
authorpersonThorsten Altenkirch, personPaolo
Capriotti, and personNicolai Kraus.
Extending Homotopy Type Theory with Strict
journalComputer Science Logic

[Barbanera, Fernández, and GeuversBarbanera
et al1997]
authorpersonFranco Barbanera, personMaribel
Fernández, and personHerman Geuvers.
Modularity of Strong Normalization in the
journalJournal of Functional Programming
volume7, number6 (year1997),

[Barendregt, Dekkers, and StatmanBarendregt
et al2013]
authorpersonHendrik Pieter Barendregt,
personWil Dekkers, and personRichard Statman.
booktitleLambda Calculus with Types.
publisherCambridge University Press.

[Barthe and UustaluBarthe and
authorpersonGilles Barthe and personTarmo
Uustalu. year2002.
CPS Translating Inductive and Coinductive Types.
In booktitleProceedings of Partial Evaluation and
Semantics-based Program Manipulation (Portland, Oregon).
publisherACM, pages131–142.

[Basold and GeuversBasold and
authorpersonHenning Basold and
personHerman Geuvers. year2016.
Type Theory based on Dependent Inductive and
Coinductive Types, editorpersonMartin Grohe,
personEric Koskinen, and personNatarajan Shankar
(Eds.). publisherACM Press, addressNew York, NY, USA,

[Birkedal, Clouston, Mannaa, Møgelberg,
Pitts, and SpittersBirkedal et al2020]
authorpersonLars Birkedal, personRanald
Clouston, personBassel Mannaa, personRasmus Ejlers
Møgelberg, personAndrew M. Pitts, and personBas
Spitters. year2020.
Modal dependent type theory and dependent right
journalMath. Struct. Comput. Sci.
volume30, number2 (year2020),

authorpersonFrédéric Blanqui.
Definitions by rewriting in the Calculus of
journalMathematical Structures in Computer Science
volume15, number1 (year2005),

[Boulier, Pédrot, and TabareauBoulier
et al2017]
authorpersonSimon Boulier,
personPierre-Marie Pédrot, and personNicolas
Tabareau. year2017.
The next 700 syntactical models of type theory. In
booktitleProceedings of the 6th ACM SIGPLAN Conference
on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17,
2017. pages182–194.

authorpersonAdam Chlipala.
booktitleCertified Programming with Dependent
publisherMIT Press.

[Cockx, Tabareau, and WinterhalterCockx
et al2021]
authorpersonJesper Cockx, personNicolas
Tabareau, and personThéo Winterhalter.
The taming of the rew: a type theory with
computational assumptions.
journalProc. ACM Program. Lang.
volume5, numberPOPL (dateJan.
year2021), pages1–29.

authorpersonThierry Coquand.
Canonicity and normalization for dependent type
journalTheor. Comput. Sci.  volume777
(year2019), pages184–191.

authorpersonThierry Coquand.
Reduction Free Normalisation for a proof irrelevant
type of propositions.
journalCoRR  volumeabs/2103.04287

[Coquand and HuetCoquand and Huet1988]
authorpersonThierry Coquand and
personGérard Huet. year1988.
The Calculus of Constructions.
journalInformation and Computation
volume76, number2-3 (dateFeb.
year1988), pages95–120.

authorpersonMarcelo Fiore.
Semantic Analysis of Normalisation by Evaluation
for Typed Lambda Calculus. In booktitleProceedings of the
4th ACM SIGPLAN International Conference on Principles and Practice of
Declarative Programming (Pittsburgh, PA, USA) (seriesPPDP
'02). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages26–37.

[Gilbert, Cockx, Sozeau, and TabareauGilbert
et al2019]
authorpersonGaëtan Gilbert,
personJesper Cockx, personMatthieu Sozeau, and
personNicolas Tabareau. year2019.
Definitional proof-irrelevance without K.
journalProc. ACM Program. Lang.
volume3, numberPOPL (dateJan.
year2019), pages3:1–3:28.

authorpersonV. Glivenko.
Sur Quelques Points de la Logique de M.
journalBulletins de la classe des sciences
volume15 (year1929), pages183–188.

[Gratzer, Kavvos, Nuyts, and BirkedalGratzer
et al2020]
authorpersonDaniel Gratzer, personG. A.
Kavvos, personAndreas Nuyts, and personLars
Birkedal. year2020.
Multimodal Dependent Type Theory, See
lics2020, pages492–506.

[Gratzer, Sterling, and BirkedalGratzer
et al2019]
authorpersonDaniel Gratzer, personJonathan
Sterling, and personLars Birkedal.
Implementing a modal dependent type theory.
Seeicfp2019, pages107:1–107:29.

authorpersonHugo Herbelin.
On the Degeneracy of Sigma-Types in Presence of
Computational Classical Logic. In booktitleSeventh
International Conference, TLCA '05, Nara, Japan. April 2005, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume3461), editorpersonPawel
Urzyczyn (Ed.). publisherSpringer, pages209–220.

[Herbelin and SpiwackHerbelin and
authorpersonHugo Herbelin and personArnaud
Spiwack. year2013.
The Rooster and the Syntactic Bracket. In
booktitle19th International Conference on Types for Proofs
and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France
(seriesLIPIcs, Vol. volume26),
editorpersonRalph Matthes and
personAleksy Schubert (Eds.). publisherSchloss
Dagstuhl - Leibniz-Zentrum für Informatik, pages169–187.

[Hermanns, Zhang, Kobayashi, and
MillerHermanns et al2020]
editorpersonHolger Hermanns, personLijun
Zhang, personNaoki Kobayashi, and personDale
Miller (Eds.). year2020.
booktitleProceedings of the 35th ACM/IEEE
Symposium on Logic in Computer Science (LICS 2020).
publisherACM, addressSaarbrücken, Germany.

[ICFP 2019ICFP 20192019]
ICFP 2019 year2019.

authorpersonG. A. Kavvos.
Modalities, cohesion, and information flow.
journalProc. ACM Program. Lang.
volume3, numberPOPL (year2019),

authorpersonMeven Lennon-Bertrand.
Complete Bidirectional Typing for the Calculus of
Inductive Constructions. In booktitle12th International
Conference on Interactive Theorem Proving (ITP 2021)
(seriesLeibniz International Proceedings in Informatics
(LIPIcs), Vol. volume193),
editorpersonLiron Cohen and personCezary
Kaliszyk (Eds.). publisherSchloss Dagstuhl – Leibniz-Zentrum
für Informatik.

authorpersonPierre Letouzey.
titleProgrammation fonctionnelle certifiée –
L'extraction de programmes dans l'assistant Coq.
thesistypePh.D. Dissertation.
schoolUniversité Paris-Sud.

[Licata, Shulman, and RileyLicata
et al2017]
authorpersonDaniel R. Licata, personMichael
Shulman, and personMitchell Riley.
A Fibrational Framework for Substructural and Modal
Logics. In booktitle2nd International Conference on Formal
Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017,
Oxford, UK (seriesLIPIcs, Vol. volume84),
editorpersonDale Miller (Ed.).
publisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik,

authorpersonZhaohui Luo.
titleAn Extended Calculus of Constructions.
thesistypePh.D. Dissertation. schoolDepartment
of Computer Science, University of Edinburgh.

authorpersonPer Martin-Löf.
titleAn Intuitionistic Theory of Types.
Unpublished manuscript.

authorpersonPer Martin-Löf.
An intuitionistic theory of types: predicative
In booktitleLogic Colloquium '73, Proceedings of the
Logic Colloquium, editorpersonH.E. Rose and
personJ.C. Shepherdson (Eds.). seriesStudies in Logic
and the Foundations of Mathematics, Vol. volume80.
publisherNorth-Holland, pages73–118.

authorpersonPer Martin-Löf.
100 years of Zermelo's axiom of choice: what was
the problem with it?
journalComput. J. volume49,
number3 (year2006), pages345–350.

authorpersonConor McBride.
titleDependently Typed Functional Programs and their
thesistypePh.D. Dissertation. schoolUniversity
of Edinburgh.

authorpersonJohn C. Mitchell.
booktitleType Systems for Programming Languages.
publisherMIT Press, addressCambridge, MA,
USA, pages365–458.

[Mitchell and ScedrovMitchell and
authorpersonJohn C. Mitchell and
personAndre Scedrov. year1992.
Notes on Sconing and Relators. In
booktitleComputer Science Logic, 6th Workshop, CSL '92,
San Miniato, Italy, September 28 - October 2, 1992, Selected Papers
(seriesLecture Notes in Computer Science,
Vol. volume702), editorpersonEgon
Börger, personGerhard Jäger, personHans
Kleine Büning, personSimone Martini, and
personMichael M. Richter (Eds.). publisherSpringer,

authorpersonEugenio Moggi.
Notions of computation and monads.
journalInformation and Computation
volume93, number1 (dateJuly
year1991), pages55–92.

authorpersonUlf Norell.
Dependently Typed Programming in Agda. In
booktitleAdvanced Functional Programming (AFP 2008)
(seriesLecture Notes in Computer Science,
Vol. volume5832). publisherSpringer-Verlag,

[Nuyts and DevrieseNuyts and
authorpersonAndreas Nuyts and
personDominique Devriese. year2018.
Degrees of Relatedness: A Unified Framework for
Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and
Algebra in Dependent Type Theory. In booktitleProceedings
of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS
2018, Oxford, UK, July 09-12, 2018, editorpersonAnuj
Dawar and personErich Grädel (Eds.).
publisherACM, pages779–788.

authorpersonDavid Parnas.
On the criteria for decomposing systems into
journalCommun. ACM volume15,
number12 (dateDec. year1972),

authorpersonChristine Paulin-Mohring.
Inductive Definitions in the System Coq -
Rules and Properties. In booktitleTyped Lambda Calculi
and Applications, editorpersonMarc Bezem and
personJan Friso Groote (Eds.).

authorpersonChristine Paulin-Mohring.
Introduction to the Calculus of Inductive
In booktitleAll About Proofs, Proofs for All,
editorpersonBruno Woltzenlogel Paleo and
personDavid Delahaye (Eds.). publisherCollege

[Pédrot and TabareauPédrot and
authorpersonPierre-Marie Pédrot and
personNicolas Tabareau. year2020.
The fire triangle: how to mix substitution,
dependent elimination, and effects.
journalProceedings of the ACM on Programming
Languages volume4, numberPOPL (dateJan.
year2020), pages58:1–58:28.

[Pédrot, Tabareau, Fehrmann, and
TanterPédrot et al2019]
authorpersonPierre-Marie Pédrot,
personNicolas Tabareau, personHans Jacob Fehrmann,
and personÉric Tanter. year2019.
A Reasonably Exceptional Type Theory.
volume3, numberICFP, Article
articleno108 (dateJuly year2019),
numpages29 pages.

authorpersonGordon D. Plotkin.
titleLambda-definability and logical relations.

<https://www.cl.cam.ac.uk/ nk480/plotkin-logical-relations.pdf>

[Pédrot and TabareauPédrot and
authorpersonPierre-Marie Pédrot and
personNicolas Tabareau. year2018.
Failure is Not an Option - An Exceptional Type
Theory. In booktitleProceedings of the 27th European
Symposium on Programming Languages and Systems (ESOP 2018)
(seriesLecture Notes in Computer Science,
Vol. volume10801), editorpersonAmal
Ahmed (Ed.). publisherSpringer-Verlag,
addressThessaloniki, Greece, pages245–271.

[Rijke, Shulman, and SpittersRijke
et al2020]
authorpersonEgbert Rijke, personMichael
Shulman, and personBas Spitters.
Modalities in homotopy type theory.
journalLog. Methods Comput. Sci.
volume16, number1 (year2020).

[Schreiber and ShulmanSchreiber and
authorpersonUrs Schreiber and
personMichael Shulman. year2012.
Quantum Gauge Field Theory in Cohesive Homotopy
Type Theory. In booktitleProceedings 9th Workshop on
Quantum Physics and Logic, QPL 2012, Brussels, Belgium, 10-12 October
2012 (seriesEPTCS, Vol. volume158),
editorpersonRoss Duncan and
personPrakash Panangaden (Eds.). pages109–126.

authorpersonMichael Shulman.
Univalence for inverse diagrams and homotopy
journalMath. Struct. Comput. Sci.
volume25, number5 (year2015),

authorpersonMichael Shulman.
Brouwer's fixed-point theorem in real-cohesive
homotopy type theory.
journalMath. Struct. Comput. Sci.
volume28, number6 (year2018),

[Sozeau, Boulier, Forster, Tabareau, and
WinterhalterSozeau et al2020]
authorpersonMatthieu Sozeau, personSimon
Boulier, personYannick Forster, personNicolas
Tabareau, and personThéo Winterhalter.
Coq Coq correct! verification of type checking and
erasure for Coq, in Coq.
journalProc. ACM Program. Lang.
volume4, numberPOPL (year2020),

[Sozeau and TabareauSozeau and
authorpersonMatthieu Sozeau and
personNicolas Tabareau. year2014.
Universe Polymorphism in Coq. In
booktitleInteractive Theorem Proving,
editorpersonGerwin Klein and personRuben
Gamboa (Eds.). publisherSpringer International Publishing,
addressCham, pages499–514.

authorpersonJonathan Sterling.
titleAlgebraic Type Theory and Universe Hierarchies.

[Sterling and HarperSterling and
authorpersonJonathan Sterling and
personRobert Harper. year2020.
Logical Relations as Types: Proof-Relevant
Parametricity for Program Modules.
journalCoRR  volumeabs/2010.08599

[Sterling and SpittersSterling and
authorpersonJonathan Sterling and
personBas Spitters. year2018.
Normalization by gluing for free
\(\lambda\)-theories.
journalCoRR  volumeabs/1809.08646

[Swamy, Chen, and LivshitsSwamy
et al2013]
authorpersonNikhil Swamy, personJuan Chen,
and personBen Livshits. year2013.
Verifying Higher-order Programs with the Dijkstra
Monad. In booktitleACM Programming Language Design and
Implementation (PLDI) 2013.

authorpersonVal Tannen.
Combining Algebra and Higher-Order Types. In
booktitleProceedings, Third Annual Symposium on Logic in
Computer Science, 5-8 July 1988, Edinburgh, Scotland, UK.
publisherIEEE Computer Society, pages82–90.

[The Agda Development TeamThe Agda
Development Team2021]
authorpersonThe Agda Development Team.
titleUniverse Levels.

[The Coq Development TeamThe Coq
Development Team2020]
authorpersonThe Coq Development Team.
booktitleThe Coq proof assistant reference manual.

Version 8.12.

[Univalent Foundations ProgramUnivalent
Foundations Program2013]
authorpersonThe Univalent Foundations Program.
booktitleHomotopy Type Theory: Univalent Foundations
of Mathematics.
addressInstitute for Advanced Study.

[Vezzosi, Mörtberg, and AbelVezzosi
et al2019]
authorpersonAndrea Vezzosi, personAnders
Mörtberg, and personAndreas Abel.
Cubical Agda: A Dependently Typed Programming
Language with Univalence and Higher Inductive Types.

authorpersonVladimir Voevodsky.
booktitleA simple type system with two identity
publisherUnpublished notes,

authorpersonDaria Walukiewicz-Chrzaszcz.
Termination of rewriting in the Calculus of
journalJournal of Functional Programming
volume13, number2 (year2003),

[Walukiewicz-Chrzaszcz and
ChrzaszczWalukiewicz-Chrzaszcz and Chrzaszcz2006]
authorpersonDaria Walukiewicz-Chrzaszcz and
personJacek Chrzaszcz. year2006.
Consistency and Completeness of Rewriting in the
Calculus of Constructions. In booktitleAutomated Reasoning,
Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August
17-20, 2006, Proceedings (seriesLecture Notes in Computer
Science, Vol. volume4130),
editorpersonUlrich Furbach and
personNatarajan Shankar (Eds.). publisherSpringer,

[Whitehead and RussellWhitehead and
authorpersonAlfred North Whitehead and
personBertrand Russell. year1910.
booktitlePrincipia Mathematica.
publisherCambridge University Press,

§.§.§ Natural numbers

A standard positive type is that of natural numbers, which come with their
induction principle.

* $\params{\Nat} = \emptyContext{}$

* $\cod{\Nat} = \univ{\Type}_{0}$

* The constructors are $\Zero$ and $\Succ$:

* $\params{\Zero} = \dom{\Zero} = \emptyContext{}$, $\params{\Succ} = \emptyContext{}$, $\dom{\Succ} = \ctxvar{n}{\Nat}{\Type}$,

* $\cod{\Zero} = \cod{\Succ} = \Nat$

* The elimination principle is an active constants $\NatElim$ with:

\[\begin{array}{lcl}
\params{\NatElim} & = & \ctxvar{P}{\Nat → \univ{\Type}}{\Type}, \
\ctxvar{p0}{P~\Zero}{\Type}, \ \ctxvar{pS}{Π x : \Nat, P~x → P~(\Succ~x)}{\Type} \\
\dom{\NatElim} & = & \Nat \\
\cod{\NatElim} & = & P~n
\end{array}\]

* Ensuring progress we define the eliminator rewrite rules:

\[\begin{array}{l}
\rewtypinglin{.}{\overline{p} : \params{\NatElim}}{\NatElim}{\overline{p}}
{\Zero}{p0} \\
\rewtypinglin{.}{\overline{p} : \params{\NatElim}, \dom{\Succ} = \ctxvar{n}{\Nat}{\Type}}{\NatElim}{\overline{p}}
\end{array}\]

* The rewrite rules are obviously deterministic as they do not overlap.

§.§.§ Universes and -ing

Special modalities called -types allow to encapsulate a type in sort
$s$ into the  sort and are described in <ref>, as inference rules.

The $\BoxFull{s}{A}$ type constructor allows to encapsulate values of type $A$ in sort $s$ into
the $\Type{}$ sort. Its single constructor $\boxC_s(A,a)$ (abbreviated $\boxFull{s}{a}$) introduces a
value $a : A$ into the boxed type. Finally a constant $\cstface{boxelim}_{s_1, s_2}(A, B, t, u)$
(abbreviated as $\letbox{x}{t}{u}$, omitting type information) allows to eliminate a boxed value
in sort $s_1$ into a type in another sort $s_2$. This is essentially a rule schema that can be selectively
added when sorts $s_1$ embeds into sort $s_2$.

Placing all the universes in the sort , that is the $\BoxFull{s}{A}$ typing rule landing in $\Type$,
is the sole uniform choice capturing the examples that we want to consider.

Γ, ys_1ABs_2

Γ, xAs_1uBs_1xys_2

\begin{align}
\label{eq:box-red}
\letbox{x}{\boxFull{s_1}{z}}{u}\quad &\conv\quad u\subs{z}{x} \tag{$\beta_{\BoxInd}$}\\
\mathcolor{gray}{\letbox{x}{t}{C[\boxFull{s_1}{x}]}} \quad &\mathcolor{gray}{\conv\quad C[t]} \tag{$\eta_{\BoxInd}$}
\end{align}

Rules for -ing