# Stratified Type Theory

Jonathan Chan  0000-0003-0830-3180 University of PennsylvaniaPhiladelphiaUSA
<EMAIL_ADDRESS>and  Stephanie Weirich  0000-0002-6756-9168 University of
PennsylvaniaPhiladelphiaUSA<EMAIL_ADDRESS>
(2024)

###### Abstract.

To exploit the expressivity of being able to refer to the type of types, such
as for large elimination, dependent type systems will either employ a universe
hierarchy or else contend with an inconsistent type-in-type rule. However,
these are not be the only possible options. Taking inspiration from Stratified
System F, we introduce _Stratified Type Theory_ (StraTT), where rather than
stratifying universes by levels, we stratify typing judgements and restrict
the domain of dependent function types to some fixed level strictly lower than
that of the overall type. Even in the presence of type-in-type, this
restriction suffices to enforce consistency.

We explore the expressivity of several extensions atop this design. First, the
subsystem _subStraTT_ employs McBride’s crude-but-effective stratification
(also known as displacement) as a simple form of level polymorphism where top-
level definitions can be displaced uniformly to any higher level as needed,
which is valid due to cumulativity and plays well with stratified judgements.
Second, to recover some expressivity lost due to the restriction on dependent
function domains, the full StraTT system includes a separate nondependent
function type with _floating_ domains, whose level instead matches that of the
overall type. Finally, we have implemented a prototype type checker for StraTT
extended with datatypes along with a small type checked core library.

While the subsystem can be shown to be consistent, showing consistency for the
full system with floating nondependent functions remains an open problem.
Nevertheless, we believe that the full system is also consistent and have
mechanized a syntactic proof of subject reduction. Furthermore, we use our
implementation to investigate various well-known type-theoretic type-in-type
paradoxes. These examples all fail to type check in expected ways as evidence
towards consistency.

††journal: PACMPL††copyright: none††conference: Certified Programs and Proofs;
15 – 16 January 2024; London, United Kingdom††journalyear: 2024

##  1\. Introduction

Ever since their introduction in Martin-Löf’s intuitionistic type theory
(MLTT) (Martin-Löf, 1972), dependent type theories have included hierarchies
of type universes in order to rectify the inconsistency of the type-in-type
axiom. That is, rather than the universe $\star$ being its own type, these
type theories have universes $\star_{k}$ indexed by a sequence of levels $k$
such that the type of a universe is the universe at the next higher level.

Such a universe hierarchy is a rudimentary ingredient in many contemporary
proof assistants, such as Coq (Coq Development Team, 2022), Agda (Norell,
2007), Lean (de Moura et al., 2015), F* (Swamy et al., 2016), Arend (Clifton,
2015), and soon Idris 2 (Brady, 2011). For greater expressiveness, all of
these (except for Idris 2) also implement some sort of level polymorphism.
Supporting such generality means that the proof assistant must handle level
variable constraints, level expressions, or both. However, programming with
and especially debugging errors involving universe levels is a common pain
point among proof assistant users. So we ask: do all roads necessarily lead to
level polymorphism and more generally a universe hierarchy, or are there other
avenues to be taken?

To begin our exploration, let us take a look back at a different mechanism for
universe levels and revisit type polymorphism in System F (Girard, 1972;
Reynolds, 1974). Recall the formation rule for polymorphic type quantification
in System F, given below on the left. This rule is part of the judgement
$\Gamma\vdash A\mathrel{\mathsf{\bf type}}{}$, which asserts that the type
$\mathit{A}$ is well formed in context $\Gamma$. The quantification in this
rule is impredicative because the type $\forall x.B$ itself can be substituted
for $x$ in $B$, and it quantifies over all types including itself.

F-impredicative $\displaystyle\displaystyle{\hbox{\hskip
35.30383pt\vbox{\hbox{\hskip-35.30382pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x\mathrel{\mathsf{\bf
type}}{}\vdash B\mathrel{\mathsf{\bf type}}{}$}}}\vbox{}}}\over\hbox{\hskip
31.27599pt\vbox{\vbox{}\hbox{\hskip-31.27597pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\forall
x.B\mathrel{\mathsf{\bf type}}{}$}}}}}}$ F-stratified
$\displaystyle\displaystyle{\hbox{\hskip
63.57065pt\vbox{\hbox{\hskip-63.57063pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x\mathrel{\mathsf{\bf
type}}j\vdash B\mathrel{\mathsf{\bf type}}k$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
j<k$}}}}\vbox{}}}\over\hbox{\hskip
35.34975pt\vbox{\vbox{}\hbox{\hskip-35.34973pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\forall
x^{j}.B\mathrel{\mathsf{\bf type}}k$}}}}}}$

Impredicativity has long been a troublemaker in the metatheory of System F, in
particular the lack of a classical set-theoretic model (Reynolds, 1984). To
sidestep impredicativity, Leivant (Leivant, 1989) introduced _Stratified
System F_ , which stratifies types into different levels by disallowing
quantifying over types at the same level as the quantification itself. The
formation rule for polymorphic types in this system is shown in the above rule
on the right. This rule is part of the stratified type formation judgement,
written $\Gamma\vdash A\mathrel{\mathsf{\bf type}}k$, where $\mathit{k}$ is a
stratification level.

To extend stratified polymorphism to dependent types, there are two ways to
read this judgement. We could interpret $\Gamma\vdash A\mathrel{\mathsf{\bf
type}}k$ as a type $A$ living in some stratified type universe $\star_{k}$;
the generalization would then correspond to a usual predicative type theory
with a universe hierarchy where $\star_{j}:\star_{k}$ when $j<k$.
Alternatively, we could interpret the level $k$ as a property of the
_judgement_ rather than part of a type universe, and reëxpress the judgement
as $\Gamma\vdash\mathit{A}:^{\mathit{k}}\star$.

Since dependent types can depend on terms, we might generalize the stratified
type formation judgement to a stratified typing judgement
$\Gamma\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$, where variables
$\mathit{x}:^{\mathit{k}}\mathit{A}$ are also annotated with a level within
the context $\Gamma$, but using a type universe that doesn’t have a level
annotation. Guided by these principles, we introduce stratified dependent
function types
$\Pi\mathit{\mathit{x}}\\!:^{\mathit{k}}\\!\mathit{A}\mathpunct{.}\mathit{B}$
which similarly quantify over types at strictly lower levels.

To enable code reuse, rather than level polymorphism, we employ _crude but
effective stratification_ by McBride (2011). Following Hou et al.(2023)Hou
(Favonia), Angiuli, and Mullanix (Favonia), we refer to this as _displacement_
to prevent confusion. Given some signature $\Delta$ of global definitions, we
are permitted to use any definition with its levels displaced upwards. In the
context of StraTT, displacement enables functions with level-annotated types
to be used with arguments at any higher level.

However, even in the presence of displacement, we find that stratification is
sometimes _too_ restrictive and can rule out terms that are otherwise typeable
in an unstratified system. Therefore, StraTT includes a separate unstratified
nondependent function type with a _floating_ domain. StraTT is cumulative, so
all expressions inhabit the level at which they type check and at all higher
levels. However, in a dependent function type, the level of the domain type is
fixed even when the overall level of the type has been raised. In a floating,
nondependent type, level of the domain type floats to have the same level as
the overall type.

In the absence of floating nondependent functions, with only stratified
dependent functions, logical consistency holds even with type-in-type, because
the restriction on the domains of dependent functions prevents the kind of
self-referential trickery that enables the usual paradoxes. However, we have
not yet proven logical consistency with the addition of floating nondependent
functions. The covariant behaviour of the floating domain with respect to
levels is unusual for function types, and is the primary barrier to semantic
modelling. Even so, we have not found proof of inconsistency either, and our
attempts lead us to believe that consistency _does_ hold, making the system
suitable as a foundation for theorem proving.

These features form the basis of our Stratified Type Theory (StraTT). Our
contributions are as follows:

  * •

We first define subStraTT, a subsystem of StraTT, which features only
stratified dependent function types and displacement. We briefly sketch a
proof of consistency, modelling type universes with an inductive–recursive
definition in Agda. $\hookrightarrow$ Section 2

  * •

We then extend this subsystem to the full StraTT by adding nondependent
function types with floating domains, motivated through examples.
$\hookrightarrow$ 3

  * •

We have used the Coq proof assistant to prove important syntactic metatheorems
for StraTT, including subject reduction, which is nontrivial due to the level-
annotated context. $\hookrightarrow$ 4

  * •

We have developed a prototype implementation of a type checker, extending the
language to include datatypes. We use this implementation to demonstrate the
effectiveness of stratification and displacement in practical dependently-
typed programming, as well as its shortcomings when compared to prenex
universe polymorphism. $\hookrightarrow$ 5

  * •

As evidence towards logical consistency, we discuss how common type-theoretic
paradoxes, namely Hurkens’ paradox (Hurkens, 1995) and variants of Russell’s
paradox (Russell, 1903) and Burali-Forti’s paradox (Burali–Forti, 1897), fail
to type check. We briefly highlight the challenges in a consistency proof
attempt. $\hookrightarrow$ 6

7 discusses related work and we conclude in 8. Our Agda model, Coq metatheory,
and prototype implementation are available online at
https://github.com/plclub/StraTT. Where lemmas and theorems are first
introduced, we include a footnote indicating the corresponding source file and
lemma name in the development.

##  2\. A subsystem of Stratified Type Theory

In this section, we introduce subStraTT, a fragment of StraTT that does not
include the separate nondependent function types. As it’s a subsystem, the
main theorems of subject reduction and other lemmas in 4 proven for the full
StraTT still hold.

The subsystem subStraTT is a cumulative, extrinsic type theory with types à la
Russell, a single type universe, level-annotated dependent function types, an
empty type, and definitions with level displacement. The most significant
difference between subStraTT and other type theories with these features is
the annotation of the typing judgement with a level in place of universes in a
hierarchy. We use the naturals and their usual strict order and addition
operation for our levels, but they should be generalizable to any displacement
algebra (Hou et al.(2023)Hou (Favonia), Angiuli, and Mullanix, Favonia).

$\begin{array}[]{l l
r}\mathit{a},\mathit{b},\mathit{A},\mathit{B}&\Coloneqq&\mathit{(Syntax)}\\\
&\lx@intercol\mid\star\mid\mathit{x}\mid\mathit{\mathit{x}}^{\mathit{i}}\mid\Pi\mathit{\mathit{x}}\\!:^{\mathit{j}}\\!\mathit{A}\mathpunct{.}\mathit{B}\mid\lambda\mathit{\mathit{x}}\mathpunct{.}\mathit{b}\mid\mathit{b}\;\mathit{a}\mid\bot\mid\mathsf{absurd}(\mathit{b})\hfil\lx@intercol\end{array}$

  * $\Delta;\Gamma\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$ (_Typing_)

DT-Type $\displaystyle\displaystyle{\hbox{\hskip
13.12495pt\vbox{\hbox{\hskip-13.12495pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
21.825pt\vbox{\vbox{}\hbox{\hskip-21.825pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\star:^{\mathit{k}}\star$}}}}}}$
DT-Pi $\displaystyle\displaystyle{\hbox{\hskip
49.00012pt\vbox{\hbox{\hskip-22.45277pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{A}:^{\mathit{j}}\star$}}}\vbox{\hbox{\hskip-49.0001pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma,\mathit{x}:^{\mathit{j}}\mathit{A}\vdash\mathit{B}:^{\mathit{k}}\star$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{j}<\mathit{k}$}}}}\vbox{}}}}\over\hbox{\hskip
37.75002pt\vbox{\vbox{}\hbox{\hskip-37.75002pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\Pi\mathit{\mathit{x}}\\!:^{\mathit{j}}\\!\mathit{A}\mathpunct{.}\mathit{B}:^{\mathit{k}}\star$}}}}}}$
DT-AbsTy $\displaystyle\displaystyle{\hbox{\hskip
49.2779pt\vbox{\hbox{\hskip-22.45277pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{A}:^{\mathit{j}}\star$}}}\vbox{\hbox{\hskip-49.2779pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma,\mathit{x}:^{\mathit{j}}\mathit{A}\vdash\mathit{b}:^{\mathit{k}}\mathit{B}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{j}<\mathit{k}$}}}}\vbox{}}}}\over\hbox{\hskip
44.97227pt\vbox{\vbox{}\hbox{\hskip-44.97226pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\lambda\mathit{\mathit{x}}\mathpunct{.}\mathit{b}:^{\mathit{k}}\Pi\mathit{\mathit{x}}\\!:^{\mathit{j}}\\!\mathit{A}\mathpunct{.}\mathit{B}$}}}}}}$
DT-AppTy $\displaystyle\displaystyle{\hbox{\hskip
40.50838pt\vbox{\hbox{\hskip-36.63893pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{b}:^{\mathit{k}}\Pi\mathit{\mathit{x}}\\!:^{\mathit{j}}\\!\mathit{A}\mathpunct{.}\mathit{B}$}}}\vbox{\hbox{\hskip-40.50838pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{a}:^{\mathit{j}}\mathit{A}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{j}<\mathit{k}$}}}}\vbox{}}}}\over\hbox{\hskip
39.67224pt\vbox{\vbox{}\hbox{\hskip-39.67224pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{b}\;\mathit{a}:^{\mathit{k}}\mathit{B}\mathopen{\\{}\mathit{a}/\mathit{\mathit{x}}\mathclose{\\}}$}}}}}}$
DT-Var $\displaystyle\displaystyle{\hbox{\hskip
58.77223pt\vbox{\hbox{\hskip-58.77222pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}\\!:\\!^{\mathit{j}}\mathit{A}\in\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{j}\leq\mathit{k}$}}}}}\vbox{}}}\over\hbox{\hskip
23.2139pt\vbox{\vbox{}\hbox{\hskip-23.21388pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{\mathit{x}}:^{\mathit{k}}\mathit{A}$}}}}}}$
DT-Const $\displaystyle\displaystyle{\hbox{\hskip
56.45831pt\vbox{\hbox{\hskip-24.88333pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}\\!:\\!^{\mathit{j}}\mathit{A}\coloneqq\mathit{a}\in\Delta$}}}\vbox{\hbox{\hskip-56.45831pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Delta$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{i}+\mathit{j}\leq\mathit{k}$}}}}}\vbox{}}}}\over\hbox{\hskip
26.94724pt\vbox{\vbox{}\hbox{\hskip-26.94722pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{\mathit{x}}^{\mathit{i}}:^{\mathit{k}}\mathit{A}^{+\mathit{i}}$}}}}}}$
DT-Bottom $\displaystyle\displaystyle{\hbox{\hskip
13.12495pt\vbox{\hbox{\hskip-13.12495pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
23.2139pt\vbox{\vbox{}\hbox{\hskip-23.21388pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\bot:^{\mathit{k}}\star$}}}}}}$
DT-Absurd $\displaystyle\displaystyle{\hbox{\hskip
56.56668pt\vbox{\hbox{\hskip-56.56668pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{A}:^{\mathit{k}}\star$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{b}:^{\mathit{k}}\bot$}}}}\vbox{}}}\over\hbox{\hskip
43.39445pt\vbox{\vbox{}\hbox{\hskip-43.39445pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathsf{absurd}(\mathit{b}):^{\mathit{k}}\mathit{A}$}}}}}}$
DT-Conv $\displaystyle\displaystyle{\hbox{\hskip
52.65837pt\vbox{\hbox{\hskip-23.075pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$}}}\vbox{\hbox{\hskip-52.65836pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{B}:^{\mathit{k}}\star$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{A}\equiv\mathit{B}$}}}}\vbox{}}}}\over\hbox{\hskip
22.86667pt\vbox{\vbox{}\hbox{\hskip-22.86667pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{a}:^{\mathit{k}}\mathit{B}$}}}}}}$

Figure 1. Syntax and typing rules (subStraTT)

The typing judgement has the form
$\Delta;\Gamma\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$; its typing rules are
given in Figure 1. The judgement states that term $\mathit{a}$ is well typed
at level $\mathit{k}$ with type $\mathit{A}$ under the context $\Gamma$ and
signature $\Delta$. A signature consists of global definitions
$\mathit{x}:^{\mathit{k}}\mathit{A}\coloneqq\mathit{a}$, where each constant
$\mathit{x}$ is definitionally equal to its definition $\mathit{a}$. A context
consists of declarations $\mathit{x}:^{\mathit{k}}\mathit{A}$ of variables
$\mathit{x}$.

The type of the type universe $\star$ is itself at any level; in the next
section, we show how even with this rule, subStraTT can be proven consistent.
Stratification occurs at dependent function types in rule DT-Pi: one can only
quantify over types at strictly smaller levels, and the domain type must be
well typed at the same strictly smaller level. Similarly, in rule DT-AbsTy,
the body of a dependent function is well typed when its argument and its type
are well typed at a strictly smaller level, and by rule DT-AppTy, a dependent
function can only be applied to an argument of the strictly smaller level
indicated by the function’s type.

Rules DT-Bottom and DT-Absurd are the uninhabited type and its eliminator,
respectively. Although it should be consistent to eliminate a falsehood into
any level, including lower levels, we restrict it so that the premises have
the same level as the eliminator so that we can prove Lemma 4.0 (Regularity)..

In rules DT-Var and DT-Const, variables and constants at level $\mathit{j}$
can be used at any larger level $\mathit{k}$. This permits the following
admissible cumulativity rule,111coq/restrict.v:DTyping_cumul analogous to
having a cumulative universe hierarchy, allowing instead an entire derivation
to be used at a higher level.

$\displaystyle\displaystyle{\hbox{\hskip
40.50838pt\vbox{\hbox{\hskip-40.50838pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{a}:^{\mathit{j}}\mathit{A}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{j}\leq\mathit{k}$}}}}\vbox{}}}\over\hbox{\hskip
23.075pt\vbox{\vbox{}\hbox{\hskip-23.075pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$}}}}}}$

Constants are also annotated with a superscript indicating how much they’re
displaced by. If a constant $\mathit{x}$ is defined with a type $\mathit{A}$,
we’re permitted to use $\mathit{\mathit{x}}^{\mathit{i}}$ as an element of
type $\mathit{A}$ but with all of its levels incremented by $\mathit{i}$. The
metafunction $\mathit{a}^{+\mathit{i}}$ performs this increment in the term
$\mathit{a}$, defined recursively with
$(\Pi\mathit{\mathit{x}}\\!:^{\mathit{j}}\\!\mathit{A}\mathpunct{.}\mathit{B})^{+\mathit{i}}=\Pi\mathit{\mathit{x}}\\!:^{\mathit{i}+\mathit{j}}\\!\mathit{A}^{+\mathit{i}}\mathpunct{.}\mathit{B}^{+\mathit{i}}$
and
$(\mathit{\mathit{x}}^{\mathit{j}})^{+\mathit{i}}=\mathit{\mathit{x}}^{\mathit{i}+\mathit{j}}$.

The key formation rules for signatures $\vdash\Delta$ and contexts
$\Delta\vdash\Gamma$ are given below.

$\displaystyle\displaystyle{\hbox{\hskip
42.44997pt\vbox{\hbox{\hskip-42.44995pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Delta$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\varnothing\vdash\mathit{A}:^{\mathit{k}}\star$}}}}\vbox{\hbox{\hskip-22.45pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\varnothing\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$}}}\vbox{\hbox{\hskip-28.61104pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}\,\not\in\,\mathsf{dom}\,\Delta$}}}\vbox{}}}}}\over\hbox{\hskip
26.89444pt\vbox{\vbox{}\hbox{\hskip-26.89442pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Delta,\mathit{x}:^{\mathit{k}}\mathit{A}\coloneqq\mathit{a}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
46.19997pt\vbox{\hbox{\hskip-46.19997pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash\mathit{A}:^{\mathit{k}}\star$}}}}\vbox{\hbox{\hskip-27.56937pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}\,\not\in\,\mathsf{dom}\,\Gamma$}}}\vbox{\hbox{\hskip-28.61104pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}\,\not\in\,\mathsf{dom}\,\Delta$}}}\vbox{}}}}}\over\hbox{\hskip
23.21388pt\vbox{\vbox{}\hbox{\hskip-23.21387pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\Gamma,\mathit{x}:^{\mathit{k}}\mathit{A}$}}}}}}$

In rule DT-Conv, we use an untyped definitional equality
$\Delta\vdash\mathit{a}\equiv\mathit{b}$ that is reflexive, symmetric,
transitive, and congruent, and includes $\beta\eta$-equivalence for functions
and $\delta$-equivalence of constants $\mathit{x}$ with their definitions.
When a constant is displaced as $\mathit{\mathit{x}}^{\mathit{i}}$, we must
also increment the level annotations in their definitions by $\mathit{i}$.
Below are the rules for $\beta$-, $\eta$-, and $\delta$-equivalence; the
remaining rules can be found in A.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
46.80559pt\vbox{\vbox{}\hbox{\hskip-46.80559pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash(\lambda\mathit{\mathit{x}}\mathpunct{.}\mathit{b})\;\mathit{a}\equiv\mathit{b}\mathopen{\\{}\mathit{a}/\mathit{\mathit{x}}\mathclose{\\}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
30.41666pt\vbox{\vbox{}\hbox{\hskip-30.41664pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\lambda\mathit{\mathit{x}}\mathpunct{.}\mathit{b}\;\mathit{\mathit{x}}\equiv\mathit{b}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
25.50555pt\vbox{\hbox{\hskip-25.50555pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}\\!:\\!^{\mathit{k}}\mathit{A}\coloneqq\mathit{a}\in\Delta$}}}\vbox{}}}\over\hbox{\hskip
21.37224pt\vbox{\vbox{}\hbox{\hskip-21.37224pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{\mathit{x}}^{\mathit{i}}\equiv\mathit{a}^{+\mathit{i}}$}}}}}}$

Given a well-typed, locally-closed term
$\Delta;\varnothing\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$, the entire
derivation itself can be displaced upwards by some level increment
$\mathit{i}$. This lemma differs from cumulativity, since the level
annotations in the term and its type are raised as well, not just the level of
the judgement.

###### Lemma 2.0 (Displaceability (empty context)).

222coq/incr.v:DTyping_incr

If $\Delta;\varnothing\vdash\mathit{a}:^{\mathit{k}}\mathit{A}$ then
$\Delta;\varnothing\vdash\mathit{a}^{+\mathit{i}}:^{\mathit{i}+\mathit{k}}\mathit{A}^{+\mathit{i}}$.

With $\mathit{x}:^{\mathit{k}}\mathit{A}\coloneqq\mathit{a}$ in the signature,
$\mathit{\mathit{x}}^{\mathit{i}}$ is definitionally equal to
$\mathit{a}^{+\mathit{i}}$. Thus, this lemma justifies rule DT-Const, which
gives such displaced constants $\mathit{\mathit{x}}^{\mathit{i}}$ the type
$\mathit{A}^{+\mathit{i}}$.

###  2.1. Consistency proof sketch

We can show that subStraTT is a consistent type theory, _i.e._ that not all
types are inhabited. In this section, we sketch a model for subStraTT in Agda
through the framework of _categories with families_ (Dybjer, 1996), focussing
on how types are modelled.

Inspired by Kovács (2022), we use induction–recursion to model universes at
each level, relying on the well-foundedness of levels to ensure their well-
definedness. The elements of the inductive definition represent codes of the
types of subStraTT, while the recursive function interprets these codes as
types in Agda. Consistency follows from the interpretation of the empty type
in subStraTT as an empty type in Agda, and so is relative to the consistency
of Agda.

Because the interesting part of subStraTT when considering consistency is the
presence of type-in-type, here we only include the model for universes, and
omit constants and displacement, as well as the interpretation from subStraTT
into the model. We have made the Agda files containing the whole model
available at https://github.com/plclub/StraTT under the agda/ directory.

First, assume a type of `Level`s along with a well-founded order `_<_` on
them. The proof of well-foundedness `wf` has type ` $\forall$ (k : Level)
$\shortrightarrow$ Acc k`, where `Acc k` is the usual accessibility predicate
and `acc<` its constructor.333agda/Acc.agda

Now, the most direct way to model universes is as follows.444agda/direct-
model.agda

⬇

data U (k : Level) : Set

el : ∀ k → U k → Set

data U k where

Û : U k

⊥̂ : U k

Π̂ : ∀ j → j < k → (A : U j) →

(B : el j A → U k) → U k

el k Û = U k

el k ⊥̂ = ⊥

el k (Π̂ j j<k A B) = (x : el j A) → el k (B x)

The universe `U k` contains the code for itself `Û`, the code for the empty
type `⊥̂`, and the code for dependent functions `Π̂`, containing a strictly
smaller level `j`, the code for its domain at the smaller level, and a
function that produces a code for its codomain at the same level given an
element of the interpretation of the code of the domain. The interpretation
`el k` interprets each code as expected, though in contrast to usual
inductive–recursive models, the interpretation of `Û` in `U k` isn’t some
smaller `U j`, but rather `U k` itself.

Agda will reject this inductive–recursive definition for not being strictly
positive, because in the type of the `B` argument of `Π̂`, Agda thinks `U`
could appear in a negative position as the result of `el`. However, we know
that only a strictly smaller `U j` will be returned by virtue of well-
foundedness of the levels, so this definition is morally valid. To convince
Agda of this, we adapt the technique from Kovács (2022) and parametrize `U` by
`U<` and `el<`. These parameters represent universes at strictly smaller
levels and interpretation functions that can only be used on these strictly
smaller universes.

⬇

data U’ k (U< : ∀ {j} → j < k → Set)

(el< : ∀ {j} (j<k : j < k) → U< j<k → Set)

: Set

el’ : ∀ k (U< : ∀ {j} → j < k → Set)

(el< : ∀ {j} (j<k : j < k) → U< j<k → Set)

→ U’ k U< el< → Set

With this change, the `A` argument of `Π̂` has type

    U< j<k},
    while the \mintinline

agda—B— argument has type `el< j<k A  $\shortrightarrow$ U’ k U< el<`, no
longer violating strict positivity. We tie the knot by defining the top-level
`U<` and `el<` by induction over accessibility predicates on levels, then
finally instantiate the predicates by well-foundedness in `U` and `el`.

⬇

U< : ∀ {k} → Acc k → ∀ {j} → j < k → Set

el< : ∀ {k} (p : Acc k) {j} (j<k : j < k)

→ U< p j<k → Set

U< (acc< f) {j} j<k =

U’ j (U< (f j<k)) (el< (f j<k))

el< (acc< f) {j} j<k =

el’ j (U< (f j<k)) (el< (f j<k))

U : ∀ k → Set

U k = U’ k (U< (wf k)) (el< (wf k))

el : ∀ k → U k → Set

el k = el’ k (U< (wf k)) (el< (wf k))

To correctly model the cumulativity of subStraTT, we also need to show that
universes and codes are cumulative as well. More precisely, we prove that
given a code in `U j`, it can be lifted to a larger universe `U k`, and given
an element in the interpretation of the smaller code, we can produce an
element in the interpretation of the lifted code.

⬇

lift : ∀ {j k} → j < k → U j → U k

el→ : ∀ {j k} → (j<k : j < k) →

∀ u → el j u → el k (lift j<k u)

The proofs of these cumulativity lemmas are slightly involved due to having to
deal with accessibility proofs, which further requires assuming that `Acc k`
is a mere proposition. These proofs and the full definitions of `U’` and `el’`
can also be found in the Agda files.555agda/model.agda

##  3\. StraTT and floating functions

We have found that subStraTT alone is insufficiently expressive, with some
examples being unexpectedly untypeable and others being simply clunky to work
with. The full StraTT system therefore extends the subsystem with a separate
nondependent function type, written $\ottnt{A}\mathrel{\rightarrow}\ottnt{B}$,
that does not have the same level restriction on the domain as the dependent
function type.

(DT-Arrow?) (DT-AbsTm?) (DT-AppTm?)

Figure 2. Typing rules (nondependent functions)

The typing rules for nondependent function types, functions, and application
are given in 2. The domain, codomain, and entire nondependent function type
are all typed at the same level. Functions take arguments of the same level as
their bodies, and are applied to arguments of the same level. This distinction
between stratified dependent and unstratified nondependent functions
corresponds closely to Stratified System F: type polymorphism is syntactically
distinct from ordinary function types, and the former forces the codomain to
be a higher level while the latter doesn’t. From the perspective of Stratified
System F, StraTT merely generalizes stratified type polymorphism over types to
include term polymorphism. We say that the domain of these nondependent
function types _floats_ because unlike dependent function types, it isn’t
fixed to some particular level. The interaction between nondependent functions
and cumulativity is where this becomes interesting. Given a function
$\mathit{f}$ of type $\ottnt{A}\mathrel{\rightarrow}\ottnt{B}$ at level
$\ottnt{j}$, by cumulativity, it remains well typed with the same type at any
level $\ottnt{k}\geq\ottnt{j}$. The level of the domain floats up from
$\ottnt{j}$ to match the function at $\ottnt{k}$, in the sense that
$\mathit{f}$ can be applied to an argument of type $\ottnt{A}$ at any greater
level $\ottnt{k}$. This is unusual because the domain isn’t contravariant with
respect to the ordering on the levels as we might expect. This behaviour is
why the consistency model from Section 2.1 can’t straightforwardly be extended
to accommodate nondependent function types. We examine the issue in detail in
6.4.

###  3.1. Examples

#### The identity function

Here’s one way we could assign a type to the type-polymorphic identity
function. For concision, we use a pattern syntax when defining global
functions and place function arguments to the left of the definition. (The
subscript is part of constant name.)

$\displaystyle\mathsf{id_{0}}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}$
$\displaystyle\mathsf{id_{0}}\;\mathit{X}\;\mathit{\mathit{x}}\coloneqq\mathit{\mathit{x}}$

Stratification enforces that the codomain of the function type and the
function body have a higher level than that of the domain and the argument, so
the overall identity function is well typed at level 1. While $\mathit{x}$ and
$X$ have level 0 in the context of the body, by subsumption, we can use
$\mathit{x}$ at level 1 in the body as required. Although the level of the
domain of $\mathsf{id_{0}}$ is fixed at 0, we can displace the constant by 1.

$\displaystyle\mathsf{id_{1}}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{1}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{1}}\\!\mathit{X}\mathpunct{.}\mathit{X}$
$\displaystyle\mathsf{id_{1}}\coloneqq\mathsf{id_{0}}^{\ottsym{1}}$

Since we have cumulativity, we would expect to be able to apply
$\mathsf{id_{1}}$ to itself. This is possible with a typical cumulative
universe hierarchy, such as in Coq. In the below definition, since `(forall (X
: Type@{u0}), X -> X)` can be assigned type `Type@{u1}`, it can be used as the
first argument to `id1`. The second argument must then have type `(forall (X :
Type@{u0}), X -> X)`. While `id1` itself doesn’t have this type, we can
$\eta$-expand it to a function that does, since `Type@{u0}` is a subtype of
`Type@{u1}` and thus `X` of the former type can be passed into a function that
takes the latter.

⬇

Universe u0 u1.

Constraint u0 <= u1.

Definition id1 (X : Type@{u1}) (x : X) : X := x.

Definition idid1 : forall X, X -> X :=

id1 (forall (X : Type@{u0}), X -> X)

(fun X x => id1 X x).

However, the analogous definition applying $\mathsf{id_{1}}$ to itself doesn’t
type check! The problematic subterm is bolded in red below.

$\displaystyle\mathsf{idid_{1}}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathit{X}$
$\displaystyle\mathsf{idid_{1}}\coloneqq\mathsf{id_{1}}\;\ottsym{(}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathit{X}\ottsym{)}\;{\color[rgb]{1,0,0}\bm{\ottsym{(}\lambda\mathit{X}\mathpunct{.}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{id_{1}}\;\mathit{X}\;\mathit{\mathit{x}}\ottsym{)}}}$

The type
$\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathit{X}$
is well typed at level 1, but the term
$\lambda\mathit{X}\mathpunct{.}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{id_{1}}\;\mathit{X}\;\mathit{\mathit{x}}$
is only well typed with that type (again via subsumption) at level 2, so the
latter can’t be applied as the second argument to $\mathsf{id_{1}}$, which is
fixed at level 1. Here is where floating nondependent function type comes to
use. Since the second argument isn’t depended upon in the type, we can assign
the identity function as follows.

$\displaystyle\mathsf{id}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{id}\;\mathit{X}\;\mathit{\mathit{x}}\coloneqq\mathit{\mathit{x}}$

Now the argument $\mathit{x}$ and the function body are both at level 1
without requiring subsumption. The argument and body of a nondependent
function having the same level is key to typing the self-application.

$\displaystyle\mathsf{idid}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{idid}\coloneqq\mathsf{id}^{\ottsym{1}}\;\ottsym{(}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}\ottsym{)}\;\ottsym{(}\lambda\mathit{X}\mathpunct{.}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{id}^{\ottsym{1}}\;\mathit{X}\;\mathit{\mathit{x}}\ottsym{)}$

Displacing $\mathsf{id}$ by 1, we can then pass in the type
$\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}$,
which has level 1, followed by
$\lambda\mathit{X}\mathpunct{.}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{id}^{\ottsym{1}}\;\mathit{X}\;\mathit{\mathit{x}}$,
which has level 2, yielding a final term at level 2.

#### Decidable types

Floating nondependent function types are similarly crucial for type
constructors. Later in 5 we’ll consider datatypes with parameters, but for
now, consider the following Church encoding (Böhm and Berarducci, 1985) of
decidable types, which additionally uses negation defined as implication into
the empty type.

$\displaystyle\mathsf{neg}:^{\ottsym{0}}\star\mathrel{\rightarrow}\star$
$\displaystyle\mathsf{neg}\;\mathit{X}\coloneqq\mathit{X}\mathrel{\rightarrow}\bot$
$\displaystyle\mathsf{Dec}:^{\ottsym{1}}\star\mathrel{\rightarrow}\star$
$\displaystyle\mathsf{Dec}\;\mathit{X}\coloneqq\Pi\mathit{Z}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\ottsym{(}\mathit{X}\mathrel{\rightarrow}\mathit{Z}\ottsym{)}\mathrel{\rightarrow}\ottsym{(}\mathsf{neg}\;\mathit{X}\mathrel{\rightarrow}\mathit{Z}\ottsym{)}\mathrel{\rightarrow}\mathit{Z}$
$\displaystyle\mathsf{yes}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathsf{Dec}\;\mathit{X}$
$\displaystyle\mathsf{yes}\;\mathit{X}\;\mathit{\mathit{x}}\coloneqq\lambda\mathit{Z}\mathpunct{.}\lambda\mathit{\mathit{f}}\mathpunct{.}\lambda\mathit{\mathit{g}}\mathpunct{.}\mathit{\mathit{f}}\;\mathit{\mathit{x}}$
$\displaystyle\mathsf{no}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathsf{neg}\;\mathit{X}\mathrel{\rightarrow}\mathsf{Dec}\;\mathit{X}$
$\displaystyle\mathsf{no}\;\mathit{X}\;\mathit{nx}\coloneqq\lambda\mathit{Z}\mathpunct{.}\lambda\mathit{\mathit{f}}\mathpunct{.}\lambda\mathit{\mathit{g}}\mathpunct{.}\mathit{\mathit{g}}\;\mathit{nx}$

The $\mathsf{yes}\;\mathit{X}$ constructor decides $X$ by a witness, while the
$\mathsf{no}\;\mathit{X}$ constructor decides $X$ by its refutation. We’re
able to show that deciding a given type is irrefutable.666Note this differs
from irrefutability of the law of excluded middle,
$\mathsf{neg}\;\ottsym{(}\mathsf{neg}\;\ottsym{(}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathsf{Dec}\;\mathit{X}\ottsym{)}\ottsym{)}$,
which cannot be proven constructively.

$\displaystyle\mathsf{irrDec}:\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathsf{neg}\;\ottsym{(}\mathsf{neg}\;\ottsym{(}\mathsf{Dec}\;\mathit{X}\ottsym{)}\ottsym{)}$
$\displaystyle\mathsf{irrDec}\;\mathit{X}\;\mathit{ndec}\coloneqq\mathit{ndec}\;\ottsym{(}\mathsf{no}\;\mathit{X}\;\ottsym{(}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathit{ndec}\;\ottsym{(}\mathsf{yes}\;\mathit{X}\;\mathit{\mathit{x}}\ottsym{)}\ottsym{)}\ottsym{)}$

Without the nondependent function type, $\mathsf{neg}$ and $\mathsf{Dec}$
would be forced produce types at higher levels. The corresponding constructors
$\mathsf{yes^{\prime}}$ and $\mathsf{no^{\prime}}$, omitted below, would also
have higher levels.

$\displaystyle\mathsf{neg^{\prime}}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\star$
$\displaystyle\mathsf{neg^{\prime}}\;\mathit{X}\coloneqq\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\bot$
$\displaystyle\mathsf{Dec^{\prime}}:^{\ottsym{3}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\star$
$\displaystyle\mathsf{Dec^{\prime}}\;\mathit{X}\coloneqq\Pi\mathit{Z}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{yz}\\!:^{\ottsym{2}}\\!\ottsym{(}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathit{Z}\ottsym{)}\mathpunct{.}{}$
$\displaystyle\phantom{\mathsf{Dec^{\prime}}\;\mathit{X}\coloneqq\Pi\mathit{Z}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}{}}\Pi\mathit{nz}\\!:^{\ottsym{2}}\\!\ottsym{(}\Pi\mathit{nx}\\!:^{\ottsym{1}}\\!\mathsf{neg^{\prime}}\;\mathit{X}\mathpunct{.}\mathit{Z}\ottsym{)}\mathpunct{.}\mathit{Z}$

Every dependent quantification in the domain increases the overall level, so
the smallest level that can be assigned to $\mathsf{Dec^{\prime}}\;\mathit{X}$
is 3, since it takes a function eliminating a $\mathsf{no^{\prime}}$, which is
a function taking the negation of $X$, which itself is a function from $X$. We
can continue on to write the corresponding type of $\mathsf{irrDec^{\prime}}$,
displacing $\mathsf{neg^{\prime}}$ as needed, but the body will no longer type
check against it.

$\displaystyle\mathsf{irrDec^{\prime}}:^{\ottsym{5}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathsf{neg^{\prime}}^{\ottsym{4}}\;\ottsym{(}\mathsf{neg^{\prime}}^{\ottsym{3}}\;\ottsym{(}\mathsf{Dec^{\prime}}\;\mathit{X}\ottsym{)}\ottsym{)}$
$\displaystyle\mathsf{irrDec^{\prime}}\;\mathit{X}\;\mathit{ndec}\coloneqq\mathit{ndec}\;\ottsym{(}\mathsf{no^{\prime}}\;\mathit{X}\;\ottsym{(}\lambda\mathit{\mathit{x}}\mathpunct{.}{\color[rgb]{1,0,0}\bm{\mathit{ndec}\;\ottsym{(}\mathsf{yes^{\prime}}\;\mathit{X}\;\mathit{\mathit{x}}\ottsym{)}}}\ottsym{)}\ottsym{)}$

The level of the function $ndec$ of type
$\mathsf{neg^{\prime}}^{\ottsym{3}}\;\ottsym{(}\mathsf{Dec^{\prime}}\;\mathit{X}\ottsym{)}$
is now 4, which is too high to be used in the argument of
$\mathsf{no^{\prime}}$; if we displace $\mathsf{yes^{\prime}}$ and
$\mathsf{no^{\prime}}$, then the level of the argument of $ndec$ will in turn
be too high to fit.

#### Leibniz equality

Although nondependent functions can often benefit from a floating domain,
sometimes we don’t want the domain to float. In some examples, the level of
the domain needs to be fixed to something strictly smaller than that of the
codomain even when the codomain doesn’t depend on the function argument. Here,
we turn to a simple application of dependent types with Leibniz equality
(Leibniz, 1686; Martin-Löf, 1971) to demonstrate such a situation.

$\displaystyle\mathsf{eq}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}\mathrel{\rightarrow}\star$
$\displaystyle\mathsf{eq}\;\mathit{X}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\coloneqq\Pi\mathit{P}\\!:^{\ottsym{0}}\\!\mathit{X}\mathrel{\rightarrow}\star\mathpunct{.}\mathit{P}\;\mathit{\mathit{x}}\mathrel{\rightarrow}\mathit{P}\;\mathit{\mathit{y}}$

An equality $\mathsf{eq}\;\ottnt{A}\;\ottnt{a}\;\ottnt{b}$ states that two
terms are equal if given any predicate $P$, a proof of $\mathit{P}\;\ottnt{a}$
yields a proof of $\mathit{P}\;\ottnt{b}$; in other words, $\ottnt{a}$ and
$\ottnt{b}$ are indiscernible. The proof of reflexivity of Leibniz equality
should be unsurprising.

$\displaystyle\mathsf{refl}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathsf{eq}\;\mathit{X}\;\mathit{\mathit{x}}\;\mathit{\mathit{x}}$
$\displaystyle\mathsf{refl}\;\mathit{X}\;\mathit{\mathit{x}}\;\mathit{P}\;\mathit{px}\coloneqq\mathit{px}$

We might try to define a predicate stating that a given type $X$ is a mere
proposition, i.e. that all of its inhabitants are equal, and give it a
nondependent function type.

$\displaystyle\mathsf{isProp}:^{\ottsym{0}}\star\mathrel{\rightarrow}\star$
$\displaystyle\mathsf{isProp}\;\mathit{X}\coloneqq{\color[rgb]{1,0,0}\bm{\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\Pi\mathit{\mathit{y}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathsf{eq}\;\mathit{X}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}}}$

But this doesn’t type check, since the body contains an equality over elements
of $X$, which necessarily has level 1 rather than the expected level 0. We
must assign $\mathsf{isProp}$ a stratified function type; informally,
stratification propagates dependency information not only from the codomain,
but also from the function body.

$\displaystyle\mathsf{isProp}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\star$
$\displaystyle\mathsf{isProp}\;\mathit{X}\coloneqq\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\Pi\mathit{\mathit{y}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathsf{eq}\;\mathit{X}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}$

Going one further, we can define a predicate $isSet$ stating that $X$ is an
h-set (Univalent Foundations Program, 2013), or that its equalities are mere
propositions, by using a displaced $\mathsf{isProp}$, which also raises the
overall level. Once again, despite the type of $\mathsf{isSet}$ not being an
actual dependent function type, here we need to fix the level of the domain.

$\displaystyle\mathsf{isSet}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\star$
$\displaystyle\mathsf{isSet}\;\mathit{X}\coloneqq\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\Pi\mathit{\mathit{y}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathsf{isProp}^{\ottsym{1}}\;\ottsym{(}\mathsf{eq}\;\mathit{X}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\ottsym{)}$

##  4\. Syntactic metatheory

We use Coq to mechanize the syntactic metatheory of the typing, context
formation, and signature formation judgements of StraTT, recalling that this
covers all of stratified dependent functions, floating nondependent functions,
and displaced constants. The proof scripts are available at
https://github.com/plclub/StraTT under the coq/ directory.

#### Strengthening

The key idea of this type system design is that stratification levels
delineate judgements. A judgement at level $\ottnt{k}$ is only allowed to
depend on judgements at the same or lower levels. One way to observe this
property is through a form of strengthening result, which states that
variables from higher levels can always be removed from the context and that
contexts can be truncated at any level. Formally, we define the _restriction_
operation, written $\lceil\Gamma\rceil^{\ottnt{k}}$, that filters out all
assumptions from the context with level greater than $k$.

###### Lemma 4.0 (Restriction).

777coq/ctx.v:DSig_DCtx_DTyping_restriction

If $\Delta\vdash\Gamma$ then $\Delta\vdash\lceil\Gamma\rceil^{\ottnt{k}}$ for
any $\ottnt{k}$, and if $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$
then
$\Delta;\lceil\Gamma\rceil^{\ottnt{k}}\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$.

#### Weakening and Narrowing

We can extend the ordering between levels, $\ottnt{j}\leq\ottnt{k}$, to an
ordering between contexts, $\Gamma_{{\mathrm{1}}}\leq\Gamma_{{\mathrm{2}}}$.
At the same time, we also incorporate the idea of weakening into this
relation. Stronger contexts have higher levels and fewer assumptions.

  * $\Gamma_{{\mathrm{1}}}\leq\Gamma_{{\mathrm{2}}}$ (_Context ordering_)

(S-Nil?)(S-Cons?)(S-Weak?)

This ordering is contravariant in the typing judgement: we can lower the
context without destroying typeability. This result subsumes a standard
weakening lemma.

###### Lemma 4.0 (Weakening/Narrowing).

888coq/ctx.v:DTyping_SubG

If $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$ and
$\Delta\vdash\Gamma^{\prime}$ and $\Gamma^{\prime}\leq\Gamma$ then
$\Delta;\Gamma^{\prime}\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$.

Note that a restricted context could be stronger than the original because it
could contain fewer variable assumptions.

###### Lemma 4.0 (Restriction subsumption).

999coq/restrict.v:SubG_restrict

$\Gamma\leq\lceil\Gamma\rceil^{\ottnt{k}}$.

#### Substitution and regularity

The substitution operation must respect levels.

###### Lemma 4.0 (Substitution).

101010coq/subst.v:DTyping_subst

If
$\Delta;\Gamma_{{\mathrm{1}}},\mathit{x}:^{\ottnt{j}}\ottnt{B},\Gamma_{{\mathrm{2}}}\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$
and $\Delta;\Gamma_{{\mathrm{1}}}\vdash\ottnt{b}:^{\ottnt{j}}\ottnt{B}$ then
$\Delta;\Gamma_{{\mathrm{1}}},\Gamma_{{\mathrm{2}}}\ottsym{\\{}\ottnt{b}\ottsym{/}\mathit{x}\ottsym{\\}}\vdash\ottnt{a}\mathopen{\\{}\ottnt{b}/\mathit{\mathit{x}}\mathclose{\\}}:^{\ottnt{k}}\ottnt{A}\mathopen{\\{}\ottnt{b}/\mathit{\mathit{x}}\mathclose{\\}}$.

This lemma reflects the idea that a variable assumption
$\mathit{x}:^{\ottnt{k}}\ottnt{B}$ is a hypothetical judgement. The variable
$\mathit{x}$ stands for any typing derivation of the appropriate type and
level. Typing judgements themselves ensure the well-formedness of their
subcomponents. Note that if a term type checks, its type can be typed at the
same level.

###### Lemma 4.0 (Regularity).

111111coq/ctx.v:DCtx_DSig , coq/inversion.v:DTyping_DCtx ,
coq/ctx.v:DTyping_regularity

If $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$ then $\vdash\Delta$
and $\Delta\vdash\Gamma$ and $\Delta;\Gamma\vdash\ottnt{A}:^{\ottnt{k}}\star$

Because our type system includes the non–syntax-directed rule T-Conv, the
proof of this lemma depends on several inversion lemmas (not shown).

#### Displacement

Derivations can be displaced wholesale. For example, if we have a derivation

$\mathit{f}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\ottnt{A}\mathpunct{.}\ottnt{B},\mathit{x}:^{\ottsym{0}}\ottnt{A}\vdash\mathit{\mathit{f}}\;\mathit{\mathit{x}}:^{\ottsym{1}}\ottnt{B}$

we can add 1 to each level in the judgement to get a new derivation.

$\mathit{f}:^{\ottsym{2}}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{1}}\\!\ottnt{A}\mathpunct{.}\ottnt{B},\mathit{x}:^{\ottsym{1}}\ottnt{A}\vdash\mathit{\mathit{f}}\;\mathit{\mathit{x}}:^{\ottsym{2}}\ottnt{B}$

More generally, we can add any level displacement $\ottnt{i}$ to each level in
the judgement.

$\mathit{f}:^{\ottsym{1}\ottsym{+}\ottnt{i}}\Pi\mathit{\mathit{x}}\\!:^{\ottnt{i}}\\!\ottnt{A}\mathpunct{.}\ottnt{B},\mathit{x}:^{\ottnt{i}}\ottnt{A}\vdash\mathit{\mathit{f}}\;\mathit{\mathit{x}}:^{\ottsym{1}\ottsym{+}\ottnt{i}}\ottnt{B}$

This is a generalization of displaceability in an empty context to include
displacement of contexts, written as $\Gamma^{+\ottnt{i}}$, where
$\ottsym{(}\Gamma,\mathit{x}:^{\ottnt{k}}\ottnt{A}\ottsym{)}^{+\ottnt{i}}=\Gamma^{+\ottnt{i}},\mathit{x}:^{\ottnt{k}\ottsym{+}\ottnt{i}}\ottnt{A}^{+\ottnt{i}}$.

###### Lemma 4.0 (Displacement).

121212coq/ctx.v:DTyping_incr

If $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$ then
$\Delta;\Gamma^{+\ottnt{j}}\vdash\ottnt{a}^{+\ottnt{j}}:^{\ottnt{j}\ottsym{+}\ottnt{k}}\ottnt{A}^{+\ottnt{j}}$.

Note that if we displace a context, the result may not be stronger than the
original because displacement may modify the types in the assumptions. In
other words, it is _not_ the case that $\Gamma\leq\Gamma^{+\ottnt{k}}$.

#### Floating

Sometimes we would like to use a dependent function, like $\mathit{f}$ above,
at a higher level, without displacing its type. The cumulativity rule allows
variables from one level to be made available to all higher levels using their
current type. However, when we use this rule in a judgement it does not change
the context that is used to check the term. This can be restrictive — we can
only substitute their assumptions with lower level derivations. In a special
case, we can raise the level of some assumptions in the context when we raise
the level of the judgement without displacing their types or the rest of the
context. For example, suppose we have the following derivation.

$\mathit{f}:^{\ottnt{j}}\Pi\mathit{\mathit{x}}\\!:^{\ottnt{i}}\\!\ottnt{A}\mathpunct{.}\ottnt{B},\mathit{x}:^{\ottnt{i}}\ottnt{A}\vdash\mathit{\mathit{f}}\;\mathit{\mathit{x}}:^{\ottnt{j}}\ottnt{B}$

This structure would also make sense at a higher level $\ottnt{k}$, where we
have also raised the level of $\mathit{f}$.

$\mathit{f}:^{\ottnt{k}}\Pi\mathit{\mathit{x}}\\!:^{\ottnt{i}}\\!\ottnt{A}\mathpunct{.}\ottnt{B},\mathit{x}:^{\ottnt{i}}\ottnt{A}\vdash\mathit{\mathit{f}}\;\mathit{\mathit{x}}:^{\ottnt{k}}\ottnt{B}$

However, we can only raise the level of variables, like $\mathit{f}$, that are
at the _same_ level as the entire judgement. For example, we cannot raise
$\mathit{x}$ which is at some lower level $\ottnt{i}$ because then it would be
invalid as an argument to $\mathit{f}$. To prove this formally, we must work
with judgements that do not have any assumptions above the current level. We
know from strengthening that these assumptions aren’t needed by the
derivation, but their types could mention the variables that are being raised,
and we want to ensure that the resulting context is well formed. Therefore, we
use the restriction operation to first discard the irrelevant variables.
Furthermore, to raise the level of certain levels, we introduce the _floating_
operation on contexts $\mathopen{\uparrow_{\ottnt{j}}^{\ottnt{k}}}\Gamma$ that
raises assumptions in $\Gamma$ at level $\ottnt{j}$ to some higher level
$\ottnt{k}$ without displacing their types.

###### Lemma 4.0 (Restricted Floating).

131313coq/restrict.v:DTyping_float_restrict

If $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{j}}\ottnt{A}$ and
$\ottnt{j}\leq\ottnt{k}$ then
$\Delta;\mathopen{\uparrow_{\ottnt{j}}^{\ottnt{k}}}\ottsym{(}\lceil\Gamma\rceil^{\ottnt{j}}\ottsym{)}\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$.

The proof of the lemma above requires the following two observations. First,
that floating starting from a lower number is stronger than floating from a
higher number.

###### Lemma 4.0.

141414coq/restrict.v:SubG_float_leq

Say $\ottnt{i}\leq\ottnt{j}$ and $\ottnt{j}\leq\ottnt{k}$, then
$\mathopen{\uparrow_{\ottnt{j}}^{\ottnt{k}}}\ottsym{(}\lceil\Gamma\rceil^{\ottnt{j}}\ottsym{)}\leq\mathopen{\uparrow_{\ottnt{i}}^{\ottnt{k}}}\ottsym{(}\lceil\Gamma\rceil^{\ottnt{i}}\ottsym{)}$

Second, if we have a strict ordering between $\ottnt{i}$ and $\ottnt{j}$, then
it doesn’t matter what the higher number floats to because they won’t be
present in the lower restriction.

###### Lemma 4.0.

151515coq/restrict.v:SubG_float_lt

Say $\ottnt{i}\ottsym{<}\ottnt{j}$ and
$\ottnt{i}\leq\ottnt{k_{{\mathrm{2}}}}$, then for any
$\ottnt{k_{{\mathrm{1}}}}$,
$\mathopen{\uparrow_{\ottnt{j}}^{\ottnt{k_{{\mathrm{1}}}}}}\ottsym{(}\lceil\Gamma\rceil^{\ottnt{j}}\ottsym{)}\leq\mathopen{\uparrow_{\ottnt{i}}^{\ottnt{k_{{\mathrm{2}}}}}}\ottsym{(}\lceil\Gamma\rceil^{\ottnt{i}}\ottsym{)}$

#### Type Safety

We have shown that this language satisfies the preservation (i.e. subject
reduction) and progress lemmas, where $\Delta\vdash\ottnt{a}\leadsto\ottnt{b}$
consists of $\beta$\- and $\delta$-reduction with call-by-name evaluation.

###### Lemma 4.0 (Preservation).

161616coq/typesafety.v:Reduce_Preservation

If $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$ and
$\Delta\vdash\ottnt{a}\leadsto\ottnt{a^{\prime}}$ then
$\Delta;\Gamma\vdash\ottnt{a^{\prime}}:^{\ottnt{k}}\ottnt{A}$.

The case for $\beta$-reduction of nondependent functions requires the
expressiveness of the restricted floating lemma above. In this case, we have a
derivation of the form
$\Gamma\vdash\ottsym{(}\lambda\mathit{\mathit{x}}\mathpunct{.}\ottnt{a}\ottsym{)}\;\ottnt{b}:^{\ottnt{k}}\ottnt{B}$,
and we would like to show that the term after reduction
$\Gamma\vdash\ottnt{a}\mathopen{\\{}\ottnt{b}/\mathit{\mathit{x}}\mathclose{\\}}:^{\ottnt{k}}\ottnt{B}$
is well typed. Our inversion lemmas give us the typing of the function and
argument at some level $\ottnt{k}$.

$\Gamma\vdash\lambda\mathit{\mathit{x}}\mathpunct{.}\ottnt{a}:^{\ottnt{k}}\ottnt{A}\mathrel{\rightarrow}\ottnt{B}\qquad\Gamma\vdash\ottnt{b}:^{\ottnt{k}}\ottnt{A}$

Inverting the first derivation again, we find that because of cumulativity,
for some $\ottnt{j}\leq\ottnt{k}$ we have
$\Gamma,\mathit{x}:^{\ottnt{j}}\ottnt{A_{{\mathrm{1}}}}\vdash\ottnt{a}:^{\ottnt{j}}\ottnt{A_{{\mathrm{2}}}}$.
We cannot directly use the substitution lemma to show the result because
$\mathit{x}$ needs to be at level $\ottnt{j}$, but the argument may be at some
potentially higher level $\ottnt{k}$. Therefore, to complete the proof, we use
the restricted floating lemma above to modify the derivation above so that we
have the one required for substitution.

$\mathopen{\uparrow_{\ottnt{j}}^{\ottnt{k}}}\ottsym{(}\lceil\Gamma\rceil^{\ottnt{j}}\ottsym{)},\mathit{x}:^{\ottnt{k}}\ottnt{A_{{\mathrm{1}}}}\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A_{{\mathrm{2}}}}$

We can then weaken this derivation to the original context

$\Gamma,\mathit{x}:^{\ottnt{k}}\ottnt{A_{{\mathrm{1}}}}\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A_{{\mathrm{2}}}}$

and then, with the help of rule T-Conv to convert the types
$\ottnt{A_{{\mathrm{2}}}}$ to $\ottnt{B}$ and $\ottnt{A}$ to
$\ottnt{A_{{\mathrm{1}}}}$, conclude the desired result via our substitution
lemma. Because we have not mechanized the metatheory of our equivalence
relation $\ottnt{A}\equiv\ottnt{B}$, the preservation proof relies on standard
properties about this relation (Barendregt, 1984) that we state as axioms in
the development. Levels do not play a role in definitional equality.

###### Proposition 4.11 (Injectivity for nondependent function types).

171717coq/axioms.v:DEquiv_Arrow_inj1,DEquiv_Arrow_inj2

If
$\ottnt{A_{{\mathrm{1}}}}\mathrel{\rightarrow}\ottnt{A_{{\mathrm{2}}}}\equiv\ottnt{A}\mathrel{\rightarrow}\ottnt{B}$
then $\ottnt{A_{{\mathrm{1}}}}\equiv\ottnt{A}$ and
$\ottnt{A_{{\mathrm{2}}}}\equiv\ottnt{B}$.

###### Proposition 4.12 (Injectivity for dependent function types).

181818coq/axioms.v:DEquiv_Pi_inj1,DEquiv_Pi_inj2

If
$\Pi\mathit{\mathit{x}}\\!:^{\ottnt{j_{{\mathrm{1}}}}}\\!\ottnt{A_{{\mathrm{1}}}}\mathpunct{.}\ottnt{B_{{\mathrm{1}}}}\equiv\Pi\mathit{\mathit{x}}\\!:^{\ottnt{j_{{\mathrm{2}}}}}\\!\ottnt{A_{{\mathrm{2}}}}\mathpunct{.}\ottnt{B_{{\mathrm{2}}}}$
then $\ottnt{A_{{\mathrm{1}}}}\equiv\ottnt{A_{{\mathrm{2}}}}$,
$\ottnt{j_{{\mathrm{1}}}}\ottsym{=}\ottnt{j_{{\mathrm{2}}}}$, and
$\ottnt{B_{{\mathrm{1}}}}\equiv\ottnt{B_{{\mathrm{2}}}}$.

###### Proposition 4.13 (Consistency of definitional equality).

191919coq/axioms.v:ineq_*

If $\ottnt{A}\equiv\ottnt{B}$ then $\ottnt{A}$ and $\ottnt{B}$ do not have
different head forms.

Preservation for the reflexive, transitive closure of reduction also follows
from preservation for reduction.

###### Corollary 4.0 (Preservation).

202020coq/typesafety.v:WHNF_Preservation

If $\Delta;\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$ and
$\Delta\vdash\ottnt{a}\leadsto^{\ast}\ottnt{a^{\prime}}$ then
$\Delta;\Gamma\vdash\ottnt{a^{\prime}}:^{\ottnt{k}}\ottnt{A}$.

The progress lemma follows in the usual way.

###### Lemma 4.0 (Progress).

212121coq/typesafety.v:progress

If $\Delta;\varnothing\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$ then either
$\ottnt{a}$ is a value or there is some $\ottnt{b}$ such that
$\Delta\vdash\ottnt{a}\leadsto\ottnt{b}$.

Aside from the assumptions about definitional equality stated above, the case
of $\mathsf{absurd}(\ottnt{a})$ in this proof also requires that the language
be logically consistent, which we assume as an axiom in our Coq
development.222222coq/axioms.v:empty_Bottom

##  5\. Prototype implementation with level inference and datatypes

To explore the expressiveness of StraTT, we have implemented a prototype type
checker, which can be found at https://github.com/plclub/StraTT under the
impl/ directory. This implementation is based on pi-forall (Weirich, 2023), a
simple bidirectional type checker for a dependently-typed programming
language.

#### Annotation inference

For convenience, displacements and level annotations on dependent types can be
omitted; the type checker then generates level metavariables in their stead.
When checking a single global definition, constraints on level metavariables
are collected, which form a set of linear integer inequalities on
metavariables. An SMT solver checks that these inequalities are satisfiable by
the naturals and finally provides a solution that minimizes the levels. As an
example, recall the $\mathsf{idid}$ example from 3.1.

$\displaystyle\mathsf{idid}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{idid}\coloneqq\mathsf{id}^{\ottsym{1}}\;\ottsym{(}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}\ottsym{)}\;\ottsym{(}\lambda\mathit{X}\mathpunct{.}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{id}^{\ottsym{1}}\;\mathit{X}\;\mathit{\mathit{x}}\ottsym{)}$

All annotations can be left out, and the exact same levels and displacements
will be inferred.

$\displaystyle\mathsf{idid^{\prime}}:\Pi\mathit{X}\\!:\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{idid^{\prime}}\coloneqq\mathsf{id}\;\ottsym{(}\Pi\mathit{X}\\!:\\!\star\mathpunct{.}\mathit{X}\mathrel{\rightarrow}\mathit{X}\ottsym{)}\;\ottsym{(}\lambda\mathit{X}\mathpunct{.}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{id}\;\mathit{X}\;\mathit{\mathit{x}}\ottsym{)}$

For clarity, in the remaining examples in this section, we always write
annotations explicitly. However, each of these examples also type check with
their annotations removed. More generally, we don’t yet know whether a most
general set of displacements and level annotations always exists and is
discoverable by an SMT solver. Although we’ve found that our simple approach
to inference doesn’t always produce the best solution in some constructed
examples, in future work we seek to address the inference question with more
sophisticated tools.

#### Datatypes

The implementation additionally features stratified datatypes, case
expressions, and recursion, used to demonstrate the practicality of
programming in StraTT. Restricting the datatypes to inductive types by
checking strict positivity and termination of recursive functions to ensure
consistency is possible but orthogonal to stratification and thus out of scope
for this work. In this section and the next, the examples we provide will
always satisfy strict positivity and structural termination. Revisiting an
example from 3.1, we can define $\mathsf{Dec}$ as a datatype.

$\displaystyle\mathbf{data}\;\mathsf{Dec}{}\;(\mathit{X}:\star):^{\ottsym{0}}\star\;\mathbf{where}$
$\displaystyle\quad\mathsf{Yes}:^{\ottsym{0}}\mathit{X}\mathrel{\rightarrow}\mathsf{Dec}\;\mathit{X}$
$\displaystyle\quad\mathsf{No}:^{\ottsym{0}}\mathsf{neg}\;\mathit{X}\mathrel{\rightarrow}\mathsf{Dec}\;\mathit{X}$

The lack of annotation on the parameter indicates that it’s a floating domain,
so that $\lambda\mathit{X}\mathpunct{.}\mathsf{Dec}\;\mathit{X}$ can be
assigned type $\star\mathrel{\rightarrow}\star$ at level 0. Datatypes and
their constructors, like variables and constants, are cumulative, so the
aforementioned type assignment is valid at any level above 0 as well. When
destructing a datatype, the constructor arguments of each branch are typed
such that the constructor would have the same level as the level of the
scrutinee. Consider the following proof that decidability of a type implies
its double negation elimination, which requires inspecting the decision.

$\displaystyle\mathsf{decDNE}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\mathsf{Dec}\;\mathit{X}\mathrel{\rightarrow}\mathsf{neg}\;\ottsym{(}\mathsf{neg}\;\mathit{X}\ottsym{)}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{decDNE}\;\mathit{X}\;\mathit{dec}\;\mathit{nnx}\coloneqq\mathbf{case}\;\mathit{dec}\;\mathbf{of}$
$\displaystyle\quad\mathsf{Yes}\;\mathit{\mathit{x}}\mathrel{\Rightarrow}\mathit{\mathit{x}}$
$\displaystyle\quad\mathsf{No}\;\mathsf{nx}\mathrel{\Rightarrow}\mathsf{absurd}(\mathit{nnx}\;\mathit{nx})$

By the level annotation on the function, we know that $dec$ and $nnx$ both
have level 1. Then in the branches, the patterns
$\mathsf{Yes}\;\mathit{\mathit{x}}$ and $\mathsf{No}\;\mathit{nx}$ must also
be typed at level 1, so that $\mathit{x}$ has type $X$ and $nx$ has type
$\mathsf{neg}\;\mathit{X}$ both at level 1.

#### Datatype displacement

Datatypes and their constructors, like constants, can be displaced as well,
uniformly raising the levels of their types. Consider now a $\mathsf{Box}$
type which stores in it a term of a fixed lower level.

$\displaystyle\mathbf{data}\;\mathsf{Box}{}\;(\mathit{X}:^{\ottsym{0}}\star):^{\ottsym{1}}\star\;\mathbf{where}$
$\displaystyle\quad\mathsf{MkBox}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathsf{Box}\;\mathit{X}$

This time, the presence of the level 0 annotation on the parameter indicates
that it’s fixed, which also allows the constructor argument $\mathit{x}$ to be
fixed at level 0. Displacing a $\mathsf{Box}$ by 1 then raises the fixed
parameter level to 1, and its sole constructor would be a $\mathsf{MkBox}$
displaced by 1 which destructs to yield a term at level 1. The following
$\mathsf{map}$ over a box displaced by 1 with a function at level 1
demonstrates this behaviour.

$\displaystyle\mathsf{map}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{1}}\\!\star\mathpunct{.}\Pi\mathit{Y}\\!:^{\ottsym{1}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{f}}\\!:^{\ottsym{1}}\\!\mathit{X}\mathrel{\rightarrow}\mathit{Y}\mathpunct{.}\mathsf{Box}^{\ottsym{1}}\;\mathit{X}\mathrel{\rightarrow}\mathsf{Box}^{\ottsym{1}}\;\mathit{Y}$
$\displaystyle\mathsf{map}\;\mathit{X}\;\mathit{Y}\;\mathit{\mathit{f}}\;\mathit{box}\coloneqq\mathbf{case}\;\mathit{box}\;\mathbf{of}$
$\displaystyle\quad\mathsf{MkBox}^{\ottsym{1}}\;\mathit{\mathit{x}}\mathrel{\Rightarrow}\mathsf{MkBox}^{\ottsym{1}}\;\ottsym{(}\mathit{\mathit{f}}\;\mathit{\mathit{x}}\ottsym{)}$

###  5.1. Extended example: dependent pairs

Along with $\mathsf{Dec}$ and $\mathsf{Box}$, we include with our
implementation a variety of common datatypes and associated functions, such as
dependent pairs, logical connectives, booleans, optionals, naturals, lists,
finite sets, and vectors.232323impl/pi/README.pi Here, we take a closer look
at dependent pairs to further explore the behaviour and limitations of StraTT.
Because there are two different function types, there are also two different
ways to define dependent pairs. Using a floating function type for the second
component’s type results in pairs whose first and second projections can be
defined as usual, while using the stratified dependent function type results
in pairs whose second projection can’t be defined in terms of the first. We
first take a look at the former.

$\displaystyle\mathbf{data}\;\mathsf{NPair}{}\;(\mathit{X}:^{\ottsym{0}}\star)\;(\mathit{P}:\mathit{X}\mathrel{\rightarrow}\star):^{\ottsym{1}}\star\;\mathbf{where}$
$\displaystyle\quad\mathsf{MkPair}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathit{P}\;\mathit{\mathit{x}}\mathrel{\rightarrow}\mathsf{NPair}\;\mathit{X}\;\mathit{P}$
$\displaystyle\mathsf{nfst}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{P}\\!:^{\ottsym{1}}\\!\mathit{X}\mathrel{\rightarrow}\star\mathpunct{.}\mathsf{NPair}\;\mathit{X}\;\mathit{P}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{nfst}\;\mathit{X}\;\mathit{P}\;\mathit{p}\coloneqq\mathbf{case}\;\mathit{p}\;\mathbf{of}\;\mathsf{MkPair}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\mathrel{\Rightarrow}\mathit{\mathit{x}}$
$\displaystyle\mathsf{nsnd}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{P}\\!:^{\ottsym{1}}\\!\mathit{X}\mathrel{\rightarrow}\star\mathpunct{.}\Pi\mathit{p}\\!:^{\ottsym{1}}\\!\mathsf{NPair}\;\mathit{X}\;\mathit{P}\mathpunct{.}\mathit{P}\;\ottsym{(}\mathsf{nfst}\;\mathit{X}\;\mathit{P}\;\mathit{p}\ottsym{)}$
$\displaystyle\mathsf{nsnd}\;\mathit{X}\;\mathit{P}\;\mathit{p}\coloneqq\mathbf{case}\;\mathit{p}\;\mathbf{of}\;\mathsf{MkPair}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\mathrel{\Rightarrow}\mathit{\mathit{y}}$

Due to stratification, the projections unfortunately need to be defined at
level 2 to accommodate dependently quantifying over the $P$ at level 1. Even
so, the second projection is well typed, since $P$ can be used at level 2 by
subsumption to be applied to the first projection. As the two function types
are distinct, we do need both varieties of dependent pairs. In particular,
with the above pairs alone, we aren’t able to define a universe of
propositions
$\mathsf{NPair}\;\star\;{\color[rgb]{1,0,0}\bm{\mathsf{isProp}}}$, as you’ll
recall that the predicate has type
$\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\star$ at level 1.

$\displaystyle\mathbf{data}\;\mathsf{DPair}{}\;(\mathit{X}:^{\ottsym{0}}\star)\;(\mathit{P}:\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\star):^{\ottsym{1}}\star\;\mathbf{where}$
$\displaystyle\quad\mathsf{MkPair}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\mathit{P}\;\mathit{\mathit{x}}\mathrel{\rightarrow}\mathsf{DPair}\;\mathit{X}\;\mathit{P}$
$\displaystyle\mathsf{dfst}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{P}\\!:^{\ottsym{1}}\\!\ottsym{(}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\star\ottsym{)}\mathpunct{.}\mathsf{DPair}\;\mathit{X}\;\mathit{P}\mathrel{\rightarrow}\mathit{X}$
$\displaystyle\mathsf{dfst}\;\mathit{X}\;\mathit{P}\;\mathit{p}\coloneqq\mathbf{case}\;\mathit{p}\;\mathbf{of}\;\mathsf{MkPair}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\mathrel{\Rightarrow}\mathit{\mathit{x}}$
$\displaystyle\mathsf{dsnd}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{P}\\!:^{\ottsym{1}}\\!\ottsym{(}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\star\ottsym{)}\mathpunct{.}\Pi\mathit{p}\\!:^{\ottsym{1}}\\!\mathsf{DPair}\;\mathit{X}\;\mathit{P}\mathpunct{.}{}$
$\displaystyle\phantom{dsnd\mathrel{:^{2}}}\mathbf{case}\;\mathit{p}\;\mathbf{of}\;\mathsf{MkPair}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\mathrel{\Rightarrow}\mathit{P}\;\mathit{\mathit{x}}$
$\displaystyle\mathsf{dsnd}\;\mathit{X}\;\mathit{P}\;\mathit{p}\coloneqq\mathbf{case}\;\mathit{p}\;\mathbf{of}\;\mathsf{MkPair}\;\mathit{\mathit{x}}\;\mathit{\mathit{y}}\mathrel{\Rightarrow}\mathit{\mathit{y}}$

In the second variant of dependent pairs where $P$ is a stratified dependent
function type, the domain of $P$ is fixed to level 0, so in the type in
$\mathsf{dsnd}$, it can’t be applied to the first projection, but it can still
be applied to the first component by matching on the pair. Now we’re able to
define $\mathsf{DPair}\;\star\;\mathsf{isProp}$. In both cases, the first
component has a fixed level, while the second component is floating, so using
a predicate at a higher level results in a pair type at a higher level by
subsumption. Consider the predicate $\mathsf{isSet}$, which has type
$\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\star$ at level 2: the
universe of sets $\mathsf{DPair}\;\star\;\mathsf{isSet}$ is also well typed at
level 2. Unfortunately, the first projection $\mathsf{dfst}$ can no longer be
used on an element of this pair, since the predicate is now at level 2, nor
can its displacement $\mathsf{dfst}^{\ottsym{1}}$, since that would displace
the level of the first component as well. Without proper level polymorphism,
which would allow keeping the first argument’s level fixed while setting the
second argument’s level to 2, we’re forced to write a whole new first
projection function. In general, this limitation occurs whenever a datatype
contains both dependent and nondependent parameters. Nevertheless, in the case
of the pair type, the flexibility of a nondependent second component type is
still preferable to a dependent one that fixes its level, since there would
need to be entirely separate datatype definitions for different combinations
of first and second component levels, i.e. one with levels 0 and 1 (as in the
case of $\mathsf{isProp}$), one with levels 0 and 2 (as in the case of
$\mathsf{isSet}$), and so on.

##  6\. On consistency

In this section, we delve into the design of StraTT and the implementation as
they relate to logical consistency, i.e. the absence of a closed inhabitant of
$\bot$.

###  6.1. Level annotations

The lack of level annotations on unstratified nondependent function types
lends to them their flexibility with respect to cumulativity. A declared
function $\mathit{f}:^{\ottsym{0}}\ottnt{A}\mathrel{\rightarrow}\ottnt{B}$
taking and returning a term at level 0 can, by subsumption, be used as a
function taking and returning a term at _any_ higher level so long as the
input and output levels match. It may be tempting to remove the level
annotation on dependent function types as well, so that they enjoy the same
flexibility as long as the output level is strictly greater than the input
level, but this recovers impredicativity, thus defeating the purpose of
stratification. Supposing the level annotations are removed and that we have
some well-typed function type
$\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}$ at level 1, the
following derivation is valid.

$\displaystyle\displaystyle{\hbox{\hskip
135.76463pt\vbox{\hbox{\hskip-135.76462pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}\vdash\mathit{\mathit{f}}:^{\ottsym{2}}\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}\qquad\mathit{f}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}\vdash\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}:^{\ottsym{1}}\star$}}}\vbox{}}}\over\hbox{\hskip
117.23299pt\vbox{\vbox{}\hbox{\hskip-117.23297pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f}:^{\ottsym{1}}\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}\vdash\mathit{\mathit{f}}\;\ottsym{(}\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}\ottsym{)}:^{\ottsym{2}}\ottnt{B}\mathopen{\\{}\Pi\mathit{\mathit{x}}\\!:\\!\star\mathpunct{.}\ottnt{B}/\mathit{\mathit{x}}\mathclose{\\}}$}}}}}}$

Without the level annotation, the application rule for dependent functions now
applies merely whenever the argument is typed at a level strictly lower than
the function, allowing our function type to be substituted into its own
codomain. With both impredicativity and type-in-type, this system would be no
different from an unstratified system with type-in-type, allowing us to derive
an inconsistency.

###  6.2. Constructor levels

In the implementation, a datatype definition is valid if, among the other
rules discussed, the level of the constructors cannot be higher than that of
the datatype itself. If the level were allowed to be higher, while regularity
wouldn’t be violated, it would yet again be possible to derive an
inconsistency. We demonstrate this with a variant of Burali-Forti’s paradox
(Burali–Forti, 1897) concerning the simultaneous well-foundedness and
non–well-foundedness of particular datatype $\mathsf{U}$.242424This example
was provided by Stephen Dolan in private correspondence.,252525impl/pi/WFU.pi

$\displaystyle\mathbf{data}\;\mathsf{U}{}:^{\ottsym{0}}\star\;\mathbf{where}$
$\displaystyle\quad\mathsf{MkU}:^{\ottsym{1}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\ottsym{(}\mathit{X}\mathrel{\rightarrow}\mathsf{U}\ottsym{)}\mathrel{\rightarrow}\mathsf{U}$

While $\mathsf{MkU}$ is assigned level 1, we consider the possibility of
assigning level 0 to its type $\mathsf{U}$. Note that this definition is
strictly positive, so we aren’t using any tricks relying on negative
datatypes. Next, we define a well-foundedness predicate for $\mathsf{U}$.

$\displaystyle\mathbf{data}\;\mathsf{WF}{}:^{\ottsym{2}}\Pi\mathit{u}\\!:^{\ottsym{1}}\\!\mathsf{U}\mathpunct{.}\star\;\mathbf{where}$
$\displaystyle\quad\mathsf{MkWF}:^{\ottsym{2}}\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\Pi\mathit{\mathit{f}}\\!:^{\ottsym{1}}\\!\mathit{X}\mathrel{\rightarrow}\mathsf{U}\mathpunct{.}\ottsym{(}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{1}}\\!\mathit{X}\mathpunct{.}\mathsf{WF}\;\ottsym{(}\mathit{\mathit{f}}\;\mathit{\mathit{x}}\ottsym{)}\ottsym{)}$
$\displaystyle\quad\phantom{\mathsf{MkWF}\mathrel{:^{2}}}\rightarrow\mathsf{WF}\;\ottsym{(}\mathsf{MkU}\;\mathit{X}\;\mathit{\mathit{f}}\ottsym{)}$

This definition is strictly positive as well, while the constructor’s level is
_not_ greater than that of the datatype. It’s easy to show that all
$\mathsf{U}$ are well founded.

$\displaystyle\mathsf{wf}:^{\ottsym{2}}\Pi\mathit{u}\\!:^{\ottsym{1}}\\!\mathsf{U}\mathpunct{.}\mathsf{WF}\;\mathit{u}$
$\displaystyle\mathsf{wf}\;\mathit{u}\coloneqq\mathbf{case}\;\mathit{u}\;\mathbf{of}$
$\displaystyle\quad\mathsf{MkU}\;\mathit{X}\;\mathit{\mathit{f}}\mathrel{\Rightarrow}\mathsf{MkWF}\;\mathit{X}\;\mathit{\mathit{f}}\;\ottsym{(}\lambda\mathit{\mathit{x}}\mathpunct{.}\mathsf{wf}\;\ottsym{(}\mathit{\mathit{f}}\;\mathit{\mathit{x}}\ottsym{)}\ottsym{)}$

However, with $\mathsf{U}$ typeable at level 0, we’re able to construct an
inhabitant that is provably _not_ well founded.

$\displaystyle\mathsf{loop}:^{\ottsym{1}}\mathsf{U}$
$\displaystyle\mathsf{loop}\coloneqq\mathsf{MkU}\;\mathsf{U}\;\ottsym{(}\lambda\mathit{u}\mathpunct{.}\mathit{u}\ottsym{)}$
$\displaystyle\mathsf{nwfLoop}:^{\ottsym{2}}\mathsf{WF}\;\mathsf{loop}\mathrel{\rightarrow}\bot$
$\displaystyle\mathsf{nwfLoop}\;\mathit{wfLoop}\coloneqq\mathbf{case}\;\mathit{wfLoop}\;\mathbf{of}$
$\displaystyle\quad\mathsf{MkWF}\;\mathit{X}\;\mathit{\mathit{f}}\;\mathit{h}\mathrel{\Rightarrow}\mathsf{nwfLoop}\;\ottsym{(}\mathit{h}\;\mathsf{loop}\ottsym{)}$

In the branch of $\mathsf{nwfLoop}$, by pattern matching on the type of the
scrutinee, $X$ is bound to $\mathsf{U}$ and $\mathit{f}$ to
$\lambda\mathit{u}\mathpunct{.}\mathit{u}$, so $\mathit{h}\;\mathsf{loop}$
correctly has type $\mathsf{WF}\;\mathsf{loop}$. Note that this definition
would also pass the usual structural termination check, since the recursive
call is done on a subargument from $h$. Then
$\mathsf{nwfLoop}\;\ottsym{(}\mathsf{wf}\;\mathsf{loop}\ottsym{)}$ is an
inhabitant of the empty type. By restricting the level of the constructor to
the level of its datatype, the level of $\mathsf{U}$ must be 1, so the key
problematic definition $\mathsf{loop}$ is immediately disallowed. A similar
phenomenon occurs when trying to implement a variant of Russell’s paradox
(Russell, 1903), making use of the same $\mathsf{U}$ above (with its level as
1).262626This formulation is due to Paolo Capriotti (Devriese, 2013), and the
Agda implementation can be found at
https://github.com/agda/agda/blob/master/test/Succeed/Russell.agda.,272727impl/pi/Russell.pi
First, a $\mathsf{U}$ is said to be regular if it’s provably inequal to its
subarguments; this represents a set which doesn’t contain itself.

$\displaystyle\mathsf{regular}:^{\ottsym{1}}\mathsf{U}\mathrel{\rightarrow}\star$
$\displaystyle\mathsf{regular}\;\mathit{u}\coloneqq\mathbf{case}\;\mathit{u}\;\mathbf{of}$
$\displaystyle\quad\mathsf{MkU}\;\mathit{X}\;\mathit{\mathit{f}}\mathrel{\Rightarrow}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{0}}\\!\mathit{X}\mathpunct{.}\ottsym{(}\mathit{\mathit{f}}\;\mathit{\mathit{x}}=\mathsf{MkU}\;\mathit{X}\;\mathit{\mathit{f}}\ottsym{)}\mathrel{\rightarrow}\bot$

The trick is to define a $\mathsf{U}$ that is both regular and nonregular.
Normally, with type-in-type, this would be one that represents the set of all
regular sets.

$\displaystyle\mathsf{R}:^{\ottsym{3}}\mathsf{U}^{\ottsym{2}}$
$\displaystyle\mathsf{R}\coloneqq\mathsf{MkU}^{\ottsym{2}}\;\ottsym{(}\mathsf{NPair}^{\ottsym{1}}\;\mathsf{U}\;\mathsf{regular}\ottsym{)}\;{\color[rgb]{1,0,0}\bm{\ottsym{(}\mathsf{nfst}^{\ottsym{1}}\;\mathsf{U}\;\mathsf{regular}\ottsym{)}}}$

Stratification once again prevents $\mathsf{R}$ from type checking, since the
pair projection returns a $\mathsf{U}$ and not a $\mathsf{U}^{\ottsym{2}}$.
The type contained in the pair can’t be displaced to $\mathsf{U}^{\ottsym{2}}$
either, since that would make the pair’s level too large to fit inside
$\mathsf{MkU}^{\ottsym{2}}$.

###  6.3. Hurkens’ paradox

Although we’ve seen that stratification thwarts the paradoxes in 6.2, that
paradox leverages the properties of datatypes and recursive functions, which
we haven’t formalized. Here, we’ll turn to the failure of Hurkens’ paradox as
further evidence of consistency, which in contrast can be formulated in pure
StraTT without datatypes. Below is the paradox in Coq without universe
checking.

⬇

Require Import Coq.Unicode.Utf8_core.

Unset Universe Checking.

Definition P (X : Type) : Type := X → Type.

Definition U : Type :=

∀ (X : Type), (P (P X) → X) → P (P X).

Definition tau (t : P (P U)) : U :=

λ X f p, t (λ s, p (f (s X f))).

Definition sig (s : U) : P (P U) := s U tau.

Definition Delta (y : U) : Type :=

(∀ (p : P U), sig y p → p (tau (sig y))) → False.

Definition Omega : U :=

tau (λ p, ∀ (x : U), sig x p → p x).

Definition M (x : U) (s : sig x Delta) : Delta x :=

λ d, d Delta s (λ p, d (λ y, p (tau (sig y)))).

Definition D := ∀ p, (∀ x, sig x p → p x) → p Omega.

Definition R : D :=

λ p d, d Omega (λ y, d (tau (sig y))).

Definition L (d : D) : False :=

d Delta M (λ p, d (λ y, p (tau (sig y)))).

Definition false : False := L R.

If we replace unsetting universe checking with

⬇

Set Universe Polymorphism.

then the definitions check up to

    M}.
    The corresponding \lang code, too, checks up to $ \mathsf

M $,asverifiedintheimplementation.\@add@raggedright\@add@raggedright
Displacementissufficienttohandlesituationsinwhichpolymorphismwasneeded,andexplicitlyindicateswhere.\allowdisplaybreaks\begin{aligned}
&\mathsf{P}:^{\ottsym{0}}\star\mathrel{\rightarrow}\star\\\
&\mathsf{P}\;\mathit{X}\coloneqq\mathit{X}\mathrel{\rightarrow}\star\\\
&\mathsf{U}:^{\ottsym{1}}\star\\\
&\mathsf{U}\coloneqq\Pi\mathit{X}\\!:^{\ottsym{0}}\\!\star\mathpunct{.}\ottsym{(}\mathsf{P}\;\ottsym{(}\mathsf{P}\;\mathit{X}\ottsym{)}\mathrel{\rightarrow}\mathit{X}\ottsym{)}\mathrel{\rightarrow}\mathsf{P}\;\ottsym{(}\mathsf{P}\;\mathit{X}\ottsym{)}\\\
&\mathsf{tau}:^{\ottsym{1}}\mathsf{P}\;\ottsym{(}\mathsf{P}\;\mathsf{U}\ottsym{)}\mathrel{\rightarrow}\mathsf{U}\\\
&\mathsf{tau}\;\mathit{t}\;\mathit{X}\;\mathit{\mathit{f}}\;\mathit{p}\coloneqq\mathit{t}\;\ottsym{(}\lambda\mathit{s}\mathpunct{.}\mathit{p}\;\ottsym{(}\mathit{\mathit{f}}\;\ottsym{(}\mathit{s}\;\mathit{X}\;\mathit{\mathit{f}}\ottsym{)}\ottsym{)}\ottsym{)}\\\
&\mathsf{sig}:^{\ottsym{2}}\mathsf{U}^{\ottsym{1}}\mathrel{\rightarrow}\mathsf{P}\;\ottsym{(}\mathsf{P}\;\mathsf{U}\ottsym{)}\\\
&\mathsf{sig}\;\mathit{s}\coloneqq\mathit{s}\;\mathsf{U}\;\mathsf{tau}\\\
&\mathsf{Delta}:^{\ottsym{2}}\mathsf{P}\;\mathsf{U}^{\ottsym{1}}\\\
&\mathsf{Delta}\;\mathit{\mathit{y}}\coloneqq\ottsym{(}\Pi\mathit{p}\\!:^{\ottsym{1}}\\!\mathsf{P}\;\mathsf{U}\mathpunct{.}\mathsf{sig}\;\mathit{\mathit{y}}\;\mathit{p}\mathrel{\rightarrow}\mathit{p}\;\ottsym{(}\mathsf{tau}\;\ottsym{(}\mathsf{sig}\;\mathit{\mathit{y}}\ottsym{)}\ottsym{)}\ottsym{)}\mathrel{\rightarrow}\bot\\\
&\mathsf{Omega}:^{\ottsym{3}}\mathsf{U}\\\
&\mathsf{Omega}\coloneqq\mathsf{tau}\;\ottsym{(}\lambda\mathit{p}\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{2}}\\!\mathsf{U}^{\ottsym{1}}\mathpunct{.}\mathsf{sig}\;\mathit{\mathit{x}}\;\mathit{p}\mathrel{\rightarrow}\mathit{p}\;\ottsym{(}\lambda\mathit{X}\mathpunct{.}\mathit{\mathit{x}}\;\mathit{X}\ottsym{)}\ottsym{)}\\\
&\mathsf{M}:^{\ottsym{4}}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{3}}\\!\mathsf{U}^{\ottsym{2}}\mathpunct{.}\mathsf{sig}^{\ottsym{1}}\;\mathit{\mathit{x}}\;\mathsf{Delta}\mathrel{\rightarrow}\mathsf{Delta}^{\ottsym{1}}\;\mathit{\mathit{x}}\\\
&\mathsf{M}\;\mathit{\mathit{x}}\;\mathit{s}\;\mathit{d}\coloneqq\mathit{d}\;\mathsf{Delta}\;\mathit{s}\;\ottsym{(}\lambda\mathit{p}\mathpunct{.}\mathit{d}\;\ottsym{(}\lambda\mathit{\mathit{y}}\mathpunct{.}\mathit{p}\;\ottsym{(}\mathsf{tau}\;\ottsym{(}\mathsf{sig}\;\mathit{\mathit{y}}\ottsym{)}\ottsym{)}\ottsym{)}\ottsym{)}\\\
&\mathsf{D}:^{\ottsym{3}}\star\\\
&\mathsf{D}\coloneqq\Pi\mathit{p}\\!:^{\ottsym{1}}\\!\mathsf{P}\;\mathsf{U}\mathpunct{.}\ottsym{(}\Pi\mathit{\mathit{x}}\\!:^{\ottsym{1}}\\!\mathsf{U}\mathpunct{.}\mathsf{sig}\;{\color[rgb]{1,0,0}\bm{\mathit{\mathit{x}}}}\;\mathit{p}\mathrel{\rightarrow}\mathit{p}\;\mathit{\mathit{x}}\ottsym{)}\mathrel{\rightarrow}\mathit{p}\;\mathsf{Omega}\end{aligned}\par
Thenextdefinition$282828impl/pi/Hurkens.pi (no annotations),
impl/pi/HurkensAnnot.pi (all annotations) D  $doesn^{\prime}ttypecheck,since$
sig  $takesadisplaced$ U ^ 1 $andnota$ U
$.Thetypeof$x$can^{\prime}tbedisplacedtofixthiseither,since$p$takesanundisplaced$
U  $andnota$ U ^ 1
$.Beingstucktryingtoequatetwodifferentlevelsisreassuring,asconflatingdifferentuniverselevelsishowweexpectaparadoxthatexploitstype-
in-typetooperate.\par$

###  6.4. Proof attempt

The main difficulty in proving consistency via a semantic model of StraTT is
the interpretation of the nondependent function type in the presence of
cumulativity. Continuing with the framework from Section 2.1, recall that for
each level $k$ we have a collection $\mathsf{U}_{k}$ of codes of types of
StraTT and a mapping $\mathsf{el}_{k}$ from codes into the semantic domain.
Now let $\eta$ be a mapping from variables into the semantic domain, and
consider the following fragment of an interpretation from StraTT terms into
the semantic domain.

$\displaystyle\left\llbracket\mathit{x}\right\rrbracket^{k}\eta$
$\displaystyle=\eta(x)$
$\displaystyle\left\llbracket\Pi\mathit{\mathit{x}}\\!:^{\ottnt{j}}\\!\ottnt{A}\mathpunct{.}\ottnt{B}\right\rrbracket^{k}\eta$
$\displaystyle=\hat{\Pi}_{k}(j<k,\left\llbracket\ottnt{A}\right\rrbracket^{j}\eta,x\mapsto\left\llbracket\ottnt{B}\right\rrbracket^{k}\langle\eta,x\rangle)$
$\displaystyle\left\llbracket\ottnt{A}\mathrel{\rightarrow}\ottnt{B}\right\rrbracket^{k}\eta$
$\displaystyle=\hat{\rightarrow}_{k}(\left\llbracket\ottnt{A}\right\rrbracket^{k}\eta,\left\llbracket\ottnt{B}\right\rrbracket^{k}\eta)$
$\displaystyle\left\llbracket\bot\right\rrbracket^{k}\eta$
$\displaystyle=\hat{\bot}_{k}$

Here, we have codes $\hat{\Pi}$, $\hat{\rightarrow}_{k}$, and $\hat{\bot}_{k}$
in $\mathsf{U}_{k}$. Our fundamental lemma then states the following,
disregarding any issues regarding weakening of contexts and $\eta$ mappings.

###### Lemma 6.0 (Fundamental lemma).

Let $\eta$ be a mapping such that for every
$\mathit{x}\\!:\\!^{\ottnt}{j}\ottnt{A}\in\Gamma$,
$\eta(x)\in\mathsf{el}_{j}(\left\llbracket A\right\rrbracket^{j}\eta)$. If
$\Gamma\vdash\ottnt{a}:^{\ottnt{k}}\ottnt{A}$, then
$\left\llbracket\ottnt{a}\right\rrbracket^{k}\eta\in\mathsf{el}_{k}(\left\llbracket\ottnt{A}\right\rrbracket^{k}\eta)$.

Consistency arises from the fundamental lemma combined with the appropriate
definition of $\mathsf{el}_{k}(\hat{\bot}_{k})$, which in the Agda model would
be Agda’s empty type. The fundamental lemma is proven by induction on the
typing derivation. In the rule DT-Var case, we have that
$\left\llbracket\mathit{x}\right\rrbracket^{k}\eta=\eta(x)\in\mathsf{el}_{j}(\left\llbracket\ottnt{A}\right\rrbracket^{j})$,
while we need to show that
$\left\llbracket\mathit{x}\right\rrbracket^{k}\eta\in\mathsf{el}_{k}(\left\llbracket\ottnt{A}\right\rrbracket^{k})$.
We thus need a lemma stating that cumulativity is preserved.

###### Lemma 6.0 (Preservation of cumulativity).

Suppose $j\leq k$. If
$a\in\mathsf{el}_{j}(\left\llbracket\ottnt{A}\right\rrbracket^{j}\eta)$ then
$a\in\mathsf{el}_{k}(\left\llbracket\ottnt{A}\right\rrbracket^{k}\eta)$.

We proceed by induction on the structure of $\ottnt{A}$. With some unfolding,
we can see the case of
$\Pi\mathit{\mathit{x}}\\!:^{\ottnt{j}}\\!\ottnt{A}\mathpunct{.}\ottnt{B}$
poses no issue, since the level of its domain is fixed. In the case of
$\ottnt{A}\mathrel{\rightarrow}\ottnt{B}$, we need to show that if
$f\in\mathsf{el}_{j}(\hat{\rightarrow}_{j}(\left\llbracket\ottnt{A}\right\rrbracket^{j},\left\llbracket\ottnt{B}\right\rrbracket^{j}))$,
then
$f\in\mathsf{el}_{k}(\hat{\rightarrow}_{k}(\left\llbracket\ottnt{A}\right\rrbracket^{k},\left\llbracket\ottnt{B}\right\rrbracket^{k}))$,
with the induction hypotheses stating that if
$a\in\mathsf{el}_{j}(\left\llbracket\ottnt{A}\right\rrbracket^{j})$ then
$a\in\mathsf{el}_{k}(\left\llbracket\ottnt{A}\right\rrbracket^{k})$, and
similarly for $\ottnt{B}$. Since terms of type
$\ottnt{A}\mathrel{\rightarrow}\ottnt{B}$ behave like functions, we expect
that the interpretation of $\hat{\rightarrow}$ codes behaves like a function
space. However, to prove our goal, we require that they not be contravariant
in the domain with respect to cumulativity, as expected from a function space,
but _covariant_! Concretely, in the Agda model, supposing we have an
interpretation function ` $\llbracket$ A  $\rrbracket$ k  $\upeta$ : U k`
given a representation of a StraTT term `A`, a level `k`, and a mapping `
$\upeta$ `, we would need to show that given a function

⬇

f : el j (⟦ A ⟧ j η) → el j (⟦ B ⟧ j η)

and an element `a : el k (  $\llbracket$ A  $\rrbracket$ k  $\upeta$ )`, we
have some element in `el k (  $\llbracket$ B  $\rrbracket$ k  $\upeta$ )`, but
the application `f a` is ill typed, and we can’t demote `a` to a lower level.
One solution would be to change the interpretation of nondependent functions
to bake in cumulativity, something along the lines of
$\ottnt{A}\mathrel{\rightarrow}\ottnt{B}=\hat{\rightarrow}_{k}(i\geq
k,\left\llbracket\ottnt{A}\right\rrbracket^{i},\left\llbracket\ottnt{B}\right\rrbracket^{i})$,
but this would prevent $\mathsf{U}_{k}$ and $\mathsf{el}_{k}$ from being well
defined by well-founded induction on $k$. We are thus at an impasse among
stratified dependent functions, floating nondependent functions, and
cumulativity, all of which are fundamental features of StraTT.

##  7\. Related Work

StraTT is directly inspired from Leivant’s stratified polymorphism (Leivant,
1989, 1991; Danner and Leivant, 1999), which developed from the ramified
polymorphic typed $\lambda$-calculus briefly introduced by Statman (1981).
Stratified System F, a slight modification of the original system, has since
been used to demonstrate a normalization proof technique using hereditary
substitution (Eades III and Stump, 2010), which in turn has been mechanized in
Coq as a case study for the Equations package (Mangin and Sozeau, 2015). More
recently, an interpreter of an intrinsically-typed Stratified System F has
been mechanized in Agda (Thiemann and Weidner, 2023), where stratification
levels are interpreted as Agda’s universe levels. Similarly, Hubers and Morris
(2023) model in Agda a stratification of $\mathrm{R}_{\omega}$, which is a
System $\mathrm{F}_{\omega}$ with row types. Meanwhile, our system of level
displacement comes from McBride’s crude but effective stratification (McBride,
2011, 2002), following Hou et al.(2023)Hou (Favonia), Angiuli, and Mullanix
(Favonia) and specializing the displacement algebra to the naturals.

##  8\. Conclusion

In this work, we have introduced Stratified Type Theory, a departure from a
decades-old tradition of universe hierarchies without, we believe, succumbing
to the threat of logical inconsistency. By stratifying dependent function
types, we obstruct the usual avenues by which paradoxes manifest their
inconsistencies; and by separately introducing floating nondependent function
types, we recover some of the expressivity lost under the strict rule of
stratification. Although proving logical consistency for the full StraTT
remains a challenge for future work, we have provided extensive evidence
supporting our conjecture of consistency by showing how well-known type-
theoretic paradoxes fail. Towards demonstrating that StraTT isn’t a mere
theoretical exercise and, if consistent, is a viable basis for theorem proving
and dependently-typed programming, we have implemented a prototype type
checker for the language augmented with datatypes, along with a small core
library. The implementation also features inference for level annotations and
displacements, allowing the user to omit them entirely, but demonstrating that
inference is complete remains future work. We also leave formally ensuring
that our rules for datatypes don’t violate existing metatheoretical properties
as future work. We have chosen level displacement over level polymorphism for
its simplicity, expressivity, and extensibility. Although we fix levels to the
naturals in both the proof mechanization (to take advantage of Coq’s
arithmetic tactics) and the Haskell implementation (to enable solving level
metavariable constraints), it should be possible to use any displacement
algebra in the sense of Hou et al.(2023)Hou (Favonia), Angiuli, and Mullanix
(Favonia). This opens future exploration with, for instance, transfinite
levels, as are used in transfinite stratified polymorphism (Danner and
Leivant, 1999). Even so, nothing precludes adopting explicit level
polymorphism in place of displacement. This raises interesting questions, such
as at what level a term like
$\Lambda\ell\mathpunct{.}\Pi\mathit{\mathit{x}}\\!:^{\ell}\\!\ottnt{A}\mathpunct{.}\ottnt{B}$
should be typed, or whether a consistency proof would be further complicated
by needing to model such terms. Ultimately, we hope that StraTT demonstrates
the feasibility of a renewed alternative to how type universes are handled,
and opens up fresh avenues in the design space of type theories for proof
assistants.

## References

  * Barendregt [1984] Henk P. Barendregt.  _The Lambda Calculus: Its Syntax and Semantics_.  Studies in Logic and the Foundations of Mathematics. North-Holland, 1984\.
  * Böhm and Berarducci [1985] Corrado Böhm and Alessandro Berarducci.  Automatic synthesis of typed $\lambda$-programs on term algebras.  _Theoretical Computer Science_ , 39:135–154, 1985.
  * Brady [2011] Edwin C. Brady.  Idris — Systems Programming Meets Full Dependent Types.  In _Programming Languages Meets Program Verification_ , pages 43–54. Association for Computing Machinery, January 2011.  ISBN 9781450304870.  doi:10.1145/1929529.1929536.
  * Burali–Forti [1897] Cesare Burali–Forti.  Una questione sui numeri transfiniti.  _Rendiconti del Circolo matematico di Palermo_ , 11, 1897.
  * Clifton [2015] Andrew V. Clifton.  _Arend — Proof-assistant assisted pedagogy_.  Master’s thesis, California State University, Fresno, California, USA, 2015.  URL https://staffwww.fullcoll.edu/aclifton/files/arend-report.pdf.
  * Coq Development Team [2022] The Coq Development Team.  The Coq Proof Assistant, January 2022.  URL https://coq.github.io/doc/v8.15/refman.
  * Danner and Leivant [1999] Normal Danner and Daniel Leivant.  Stratified polymorphism and primitive recursion.  _Mathematical Structures in Computer Science_ , 9(4):507–522, 1999.  doi:10.1017/S0960129599002868.
  * de Moura et al. [2015] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer.  The Lean Theorem Prover (System Description).  In _International Conference on Automated Deduction_ , volume 9195 of _Lecture Notes in Computer Science_ , pages 378–388, August 2015\.  ISBN 978-3-319-21400-9, 978-3-319-21401-6.  doi:10.1007/978-3-319-21401-6_26.
  * Devriese [2013] Dominique Devriese.  [Agda] Simple contradiction from type-in-type, March 2013.  URL https://lists.chalmers.se/pipermail/agda/2013/005164.html.
  * Dybjer [1996] Peter Dybjer.  Internal type theory.  In Stefano Berardi and Mario Coppo, editors, _Types for Proofs and Programs_ , volume 1158, pages 120–134. Springer Berlin Heidelberg, 1996.  ISBN 978-3-540-61780-8 978-3-540-70722-6.  doi:10.1007/3-540-61780-9_66.
  * Eades III and Stump [2010] Harley Eades III and Aaron Stump.  Hereditary substitution for stratified System F.  In _International Workshop on Proof Search in Type Theories_ , 2010\.  URL https://hde.design/includes/pubs/PSTT10.pdf.
  * Girard [1972] Jean-Yves Girard.  _Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur_.  PhD dissertation, Université Paris VII, 1972.
  * Hou et al.(2023)Hou (Favonia), Angiuli, and Mullanix [Favonia] Kuen-Bang Hou (Favonia), Carlo Angiuli, and Reed Mullanix.  An Order-Theoretic Analysis of Universe Polymorphism.  _Proc. ACM Program. Lang._ , 7(POPL), January 2023.  doi:10.1145/3571250.
  * Hubers and Morris [2023] Alex Hubers and J. Garrett Morris.  Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc.  _Proceedings of the ACM on Programming Languages_ , 7(ICFP):356–384, Aug 2023.  ISSN 2475-1421.  doi:10.1145/3607843.
  * Hurkens [1995] Antonius J. C. Hurkens.  A simplification of Girard’s paradox.  In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, _Typed Lambda Calculi and Applications_ , pages 266–278, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.  ISBN 978-3-540-49178-1.
  * Kovács [2022] András Kovács.  Generalized Universe Hierarchies and First-Class Universe Levels.  In Florin Manea and Alex Simpson, editors, _30th EACSL Annual Conference on Computer Science Logic (CSL 2022)_ , volume 216 of _Leibniz International Proceedings in Informatics (LIPIcs)_ , pages 28:1–28:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  ISBN 978-3-95977-218-1.  doi:10.4230/LIPIcs.CSL.2022.28.  URL https://drops.dagstuhl.de/opus/volltexte/2022/15748.
  * Leibniz [1686] Gottfried Wilhelm Leibniz.  Discours de métaphysique, 1686.
  * Leivant [1989] Daniel Leivant.  Stratified polymorphism.  In _[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science_ , pages 39–47, 1989.  doi:10.1109/LICS.1989.39157.
  * Leivant [1991] Daniel Leivant.  Finitely stratified polymorphism.  _Information and Computation_ , 93(1):93–113, 1991.  ISSN 0890-5401.  doi:10.1016/0890-5401(91)90053-5.  Selections from 1989 IEEE Symposium on Logic in Computer Science.
  * Mangin and Sozeau [2015] Cyprien Mangin and Matthieu Sozeau.  Equations for Hereditary Substitution in Leivant’s Predicative System F: A Case Study.  In _Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice_ , volume 185 of _EPTCS_ , Berlin, Germany, August 2015.  doi:10.4204/EPTCS.185.5.  URL https://hal.inria.fr/hal-01248807.
  * Martin-Löf [1971] Per Martin-Löf.  A theory of types, 1971.
  * Martin-Löf [1972] Per Martin-Löf.  An intuitionistic theory of types, 1972.
  * McBride [2002] Conor McBride.  Crude but Effective Stratification, 2002.  URL https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf.
  * McBride [2011] Conor McBride.  Crude but Effective Stratification, 2011.  URL https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html.
  * Norell [2007] Ulf Norell.  _Towards a practical programming language based on dependent type theory_.  PhD thesis, Chalmers University of Technology and Göteborg University, Göteborg, Sweden, 2007.  URL https://research.chalmers.se/en/publication/46311.
  * Reynolds [1974] John C. Reynolds.  Towards a theory of type structure.  In B. Robinet, editor, _Programming Symposium_ , pages 408–425, Berlin, Heidelberg, 1974. Springer Berlin Heidelberg.  ISBN 978-3-540-37819-8.
  * Reynolds [1984] John C. Reynolds.  Polymorphism is not set-theoretic.  In Gilles Kahn, David B. MacQueen, and Gordon Plotkin, editors, _Semantics of Data Types_ , pages 145–156, Berlin, Heidelberg, 1984. Springer Berlin Heidelberg.  ISBN 978-3-540-38891-3.
  * Russell [1903] Bertrand Russell.  _The Principles of Mathematics_.  Cambridge University Press, 1903.
  * Statman [1981] Richard Statman.  Number theoretic functions computable by polymorphic programs.  In _22nd Annual Symposium on Foundations of Computer Science (SFCS 1981)_ , pages 279–282, 1981.  doi:10.1109/SFCS.1981.24.
  * Swamy et al. [2016] Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin.  Dependent Types and Multi-Monadic Effects in F∗.  In _Principles of Programming Languages_ , pages 256–270, January 2016.  ISBN 978-1-4503-3549-2.  doi:10.1145/2837614.2837655.
  * Thiemann and Weidner [2023] Peter Thiemann and Marius Weidner.  Towards Tagless Interpretation of Stratified System F.  In Youyou Cong and Pierre-Evariste Dagand, editors, _TyDe 2023: Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development_ , 2023.  URL https://icfp23.sigplan.org/details/tyde-2023/12/.
  * Univalent Foundations Program [2013] The Univalent Foundations Program.  _Homotopy Type Theory: Univalent Foundations of Mathematics_.  Institute for Advanced Study, 2013.  URL https://homotopytypetheory.org/book.
  * Weirich [2023] Stephanie Weirich.  Implementing Dependent Types in pi-forall, 2023.  URL https://arxiv.org/abs/2207.02129.

##  Appendix A Well-formedness and equality

  * $\vdash\Delta$ (_Signature formation_)

(D-Empty?)(D-Cons?)

  * $\Delta\vdash\Gamma$ (_Context formation_)

(DG-Empty?)(DG-Cons?)

  * $\Delta\vdash\ottnt{a}\equiv\ottnt{b}$ (_Definitional equality_)

(DE-Refl?)(DE-Sym?)(DE-Trans?)(DE-Beta?)(DE-Eta?)(DE-Delta?)(DE-Arrow?)(DE-
Pi?)(DE-Abs?)(DE-App?)(DE-Absurd?)

Figure 3. Signature formation, context formation, and definitional equality
rules