POPL23.tex

%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For double-blind review submission, w/ CCS and ACM Reference
%\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
%% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For single-blind review submission, w/ CCS and ACM Reference
%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true}
%% For final camera-ready submission, w/ required CCS and ACM Reference
%\documentclass[acmsmall]{acmart}\settopmatter{}


%% Journal information
%% Supplied to authors by publisher for camera-ready submission;
%% use defaults for review submission.
\acmJournal{PACMPL}
\acmVolume{7}
\acmNumber{POPL}
\acmArticle{0}
\acmYear{2023}
\acmMonth{1}
\acmDOI{} % \acmDOI{10.1145/nnnnnnn.nnnnnnn}
\startPage{1}

%% Copyright information
%% Supplied to authors (based on authors' rights management selection;
%% see authors.acm.org) by publisher for camera-ready submission;
%% use 'none' for review submission.
\setcopyright{none}
%\setcopyright{acmcopyright}
%\setcopyright{acmlicensed}
%\setcopyright{rightsretained}

%% Bibliography style
\bibliographystyle{ACM-Reference-Format}
\citestyle{acmauthoryear}

%% Packages
\usepackage{style}

%% Newbox in style is too big, so we renew the new
\newlength{\fboxsepdefault}
\setlength{\fboxsepdefault}{\fboxsep}
\renewcommand{\new}[1]{%
  \setlength{\fboxsep}{3pt}%
  \colorbox{newcolour}{#1}%
  \setlength{\fboxsep}{\fboxsepdefault}%
}

%% Tricks for LaTeX shrinking
\setlength{\abovedisplayskip}{1pt}
\setlength{\belowdisplayskip}{1pt}
\setlength{\textfloatsep}{5pt}
\setlength{\intextsep}{5pt}
\setlist{labelindent=\parindent,leftmargin=*}
\captionsetup{skip=5pt}
%\renewcommand{\fbox}[1]{\relax}

%% Title information
\title{A Syntactic Model of Sized Dependent Types}

%% Author information
\author{Jonathan Chan}
\orcid{0000-0003-0830-3180}
\affiliation{
  %\position{}
  \department{Department of Computer Science}
  \institution{University of British Columbia}
  \streetaddress{2329 West Mall}
  \city{Vancouver}
  \state{British Columbia}
  \postcode{V6T 1Z4}
  \country{Canada}
}
\email{jcxz@cs.ubc.ca}
\author{William J. Bowman}
\orcid{0000-0002-6402-4840}
\affiliation{
  \position{Assistant Professor}
  \department{Department of Computer Science}
  \institution{University of British Columbia}
  \streetaddress{2329 West Mall}
  \city{Vancouver}
  \state{British Columbia}
  \postcode{V6T 1Z4}
  \country{Canada}
}
\email{wjb@williamjbowman.com}

%% Abstract
%% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
\begin{abstract}
Contemporary proof assistants based on dependent type theories
restrict nonterminating recursive functions to ensure logical consistency of the type theory
and decidability of type checking.
This is done via guard predicates that only allow stucturally recursive functions
recurring on syntactically smaller arguments.
However, guard predicates are restrictive and reject functions
that aren't structurally recursive but are obviously terminating,
creating extra work for the programmer to convince the guard checker.

An alternative is sized types, a type-based termination checking method
where inductively-defined types are annotated with sizes.
Type checking guarantees that functions recur only on arguments whose types have smaller sizes,
rather than on arguments that syntactically appear smaller,
accepting more terminating functions.
Some existing models of sized dependent type theories
support features for more expressive sized types,
namely higher-rank size quantification
(which allows for passing around size-preserving functions)
and bounded size quantification
(which eliminates the need for complex semi-continuity checks),
but unfortunately none support both simultaneously.

We present a sized dependent type theory with higher-rank and bounded sizes (\lang),
and prove its logical consistency with a syntactic model:
by compiling \lang into the Extensional Calculus of Inductive Constructions (\CICE),
a variant of the type theory on which Coq is based,
and showing that this translation is type preserving,
the consistency of \lang follows from the consistency of \CICE.
\end{abstract}

%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at http://dl.acm.org/ccs/ccs.cfm
\begin{CCSXML}
<ccs2012>
   <concept>
       <concept_id>10003752.10003790.10011740</concept_id>
       <concept_desc>Theory of computation~Type theory</concept_desc>
       <concept_significance>500</concept_significance>
       </concept>
   <concept>
       <concept_id>10003752.10010124.10010125.10010130</concept_id>
       <concept_desc>Theory of computation~Type structures</concept_desc>
       <concept_significance>500</concept_significance>
       </concept>
 </ccs2012>
\end{CCSXML}

\ccsdesc[500]{Theory of computation~Type theory}
\ccsdesc[500]{Theory of computation~Type structures}
%% End of generated code

%% Keywords
%% comma separated list
\keywords{type theory, dependent types, sized types, consistency}

\begin{document}
\maketitle

\section{Introduction} \label{sec:introduction}

In proof assistants such as Coq, Agda, and Idris that are founded on the
types-as-propositions paradigm, logical inconsistency is easily derivable in the
presence of unrestricted recursion:
given the universe $\Prop$ of all propositions,
the recursive function $f = \fun{P}{\Prop}{\app{f}{P}}$ can be assigned the type $\funtype{P}{\Prop}{P}$,
enabling proving any proposition,
and furthermore reduces endlessly:
$$\fun{P}{\Prop}{\app{f}{P}} \ \rhd \ \fun{P}{\Prop}{\app{(\fun{P}{\Prop}{\app{f}{P}})}{P}} \ \rhd \ \fun{P}{\Prop}{\app{f}{P}} \ \rhd \ \dots$$
Therefore, these proof assistants impose restrictions on recursive functions
using \emph{termination checks},
since for their underlying type theories, consistency coincides with the termination of all functions\punctstack{.}%
\footnote{Some proof assistants may be consistent while having nonterminating functions,
such as Lean 3~\citep{impred-proof-irrel}, due to interactions between definitional proof irrelevance
and impredicativity.}

The usual termination checks are done syntactically using a \emph{guardedness check}:
recursion must be done on inductively-defined types,
and recursive calls must occur on syntactic subarguments.
For instance, if a recursive function on naturals is given the successor $\app{\succ*}{n}$,
then it must recur on $n$;
if a recursive function on cons lists is given a nonempty list $\app{\cons*}{\hd}{\tl}$,
then it must recur on the tail $\tl$.

While the guardedness check, being based on the elimination principles of inductive types,
yields terminating functions and a consistent type theory,
it disallows calling some other function on a subargument prior to a recursive call,
even if that function doesn't change the structure of that subargument,
because the input of the recursive call is no longer exactly the syntactic subargument.
For instance, a recursive function on lists cannot first map over the sublist,
even though the usual map function doesn't change the length of a list
and therefore presents no threat to termination.

Some proof assistants (Coq, for one) inline and even unfold recursive functions
so that the guardedness check has more information.
However, this too has disadvantages:
\begin{itemize}
  \item Programs become nonmodular and noncompositional:
    recursive functions that require inlining
    depend on the implementation of inlined functions,
    and a minor syntactic change otherwise equivalent to the original
    can violate guardedness~\citep{CIC-hat-minus}.
  \item As aptly summarized by \citet{coqterm},
    \begin{quote}
    \textit{{\rm [\ldots]} unfold{\rm [ing]} all the definitions used in the body of the function, do{\rm [ing]} reductions, e.t.c.
    {\rm [\ldots]} makes typechecking extremely slow at times.
    Also, the unfoldings can cause the code to bloat by orders of magnitude and become impossible to debug.}
    \end{quote}
\end{itemize}

When the guardedness check fails,
the programmer can refactor the function to recur on a different, related argument,
such as the length of a list in the example above,
but this requires additional work and may bloat programs
with extra code solely for satisfying the guardedness check.
Alternatives that avoid these issues are type-based checks,
where the type system itself is augmented so that type checking
guarantees consistency without syntactically analyzing function bodies.

This paper discusses one alternative, \emph{sized typing}\punctstack{,}%
\footnote{The other common one uses \emph{guarded types}~\citep{guarded-types}.}
where inductive types are annotated with size information,
and constructors construct constructions whose size is larger than that of their arguments:
the notion of a ``smaller'' argument is then encoded within the types.
Finally, a recursive function is well typed only if it recurs on an argument
whose size is smaller than that of the original argument.

Because well typedness is the only required condition,
calling some other function before a recursive call is allowed
as long as that function's type indicates it is \emph{size preserving}.
For example, in the list mapping example,
if the sublist (whose elements have type $\tau$) has size $s$,
then the mapping function must have type $\arr*{\List{\tau}{s}}{\List{\tau}{s}}$.
The implementation of the map isn't required, merely its type, restoring
modularity and compositionality.

We introduce Sizey \textsc{mc}Type Theory (\lang),
a sized dependent type theory that we prove to be logically consistent
and therefore suitable for both recursive programming and theorem proving.
We do so using a \emph{syntactic model}:
\lang is first translated into a target type theory in whose consistency we have more confidence,
and then we prove this translation to be \emph{type preserving}.
By type preservation, consistency of the target type theory implies that of the source.

But what need is there for yet another sized type system?
Since \citet{hughes}, there has been a little over two decades' worth of past work on sized types.
\citet{flationary} notes that it has been the topic of at least five dissertations.
This paper alone names eight different type theories with sized types.
There have been many advancements along the way,
but there still remains many open problems,
especially when it comes to dependent types.

\lang does not aim to resolve all the existing problems with sized types.
Our purpose is twofold:

\begin{itemize}
  \item To fill an existing gap in sized dependent type theories.
    Two modern sized type features are higher-rank and bounded size quantification,
    and there exist a few dependent type theories with one or the other,
    but not both, to our knowledge.
    On the other hand, they are currently in Agda's implementation of sized types.
    By proving the consistency of \lang, a novel type theory with these two features,
    we bring the theoretical state-of-the-art closer to practice,
    while increasing trust in the corresponding sublanguage of sized types in Agda.
  \item To demonstrate the viability of using a syntactic model to prove consistency
    of a sized type theory.
    Doing so from scratch through a set-theoretic model is notoriously difficult,
    and often requires sacrifices to and constraints on the type theory;
    see Sacchini's dissertation~\citep{CIC-hat-minus} or \CIChatstar~\citep{CIC-hat-star},
    for instance.
    Meanwhile, a syntactic model into a similar type theory lets us highlight
    the differences unique to sized types.
\end{itemize}

\subsection{Related Work}

There are many variations on dependent type theory;
in this paper, we refer to five specific works:

\begin{itemize}
  \item The Predicative Calculus of Inductive Constructions~\citep{pCIC} (pCIC)
    is a dependent type theory with a cumulative universe hierarchy,
    definitions, and inductive types.
  \item The Predicative Calculus of Cumulative Inductive Constructions~\citep{pCuIC} (pCuIC)
    further adds cumulativity between inductive types to pCIC.
    It comes the closest to formally describing the underlying type theory of Coq.
  \item The MetaCoq project~\citep{MetaCoq} mechanizes pCuIC
    and some metatheory in Coq.
  \item Martin-L\"of type theory~\citep{MLTT} (MLTT) has a noncumulative universe hierarchy
    along with some basic types:
    the empty type, the unit type, dependent pair types, disjoint sum types,
    a propositional equality type, the naturals, and W types.
  \item Extensional Type Theory~\citep{CICE} (ETT) has a noncumulative universe hierarchy,
    dependent pair types, a propositional equality type,
    and equality reflection.
\end{itemize}

We model \lang in the Extensional Calculus of Inductive Constructions (\CICE),
which is based on pCIC with extensionality inspired by ETT.
On the other hand, \lang is based on MetaCoq's presentation of type theory,
but with naturals and well-founded trees%
\footnote{We refer to the inhabitants of W types as well-founded trees.}
in place of inductive types,
since generalizing to inductive types provides no additional insight for a lot
more irrelevant detail.
Supporting inductive types would be straightforward, since \CICE already supports them.

Sized types have a similarly long history;
the first sized dependent type theory is \CIChat~\citep{CIC-hat}
which adds implicit and fully-inferrable sized types to pCIC.
\cref{tab:sized-types} lists the sized dependent type theories that follow \CIChat,
and the main features we study:
explicit size quantification,
higher-rank size quantification,
bounded size quantification,
and consistency.
We introduce and motivate these features in the next subsection.

\begin{table}[h]
\centering
\small
\begin{tabular}{l c c c c}
Type theory & Explicit sizes? & Higher-rank? & Bounded? & Consistent? \\
\hline
\CIChat~\citep{CIC-hat} & \crossmark & \crossmark & \crossmark & \interromark \\
\CIChatminus~\citep{CIC-hat-minus} & \crossmark & \crossmark & \crossmark & \checkmark* \\
\CChatomega~\citep{CC-hat-omega} & \crossmark & \crossmark & \crossmark & \checkmark* \\
\CIChatl~\citep{CIC-hat-l} & \crossmark & \crossmark & \crossmark & \checkmark* \\
\CIChatsub~\citep{CIC-hat-sub} & \crossmark & \crossmark & \checkmark* & \checkmark* \\
\CIChatstar~\citep{CIC-hat-star} & \crossmark & \crossmark & \crossmark & \interromark \\
\citet{NbE} & \checkmark* & \checkmark* & \crossmark & \checkmark* \\
MiniAgda~\citep{MiniAgda, flationary} & \checkmark* & \checkmark* & \checkmark* & \crossmark \\
\textbf{\lang} & \checkmark* & \checkmark* & \checkmark* & \checkmark*
\end{tabular}
\caption{Sized dependent type theories and their properties}
\label{tab:sized-types}
\end{table}
\vspace{-2ex}

\subsection{Overview}

Sized types consist of explicit size quantification $\Funtype{\alpha}{\tau}$,
size abstraction $\Fun{\alpha}{e}$, and size application $\App{e}{s}$.
Sizes consist of size variables, a base size $\circ$
and a size successor operator $\sss{s}$.
Size expressions are \emph{not} terms,
and their quantifications, abstractions, and applications
are syntactically distinct from those of terms,
similar to how, in nondependent polymorphic type systems,
types are distinct from terms.

Explicit sizes differs from prior sized type systems which,
extending the type polymorphism analogy,
support only implicit \emph{rank-1} or
\emph{prenex} size quantification:
size quantifications never appear inside a type,
and all size abstractions and applications are fully inferred.
Explicit sizes, in contrast, let us express
\emph{higher-rank} size quantification,
which is more expressive.
For instance, consider a list parametrized over some sized type $\tau$:
one could write a size-preserving mapping function over a list
of type
$\Funtype{\alpha}{\arr*{(\Funtype{\beta}{\arr*{\App{\tau}{\beta}}{\App{\tau}{\beta}}})}{\app{\List*}{(\App{\tau}{\alpha})}}{\app{\List*}{(\App{\tau}{\alpha})}}}$.

We also include \emph{bounded} size quantification $\Funtype<{\alpha}{s}{\tau}$
and abstraction $\Fun<{\alpha}{s}{e}$.
An order on sizes is induced by these bound instantiations and the successor operator;
this order has nothing to do with subtyping,
and in particular we do \emph{not} have subtyping relations between
$\N{\alpha}$ and $\N{\sss{\alpha}}$, for instance.
Bounded quantification yields a natural typing rule for fixpoint expressions,
which recur on smaller sizes according to the order:
%
\begin{mathpar}
\inferrule[]{
  \check{\Phi, \alpha; \Gamma, f: \Funtype<{\beta}{\alpha}{\subst{\tau}{\alpha}{\beta}}}{e}{\tau}
}{
  \infer{\Phi; \Gamma}{\fix{f}{\alpha}{\tau}{e}}{\Funtype{\alpha}{\tau}}
}
\end{mathpar}

Without bounded quantification,
occurrences of $\alpha$ in $\tau$ must be restricted by
complex \emph{semi-continuity} requirements to avoid inconsistencies; via
\citet{flationary},
\begin{quote}
\textit{A technical condition like semi-continuity can kill a system
as a candidate for the foundation of logics and programming
{\rm [\ldots]} Most systems for type-based termination replace semi-continuity by a rough approximation,
trading expressivity for simplicity}
\end{quote}

Notably, these three features are all found in Agda's implementation of sized types.
On the other hand, \lang excludes Agda's \emph{infinite size},
since its properties and its use are known to be inconsistent.
While applications of the infinite size to finitely branching
inductives such as naturals and lists can be recovered with \emph{existential size quantification},
this isn't possible for infinitely-branching inductives
such as ordinals and well-founded trees.
We give a concrete example of an inexpressible infinitary construct in \cref{subsec:examples:limitations},
and discuss where using existential sizes breaks down for well-founded trees in \cref{subsec:infinity}.

In the syntactic model, sizes and their order are translated to inductive definitions in \CICE,
and quantification over (bounded) sizes is translated
to abstractions over the translation of sizes (and their orders).
The entire translation must be \emph{type preserving}:
if some term $e$ is well typed under some environments $\Phi; \Gamma$ with some type $\tau$,
then the translated term $\compile{e}$ must also be well typed
under the translated environment $\compile{\Phi}, \compile{\Gamma}$
with the translated type $\compile{\tau}$.
By the consistency of \CICE and a type-preserving translation to it,
we can prove the consistency of \lang:
there exists no term $e$ such that
$\type{\mt \mathbin{;} \mt}{e}{\funtypeT{\PT}{\PropT}{\PT}}$.

\begin{center}
\mbox{* * *}
\end{center}

\noindent In \cref{sec:sized-dep-types}, we describe the syntax and judgements of \lang in detail
and provide examples of sized types in \lang.
In \cref{sec:model}, we describe \CICE and define the translation from \lang to \CICE.
We explain the proof architecture and metatheoretical properties of \lang and
CICE in \cref{sec:proofs}, summarizing the proofs, but explaining key cases in
detail.
We conclude in \cref{sec:discussion}, discussing some shortcomings of \lang,
particularly regarding universe levels of the inductive types and the lost
expressivity without the infinite size, and directions for future investigation.

Throughout, initial appearances of new notation are highlighted in grey.
We use ellipses \new{$\seq$} as metanotation for denoting a repeated sequence of some syntactic construct,
overlines \new{$\vec{\phantom{I}}$} for sequences of variables or terms specifically (\eg $\vec{z}$, $\vec{p}$),
and \new{$\mt$} for denoting an empty sequence (particularly for environments).
Irrelevant constructs are omitted using an underscore \new{$\any$}.
Metafunctions are introduced in the prose as needed.

\section{Sized Dependent Types} \label{sec:sized-dep-types}

\input{figures/sized.tex}
\input{figures/ind.tex}

We present first the sublanguage of \lang without any inductives
to get the preliminary details out of the way first,
and also to show that the sublanguage is independent of the inductives chosen.
After that, we add naturals and well-founded trees as representative inductive types,
followed by examples of programming with sized dependent types.

\subsection{Base \lang}

\FigSyntax{fig:syntax}
\cref{fig:syntax} gives the syntax of \lang, consisting of universes $U$, sizes $s$, and terms $e$,
the latter of which includes term functions and size abstractions.
Note that the hierarchy of universes above $\Prop$ start at $\Type{1}$, not $\Type{0}$.
Most judgements use two environments: a term environment $\Gamma$ with assumptions $\annot{x}{\tau}$
and type-annotated definitions $\define{x}{\tau}{e}$,
and a size environment $\Phi$ with unbounded and bounded size variables.
We also use the assumption environment
$\Delta$ as a shorthand when writing nested expressions with assumptions;
in particular, letting for instance $\Delta_{xy} = \annot{x}{\sigma_1}, \annot{y}{\sigma_2}$,
We use \new{$\arr*{\Delta_{xy}}{\tau}$} to mean $\funtype{x}{\sigma_1}{\funtype{y}{\sigma_2}{\tau}}$.
Similarly, we use \new{$\arr*{\sigma}{\tau}$} to mean the nondependent function type $\funtype{\any}{\sigma}{\tau}$
As a loose convention, we use $\tau, \sigma$ for type-like terms,
$P$ for the motive of eliminators,
$z$ for variables representing constructor arguments, and
$f, g$ for variables representing functions.

As mentioned in \cref{sec:introduction}, the judgement forms of \lang include
reduction, its various closures, $\alpha$-cumulativity, subtyping, and typing.
On top of those, there are also judgement forms for subsizing, sizes,
and well formedness of size and
term environments \fbox{$\wf{}{\Phi}$}, \fbox{$\wf{\Phi}{\Gamma}$};
since well formedness rules are straightforward I omit them here,
but they can be found in \cref{app:cong:red}.

\begin{figure}[h]
\centering
\begin{mathpar}
\fbox{$\red{\Phi; \Gamma}{e}{e}$} \qquad
\fbox{$\red*{\Phi; \Gamma}{e}{e}$} \hfill
\inferrule[]{
  (\define{x}{\tau}{e}) \in \Gamma
}{
  \red{\Phi; \Gamma}{x}{e}
}
\and \inferrule[]{~}{\red{\Phi; \Gamma}{\app{(\fun{x}{\tau}{e})}{e'}}{\subst{e}{x}{e'}}}
%\and \inferrule[]{~}{\red{\Phi; \Gamma}{\J{}{d}{\refl{}}}{d}}
\and \inferrule[]{~}{\red{\Phi; \Gamma}{\App{(\Fun{\alpha}{e})}{s}}{\subst{e}{\alpha}{s}}}
\and \inferrule[]{~}{\red{\Phi; \Gamma}{\App{(\Fun<{\alpha}{r}{e})}{s}}{\subst{e}{\alpha}{s}}}
\and \inferrule[]{~}{\red{\Phi; \Gamma}{\letin{x}{\tau}{e'}{e}}{\subst{e}{x}{e'}}}
%\and \inferrule[]{~}{\red{\Phi; \Gamma}{\unpair{\alpha}{x}{\Pair{s}{e'}}{e}}{\subst{e}{\alpha, x}{s, e'}}}
\and \inferrule*[right=\rlabel{$\rhd$-cong}{red-cong}]{
  \red{\Phi'; \Gamma'}{e'}{e''}
}{
  \red{\Phi; \Gamma}{\subst{e}{x}{e'}}{\subst{e}{x}{e''}}
}
\\
\inferrule*[right=\rlabel{$\rhd^*$-once}{red*-once}]{
  \red{\Phi; \Gamma}{e_1}{e_2}
}{
  \red*{\Phi; \Gamma}{e_1}{e_2}
}
\quad
\inferrule*[right=\rlabel{$\rhd^*$-refl}{red*-refl}]{~}{\red*{\Phi; \Gamma}{e}{e}}
\quad
\inferrule*[right=\rlabel{$\rhd^*$-trans}{red*-trans}]{
  \red*{\Phi; \Gamma}{e_1}{e_2} \\
  \red*{\Phi; \Gamma}{e_2}{e_3}
}{
  \red*{\Phi; \Gamma}{e_1}{e_3}
}
\end{mathpar}
\caption{Reduction rules (base \lang)}
\label{fig:reduction}
\end{figure}

The reduction rules and their reflexive, transitive closure are described in \cref{fig:reduction}.
\new{$\subst{e}{x}{e'}$} denotes capture-avoiding substitution of $x$ for $e'$ within $e$,
and correspondingly \new{$\subst{e}{x_1, \seq, x_n}{e_1, \seq, e_n}$} denotes simultaneous substitution.
For every syntactic form of a composite term there is a corresponding congruence rule,
which is summarized by \rref{red-cong} using substitution;
the full set of rules can be found in \cref{app:cong:red}.
By convention, the reduction rules for function applications are also referred to as $\beta$-reduction,
for $\kw{let}$ expressions as $\zeta$-reduction,
and for defined variables as $\delta$-reduction.

\FigSubtype{fig:subtyping}

Rather than a single subtyping judgement like in \GCC,
we use the same presentation as MetaCoq
and split it into a subtyping judgement
and a separate $\alpha$-cumulativity judgement,
listed in \cref{fig:subtyping}.
This overcomes some technical proof complications that appear in
the single-judgement presentation due to the transitivity rule.
Aside from the expected cumulativity of universes,
the function type and size quantification are covariant in the codomain
(\ie are $\alpha$-cumulative when their codomains are),
while remaining invariant in the domain.
All other types are invariant, as reflected by \rref{acum-refl}.
A term is then a subtype of another if they are confluent up to $\alpha$-cumulativity.

\cref{fig:subsizing} describes a preorder on sizes such that
the successor operator is monotonic with respect to the order.
The base size $\circ$ is smaller than all sizes,
and the strict preorder $\bound{\alpha}{s}$ arising from bounded quantification or abstraction
is defined as $\sss{\alpha} \mathrel{\leqslant} s$.
An additional size judgement ensures well scopedness of sizes.

\FigSubsize{fig:subsizing}
\FigTyping[h]{fig:typing}

Finally, the typing rules for the base \lang are given in \cref{fig:typing}.
They use two metafunctions defined by
$\axioms{\Prop} = \Type{1}$ and $\axioms{\Type{i}} = \Type{i+1}$;
and by $\rules{U}{\Prop} = \Prop$, $\rules{\Prop}{U} = U$, and $\rules{\Type{i}}{\Type{j}} = \Type{\maximum{i, j}}$.

\rref{var, univ, let} are the usual rules for variables, universes, and $\kw{let}$ expressions in \GCC,
while \rref{pi, lam, app} are the usual ones for functions.
\rref{conv} uses the subtyping judgement and essentially allows casting a term
from one type to a supertype as needed.
\rref{forall, forall<, slam, slam<, sapp, sapp<} are the new rules relevant to sized types,
describing bound and unbound size quantification, abstraction, and application,
which work similarly to functions.
Of note is the bounded size application rule,
which only allows applications to smaller sizes following the subsizing judgement.

\subsection{Inductive Types: Naturals and Well-Founded Trees} \label{subsec:ind-types}

\FigSyntaxInd{fig:syntax-ind}
\cref{fig:syntax-ind} extends the grammar with sized naturals, sized well-founded trees,
$\kw{case}$ expressions, and fixpoint expressions.
Informally, borrowing syntax from the definition of general inductives,
sized naturals and well-founded trees can be thought of as being defined by the following:

\begin{align*}
&\data{\N{\alpha}}{\Type{1}} && \data{\App{\app{\W*}{(\annot{A}{\Type{i}})}{(\annot{B}{\arr*{A}{\Type{i}}})}}{\alpha}}{\Type{i+1}} \\
&\quad \annot{\zero*}{\Funtype<{\beta}{\alpha}{\N{\alpha}}} && \quad \annot{\sup*}{\Funtype<{\beta}{\alpha}{\arr{x}{A}{\arr*{(\arr*{\app{B}{x}}{\app{\App{\W*}{\beta}}{A}{B}})}{\App{\app{\W*}{A}{B}}{\alpha}}}}} \\
&\quad \annot{\succ*}{\Funtype<{\beta}{\alpha}{\arr*{\N{\beta}}{\N{\alpha}}}}
\end{align*}

The types of naturals and well-founded trees can then be considered to be (nonuniformly) parametrized by a size,
and constructing an element of that type requires providing a strictly smaller size,
which is the size%
\footnote{The ``size of'' some construction is more precisely the size by which its \emph{inductive type} is parametrized.}
of the constructor's recursive arguments.
Constructors therefore always construct elements whose sizes are larger than their arguments'.
Since constructor argument sizes are bounded by above,
the size of an inductive represents the size an element of the inductive can \emph{at most} have,
and it can always be lifted to a larger size, but never lowered to a smaller one.

In \lang, the constructors are annotated with their types
since the parameter-like sizes cannot otherwise be synthesized.
For instance, $\succ{s}{r}{e}$ constructs a natural of size $s$,
while taking as argument a natural of size $r < s$.
Although $\zero*$ has no recursive arguments,
it still takes a smaller size argument solely for uniformity with $\succ*$.
Additionally, W types have explicit binders for the first type parameter for convenience,
much like dependent function types:
the variable $x$ is bound within $\tau$ in the type $\W{x}{\sigma}{\tau}{s}$.

The expression
$\match{e}{\fun*{x}{P}}{(\app{\App{c}{\alpha}}{z_1}{\seq}{z_m} \Rightarrow e_c) \seq}$
contains three parts:
the \emph{target} $e$ it destructs,
the \emph{motive} $P$ denoting the return type of the expression abstracted over a target,
and the \emph{branches} $e_c$, one for each constructor of the target's type,
abstracted over the constructor's size and term arguments.
Its reduction rules for each constructor are given in \cref{fig:reduction-ind},
along with the reduction rule for fixpoint expressions.
By convention, the reduction rules for $\kw{case}$ expressions
are also referred to as $\iota$-reduction,
and for fixpoint expressions as $\mu$-reduction.
\FigRedInd{fig:reduction-ind}

Fixpoints reduce when applied to some size $s$ by substitution of itself into its own body.
Fixpoints' bodies are well typed when recursive applications occur only on smaller sizes,
so the substitution wraps itself in a bound size abstraction.
Most importantly, they reduce only when there exists some size strictly smaller than $s$;
intuitively, this restriction prevents fixpoints from reducing indefinitely
because subsizing is well founded, and there cannot be an infinite chain of smaller sizes.

\FigTypingInd{fig:typing-ind}

The typing rules for all new constructs are given in \cref{fig:typing-ind},
using two additional metafunctions: $\fresh{\seq}$ asserts the freshness of the given variables,
and $\FV{\mt}$ produces the free variables in the given term.
As discussed, the body of a fixpoint is only well typed
when the fixpoint is recursively applied to a smaller size,
as enforced by its type in the environment when type checking the body.

Sizes aside, the only difference from regular, unsized naturals and well-founded trees
is that their types live in a universe one level higher than they usually are.
$\N{s}$ lives in $\TypeT{1}$ rather than in $\Type{0}$,
and $\W{x}{\sigma}{\tau}{s}$ lives in $\axioms{U}$ rather than in $U$.
This is a direct consequence of the way that the translation is defined,
and is necessary to maintain its type preservation properties.
While not incorrect, inductive types living in the ``wrong'' universe is aesthetically unpleasant
and removes some of the impredicativity of their parameters
by preventing them from quantifying over the inductive types themselves.
Potential methods of circumventing this undesirable trait to varying degrees of success
is discussed later in \cref{subsec:infinity}.

\subsection{Examples} \label{subsec:examples}

This section presents examples of using \lang for programming.
Although it only has naturals and well-founded trees,
we also use other sized inductive types as examples,
informally defining them similarly to \cref{subsec:ind-types}.
We omit the type annotation of $\kw{let}$-bound expressions
when the type is evident or deducible from context.

\subsubsection{Size-preserving functions}

One of the most important uses of sized types is the ability to define
\emph{size-preserving} functions,
where the sizes of the input and output types are the same.
This guarantees that the output is never larger than the input,
and size-preserving functions can be used in recursive calls of fixpoints.
For instance, the $\monus$ function, which computes $\maximum{0, n - m}$,
can be size preserving in its first argument,
since $n - m$ is never greater than $n$.
Here, $\pred$ is another size-preserving function
$\Funtype{\alpha}{\arr*{\N{\alpha}}{\N{\alpha}}}$
that computes $\maximum{0, n - 1}$ for some number $n$.

\begin{align*}
&\Let{\monus}{\Funtype{\alpha}{\Funtype{\beta}{\arr*{\N{\beta}}{\N{\alpha}}{\N{\beta}}}}}{ \\
&\fix{\monus*}{\alpha}{\Funtype{\beta}{\arr*{\N{\beta}}{\N{\alpha}}{\N{\beta}}}}{ \\
&\quad \Fun{\beta}{\fun{n}{\N{\beta}}{\fun{m}{\N{\alpha}}{\match*{m}{ \\
&\qquad \App{\zero*}{\gamma} \Rightarrow n \\
&\qquad \app{\App{\succ*}{\gamma}}{k} \Rightarrow \app{\App{\monus*}{\gamma}{\beta}}{(\app{\App{\pred}{\beta}}{n})}{k}}}}}}}
\end{align*}

We see the benefit of size preservation with $\divv$,
which computes Euclidean division of $n$ by $m$, or $\left\lceil\frac{n}{m+1}\right\rceil$.
This is computed recursively by subtracting $m$ from the numerator using $\monus$
until $\zero*$ is reached, and counting the number of times the subtraction is performed.
The recursive call is performed on the result of $\monus$;
$\divv$ then only type checks because $\monus$ is size preserving.
Because the first argument of the recursive call to $\divv$ isn't \emph{structurally}
a subterm with the call to $\monus$ in the way,
a guardedness check wouldn't accept the corresponding unsized function.
%
\begin{align*}
&\Let{\divv}{\Funtype{\alpha}{\Funtype{\beta}{\arr*{\N{\alpha}}{\N{\beta}}{\N{\alpha}}}}}{ \\
&\fix{\divv*}{\alpha}{\Funtype{\beta}{\arr*{\N{\alpha}}{\N{\beta}}{\N{\alpha}}}}{ \\
&\quad \Fun{\beta}{\fun{n}{\N{\alpha}}{\fun{m}{\N{\beta}}{\match*{n}{ \\
&\qquad \App{\zero*}{\gamma} \Rightarrow \zero{\alpha}{\gamma} \\
&\qquad \app{\App{\succ*}{\gamma}}{k} \Rightarrow
\succ{\alpha}{\gamma}{
  (\app{\App{\divv*}{\gamma}{\beta}}{
    (\app{\App{\monus}{\beta}{\gamma}}{k}{
      (\app{\App{\pred}{\beta}}{m})})}{m})}}}}}}}
\end{align*}

\subsubsection{Higher-rank sizes}

This example, which demonstrates higher-rank size quantification,
is a traversal of a well-founded tree with a size-preserving function,
adapted from the rose tree traversal example by \citet{NbE}.
Given some size-preserving function on a well-founded tree,
the function is applied to subtrees prior to traversal.
Suppose that $B$ here is some type operator on $A$.
%
\begin{align*}
&\Let{\traverseW}{\arr*{(\Funtype{\gamma}{\arr*{\W{x}{A}{\app{B}{x}}{\gamma}}{\W{x}{A}{\app{B}{x}}{\gamma}}})}{ \\
&\phantom{\kw{let} \: \traverseW \mathrel{:} \phantom{}} \Funtype{\alpha}{\arr*{\W{x}{A}{\app{B}{x}}{\alpha}}{\W{x}{A}{\app{B}{x}}{\alpha}}}}}{ \\
&\quad \fun{f}{\Funtype{\gamma}{\arr*{\W{x}{A}{\app{B}{x}}{\gamma}}{\W{x}{A}{\app{B}{x}}{\gamma}}}}{ \\
&\quad \fix{\traverse}{\alpha}{\arr*{\W{x}{A}{\app{B}{x}}{\alpha}}{\W{x}{A}{\app{B}{x}}{\alpha}}}{ \\
&\qquad \fun{w}{\W{x}{A}{\app{B}{x}}{\alpha}}{\match*{w}{ \\
&\qquad \quad \app{\App{\sup*}{\beta}}{a}{g} \Rightarrow \sup{x}{A}{\app{B}{x}}{\alpha}{\beta}{a}{(\fun{b}{\app{B}{a}}{\app{\App{\traverse}{\beta}}{(\app{\App{f}{\beta}}{(\app{g}{b})})}})}}}}}}
\end{align*}

\subsubsection{Limitations} \label{subsec:examples:limitations}

As expressive as bounded, higher-rank sized types are,
there still exist limitations to what can be expressed in comparison to ordinary inductive types
or to sized type theories which have an infinite size,
such as the ones listed in \cref{tab:sized-types}.
Limitations typically arise when dealing with inductive definitions where
recursive arguments appear as the return type of a function.
Consider the following inductive definition
representing the Brouwer notation for ordinals (see \eg \citet{ordinals})
with zero, successor, and limit ordinals:
%
\begin{align*}
&\data{\Ord{\alpha}}{\Type{1}} \\
&\quad \annot{\zord*}{\Funtype<{\beta}{\alpha}{\Ord{\alpha}}} \\
&\quad \annot{\sord*}{\Funtype<{\beta}{\alpha}{\arr*{\Ord{\beta}}{\Ord{\alpha}}}} \\
&\quad \annot{\lord*}{\Funtype<{\beta}{\alpha}{\arr*{(\Funtype<{\gamma}{\beta}{\arr*{\N{\gamma}}{\Ord{\beta}}})}{\Ord{\alpha}}}}
\end{align*}

The limit ordinal, taking some function on naturals returning an ordinal,
constructs an ordinal meant to be ``larger'' than any of the returned ordinals.
Such a function should be able to return an ordinal larger than any natural,
hence the bounded size quantification in its domain.
Conversely, the naturals embed quite naturally within the ordinals;
let $\natOrd$ be such an embedding function
$\Funtype{\alpha}{\arr*{\N{\alpha}}{\Ord{\alpha}}}$.
In an unsized type theory, supposing that $\const{natOrd'}$ is an unsized version of $\natOrd$,
the first limit ordinal $\const{\omega'}$ is easily defined as
$\Let{\const{\omega'}}{\const{Ord}}{\app{\lord*}{\const{natOrd'}}}$.
However, in \lang, things aren't so easy; given a function $\App{\liftO}{\alpha}{\beta}$
that lifts an ordinal $\Ord{\beta}$ to a larger-sized ordinal $\Ord{\alpha}$, we might try:
%
\begin{align*}
&\Let{\omegaOrd}{\Ord{\sss{\hole}}}{\lord{\sss{\hole}}{\hole}{(\Fun<{\gamma}{\hole}{\fun{n}{\N{\gamma}}{\app{\App{\liftO}{\hole}{\gamma}}{(\app{\App{\natOrd}{\gamma}}{n})}}})}}
\end{align*}

The crucial problem is: what size fills in the hole \new{$\hole$}?
Intuitively, this size must be larger than the size of \emph{any} natural.
Therefore, a corresponding ``limit size'' is needed;
the infinite size in other sized type theories can fill this role since it's larger than all sizes
and therefore the limit of \emph{all} sizes.
We discuss the infinite size further in \cref{subsec:infinity}.

\section{Syntactic Model of \lang} \label{sec:model}

\input{figures/cic.tex}
\input{figures/definitions.tex}
\input{figures/translation.tex}

\lang is modelled in \CICE.
The key idea is that sizes in \lang can themselves be represented as a inductive type in \CICE,
and naturals and well-founded trees are then inductives with an additional size parameter.
Sizes are represented as a (generalization of) the Brouwer notation for ordinals in type theory,
and their order as an inductive type indexed by sizes.
The order is \emph{well founded}:
there is no infinite sequence of ever-smaller sizes,
and there is always a ``smallest'' size (or many of them).
This property allows for \emph{well-founded induction},
where to prove some property on sizes, one supposes that it holds for all strictly smaller sizes.

Every fixpoint expression in \lang is modelled as an instance of well-founded induction in \CICE.
To prove well foundedness and in turn the induction principle,
we show that sizes satisfy an \emph{accessibility predicate}~\citep{accessibility}.
For the type preservation proof to go through,
\emph{definitional proof irrelevance}
of accessibility predicates is required---all proofs of accessibility
are definitionally equal.
Since the proof irrelevance holds propositionally,
We use an extensional CIC to obtain the definitional equality
from the propositional equality via equality reflection\index{equality reflection}.

We start by briefly reviewing the syntax and judgements of \CICE.
We then describe the translation from \lang to \CICE,
which is a metafunction from typing derivations of \lang to terms of \CICE.
In addition to the notation used in \cref{sec:sized-dep-types},
given variables $\vec{\xT} = \xT_1 \seq \xT_n$,
terms $\vec{\eT} = \eT_1 \seq \eT_n$,
and types $\vec{\tauT} = \tauT_1 \seq \tauT_n$,
\new{$\annotT{\vec{\xT}}{\vec{\tauT}}$} denotes the assumption environment
$\annotT*{\xT_1}{\tauT_1}, \seq, \annotT*{\xT_n}{\tauT_n}$,
\new{$\subst{\eT}{\vec{\xT}}{\vec{\eT}}$} denotes the simultaneous substitution
$\subst{\eT}{\xT_1, \seq, \xT_n}{\eT_1, \seq, \eT_n}$, 
\new{$\funT{\vec{\xT}}{\vec{\tauT}}{\eT}$} denotes the $n$-ary function
$\funT{\xT_1}{\tauT_1}{\seq \funT{\xT_n}{\tauT_n}{\eT}}$, and
\new{$\type{\GammaT}{\vec{\eT}}{\vec{\tauT}}$} denotes the $n$ typing judgements
$(\type{\GammaT}{\eT_1}{\tauT_1})$, \seq, $(\type{\GammaT, \annotT{\eT_1}{\tauT_1}, \seq, \annotT{\eT_{n-1}}{\tauT_{n-1}}}{\eT_n}{\tauT_n})$.

\subsection{Target Type Theory}

\FigSyntaxCIC{fig:syntax-cic}
The syntax of \CICE is given in \cref{fig:syntax-cic};
differences from \lang include a 1-based index for the recursive argument of fixpoint expressions,
$\tg{case}$ expression motives abstracted over the target's inductive type indices,
and a homogeneous propositional equality type with the reflexivity constructor and $\JT*$ eliminator.
New inductive types are defined using data definitions $\DT$,
whose syntax resembles the informal presentation used in \cref{sec:sized-dep-types}.
Metavariable usage convention is roughly the same as for \lang,
with the addition of $\pT$ for inductive type parameters or proofs of equality
and $\aT$ for inductive type indices.

The well formedness conditions on inductive data definitions,
such as well typedness and \emph{strict positivity},
are entirely standard, so we omit them;
see \eg pCIC~\citep{pCIC} for instance for a full description.
Inductive definitions in their full generality aren't needed,
and nonmutual, nonnested inductives suffice.
Indeed, only six inductive definitions are used for the translation
for representing sizes, their order, their well foundedness,
and the empty type, naturals, and well-founded trees.

\begin{figure}[h]
\centering
\begin{mathpar}
\fbox{$\type{\GammaT}{\eT}{\tauT}$} \qquad
\fbox{$\subtype{\GammaT}{\tauT}{\tauT}$} \qquad
\fbox{$\defeq{\GammaT}{\eT}{\eT}{\tauT}$} \hfill \\
\inferrule[\rlabel*{conv*}]{
  \type{\GammaT}{\eT}{\sigmaT} \\
  \type{\GammaT}{\sigmaT}{\UT} \\\\
  \type{\GammaT}{\tauT}{\UT} \\
  \subtype{\GammaT}{\sigmaT}{\tauT}
}{
  \type{\GammaT}{\eT}{\tauT}
}
\and
\inferrule[\rlabel{$\preccurlyeq$-conv}{subtype-conv}]{
  \defeq{\GammaT}{\tauT_1}{\tauT_2}{\UT}
}{
  \subtype{\GammaT}{\tauT_1}{\tauT_2}
}
\and
\inferrule[\rlabel{$\equiv$-refl}{equiv-refl}]{
  \type{\GammaT}{\eT}{\tauT}
}{
  \defeq{\GammaT}{\eT}{\eT}{\tauT}
}
\and
\inferrule[\rlabel{$\equiv$-conv}{equiv-conv}]{
  \subtype{\GammaT}{\sigmaT}{\tauT} \\\\
  \defeq{\GammaT}{\eT_1}{\eT_2}{\sigmaT}
}{
  \defeq{\GammaT}{\eT_1}{\eT_2}{\tauT}
}
\and
\inferrule[\rlabel{$\equiv$-reflect}{equiv-reflect}]{
  \type{\GammaT}{\pT}{\eqT{\eT_1}{\tauT}{\eT_2}}
}{
  \defeq{\GammaT}{\eT_1}{\eT_2}{\tauT}
}
\and
\inferrule[\rlabel{$\equiv$-$\mu$}{equiv-mu}]{
  \type{\GammaT}{\tauT}{\UT} \\
  \defeq{\GammaT}{\tauT}{\arr*{\DeltaT}{\funtypeT{\any}{\app{\XT}{\vec{\pT}}{\vec{\aT}}}{\tauT'}}}{\UT} \\\\
  \card{\DeltaT} + 1 = \nT \\
  \type{\GammaT, \annotT{\fT}{\tauT}}{\eT}{\tauT}
}{
  \defeq{\GammaT}{\fixT{\nT}{\fT}{\tauT}{\eT}}{\subst{\eT}{\fT}{\fixT{\nT}{\fT}{\tauT}{\eT}}}{\tauT}
}
\and
\inferrule[\rlabel*{fix*}]{
  \type{\GammaT}{\tauT}{\UT} \\
  \defeq{\GammaT}{\tauT}{\arr*{\DeltaT}{\funtypeT{\any}{\app{\XT}{\vec{\pT}}{\vec{\aT}}}{\tauT'}}}{\UT} \\
  \card{\DeltaT} + 1 = \nT \\
  \type{\GammaT, \annotT{\fT}{\tauT}}{\eT}{\tauT}
}{
  \type{\GammaT}{\fixT{\nT}{\fT}{\tauT}{\eT}}{\tauT}
}
\end{mathpar}
\caption{Excerpt of typing, subtyping, and equivalence rules}
\label{fig:equiv-sub-type}
\end{figure}

The typed equivalence, subtyping, and typing judgements are defined mutually:
equivalence depends on typing and subtyping,
subtyping depends on equivalence,
and typing depends on subtyping and equivalence.
The judgement rules are all standard,
so \cref{fig:equiv-sub-type} presents only an excerpt;
the full rules are found in \cref{app:equiv}.
The first row contains the main mutual dependencies between the judgements,
followed by notable \rref{equiv-reflect, equiv-mu, fix*}.

To summarize, equivalence is, by definition, an equivalence relation,
satisfying reflexivity, symmetry, and transitivity as well as congruence.
An equivalence judgement can be converted to one annotated by a supertype via \rref{equiv-conv}.
The key rule for extensionality is equality reflection in \rref{equiv-reflect},
which definitionally equates two terms whenever there exists some proof of their propositional equality.
The remaining equivalence rules are typed versions of the usual reduction rules
for functions, $\tg{let}$ expressions, $\tg{case}$ expressions, and fixpoint expressions,
as well as $\eta$-equivalence for functions.

\rref{equiv-mu} for fixpoints is \emph{unguarded},
meaning that fixpoints are equivalent to the substitution of itself into its own body
regardless of what they are applied to.
To maintain normalization,
the usual guarded reduction rule in intensional CIC reduces fixpoints
only when applied to a literal constructor in the recursive argument position.
\vspace{-0.5\baselineskip}
\begin{mathpar}
\inferrule*[right=\rlabel{$\equiv$-$\mu$-guarded}{equiv-mu-guarded}]{\cdots \\ \card{\vec{\eT}'} + 1 = \nT}{
  \defeq{\GammaT}{\app{(\fixT{\nT}{\fT}{\tauT}{\eT})}{\vec{\eT}'}{(\app{\cT}{\vec{\aT}})}}{\app{(\subst{\eT}{\fT}{\fixT{\nT}{\fT}{\tauT}{\eT}})}{\vec{\eT}'}{(\app{\cT}{\vec{\aT}})}}{\tauT}
}
\end{mathpar}

Evidently \rref{equiv-mu-guarded} can be derived from \rref{equiv-mu} by congruence.
On the other hand,
\rref{equiv-mu} can be derived from \rref{equiv-mu-guarded}
by reflecting a proof of their propositional equality,
which can be constructed using transitivity, congruence, and $\eta$-equivalence.
Since \rref{equiv-mu} and \rref{equiv-mu-guarded} are metatheoretically equivalent in \CICE,
we choose to use \rref{equiv-mu} for its simplicity.

As opposed to \lang, for \CICE we use pCIC's presentation of subtyping,
which has a typed equivalence premise in \rref{subtype-conv}.
It also has an explicit rule for transitivity of subtyping since judgements such as
$\subtype{\mt}{\app{(\funT{P}{\TypeT{\tg{1}}}{P})}{\PropT}}{\TypeT{\tg{0}}}$ would fail to hold otherwise.
Finally, the typing and environment well formedness rules are similar to those in \lang.
An additional premise to \rref{fix*} ensures that the $\nT$th argument is indeed an inductive type.
As previously mentioned, fixpoints must also be guarded:
recursive calls can only occur on structurally smaller arguments of elements of inductives.
The guard condition is well studied \citep{guard, guard-relax, Coq} and so omitted here.
To justify uses of fixpoint expressions in the translation,
we will provide either a mechanization or present a brief argument of guardedness.

\subsection{Preliminary Definitions} \label{subsec:prelim}

Before defining the translation from \lang terms to \CICE terms,
in this section we describe how the necessary \CICE terms are constructed,
which comprises the aforementioned six inductive data definitions
and well-founded induction principle
as well as the various properties which the order on sizes satisfies.

\FigData{fig:data-defns}

The inductive definitions are listed in \cref{fig:data-defns}
along with some basic definitions we treat as global.
$\botT$ is the usual empty type.
$\SizeT$ is a generalization of the $\Ord*$ type introduced in \cref{subsec:examples},
with the domain of the function passed to $\limT$ replaced by some arbitrary type.
Although limit sizes aren't strictly necessary for the translation,
as \lang only has successor sizes and size variables,
we include them so that various solutions to the problem of the infinite size
can be explored in \cref{subsec:infinity}.
Furthermore, this allows for a simplification of the definition,
since the zero size $\baseT$ can be defined as a limit size rather than as another constructor.

The order on sizes $\mt \szleT \mt$ is defined by the three properties that must hold~\citep{ordinals}:
\begin{itemize}[noitemsep]
  \item $\monoT$: The successor operator $\sucT$ is monotone with respect to the order;
  \item $\coconeT$: The limit operator $\limT$ constructs an upper bound, \ie
    given some function $f$ returning sizes,
    a size smaller than any size returned by $f$ is also smaller than the limit of $f$;
  \item $\limitT$: The limit operator on $f$ constructs a \emph{least} upper bound such that
    if a size is larger than \emph{all} sizes returned by $f$
    then it must also be larger than the limit of $f$.
\end{itemize}

Other properties of the order can be derived by induction from these constructors alone.
A corresponding strict order $\mt \szltT \mt$ is also defined,
and an accessibility predicate $\AccT$ is specialized to sizes and the strict order.
Note that it lives in $\PropT$, as does the argument of its sole constructor $\accT$,
so accessibility predicates are intended to be interpreted as proof irrelevant,
and their large elimination is allowed.

\FigDefns{fig:defns}

Before moving on to naturals and well-founded trees,
\cref{fig:defns} lists the names and types of a number of provable definitions.
First is \emph{function extensionality},
asserting that two functions $\annot{f, g}{\funtypeT{x}{A}{\app{B}{x}}}$ are propositionally equal if they are pointwise equal.
In \CICE, they are in fact equivalent (\ie definitionally equal):
given some proof $h$ of their pointwise equality,
under the assumption $\annot{x}{A}$,
the propositional equality $\eq{\app{f}{x}}{}{\app{g}{x}}$ proven by $\app{h}{x}$
can be reflected into the corresponding definitional equality,
which by $\eta$-equivalence is then a definitional equality of $f$ and $g$.

The remaining definitions have been mechanized in either Agda and Coq in
\cref{app:mechanization:agda:prelim} and \cref{app:mechanization:coq:prelim},
respectively, under the assumption of function extensionality as an axiom
(which cannot be proven in, but is consistent with, intensional CIC).
The mechanizations don't use any additional type-theoretic features beyond CIC,
and the proofs could theoretically be written in plain CIC,
but they would be far less manageable without the ergonomics provided by the proof assistants.
As an example, the Coq proof for $\accessible$ consists of a dozen lines of tactics,
whereas the full proof term generated from the tactics is 129 lines long.

The definitions themselves describe properties of the order on sizes
and of the accessibility predicate:
\begin{itemize}[noitemsep]
  \item $\baseleq$, $\reflleq$, $\transleq$, and $\sucleq$:
    The order is reflexive and transitive (\ie a preorder)
    such that $\baseT$ is smaller than or equal to all sizes
    and the successor sizes are greater or equal.
  \item $\accIsProp$: Accessibility predicates are \emph{mere propositions}:
    any two proofs of accessibility of a size are propositionally equal.
  \item $\accleq$: Any size smaller or equal to an accessible size is itself accessible.
  \item $\accessible$: All sizes are accessible; in other words, the order on sizes is well founded.
  \item $\wfind$ and $\wfacc$: The well-founded induction principle on sizes with respect to the order,
    proven by structural induction on the accessibility of sizes.
\end{itemize}

The only time equality reflection is needed is to prove $\accIsProp$ (via $\funext$),
which in turn is the only other equality that is reflected when proving type preservation.
Since $\AccT$ is in already $\PropT$, \CICE could be replaced by an intensional CIC
with a universe of \emph{strict propositions} $\SPropT$
of types whose elements are definitionally equal~\citep{SProp},
then placing $\AccT$ in $\SPropT$.
This is disallowed by \opcit because it breaks normalization;
however, it doesn't break consistency,
so it would remain suitable as the target language of a syntactic model.
In any case, we use \CICE because equality reflection is more established in the literature
and it allows us to use \rref{equiv-mu} in place of \rref{equiv-mu-guarded}.

Finally, the naturals and the well-founded trees in \CICE are parametrized by a $\SizeT$.
Their definitions respect the translation in the upcoming section,
so that the types of $\NatT$ and $\WT$ and their constructors are preserved.

\subsection{Translation}

The key type preservation theorem states that well-typed terms of \lang translate to
corresponding well-typed terms of CICE.
However, terms aren't the only thing requiring translation:
well typedness holds under some environment, so term environments need translations;
sizes and their environments translate to terms and term environments as well;
and derivations of size orders translate to terms which represent them.

\FigTransSize{fig:trans:size}

We begin with the translation of sizes and their environments in \cref{fig:trans:size},
which are straightforward recursive metafunctions over their syntax.
We use an asterisk superscript \new{$\mt^\ast$} on a variable $\alphaT$ to represent
a fresh variable uniquely associated with $\alphaT$.
Given some bound size variable $\alphaT$,
$\alphaT^\ast$ represents the proof that the translated size is strictly smaller
than its size bound.

The translation of subsizing judgements, on the other hand,
is a recursive metafunction over the \emph{subsizing derivation}.
\cref{fig:trans:subsize} defines the translation to \CICE terms
by induction on the subsizing rules, which recursively translates subderivations.

\begin{figure}[h]
\centering
\begin{mathpar}
\fbox{$\subsizeto{\Phi}{s}{s}{\eT}$} \hfill
\inferrule{
  (\bound{\alpha}{s}) \in \Phi
}{
  \subsizeto{\Phi}{\sss{\alpha}}{s}{\alphaT^*}
}
\and
\inferrule{\wf{\Phi}{s}}{
  \subsizeto{\Phi}{\circ}{s}{\app{\baseleq}{\compile{s}}}
}
\and
\inferrule{\wf{\Phi}{s}}{
  \subsizeto{\Phi}{s}{s}{\app{\reflleq}{\compile{s}}}
}
\and
\inferrule{\wf{\Phi}{s}}{
  \subsizeto{\Phi}{s}{\sss{s}}{\app{\sucleq}{\compile{s}}}
}
\hfill
\inferrule{
  \subsizeto{\Phi}{r}{s}{\eT}
}{
  \subsizeto{\Phi}{\sss{r}}{\sss{s}}{\app{\monoT}{\compile{r}}{\compile{s}}{\eT}}
}
\hfill
\inferrule{
  \subsizeto{\Phi}{s_1}{s_2}{\eT_{12}} \\
  \subsizeto{\Phi}{s_2}{s_3}{\eT_{23}}
}{
  \subsizeto{\Phi}{s_1}{s_3}{\app{\transleq}{\compile{s_1}}{\compile{s_2}}{\compile{s_3}}{\eT_{12}}{\eT_{23}}}
}
\end{mathpar}
\caption{Translation of subsizing}
\label{fig:trans:subsize}
\end{figure}

The translation of terms and term environments are similarly defined
as recursive metafunctions over the typing and well formedness derivations,
denoted by
\mbox{$\typeto{\Phi; \Gamma}{e}{\tau}{\eT}$} and \mbox{$\wfto{\Phi}{\Gamma}{\GammaT}$}
respectively.
However, for concision, we use $\compile{e}$ to mean the translation of $e$
when well typed under the current implicit environments,
$\compile{e}_{\Phi}$ or $\compile{e}_{\Gamma}$ to mean the translation of $e$
with the current implicit environments extended with $\Phi$ or $\Gamma$,
and $\compile{\Gamma}$ to mean the translation of $\Gamma$
when well formed under the current implicit size environment.

\FigTransTermSquash{fig:trans:term}

The translation for base \lang without inductives is given in \cref{fig:trans:term}
in the more concise notation when translated terms follow directly from subderivations
and in the usual notation otherwise.
Terms not involving sizes are translated in a straightforward recursive manner.
Unbounded size quantifications and abstractions translate to quantifications and abstractions over $\SizeT$,
while bounded ones have additional quantifications and abstractions over a proof of $\szltT$.
Size applications translate to an additional application to a proof of $\szltT$
when the size abstraction applied is bounded.

Finally, \cref{fig:trans:ind} gives the translation for naturals, well-founded trees,
$\kw{case}$ expressions, and fixpoint expressions from their typing derivations
to a \CICE term (again omitting irrelevant premises).
Aside from fixpoints, the translations are fairly straightforward,
with an additional proof term from subsizing for constructors
and dually an additional abstraction over such terms in the branches of $\tg{case}$ expressions.

\FigTransInd[h]{fig:trans:ind}

Fixpoints in \lang are not translated as fixpoints in \CICE.
Doing so while preserving types would mean that \lang fixpoints
need to be subject to the same guard conditions as \CICE fixpoints,
which would defeat the purpose of using sized types.
Instead, every single \lang fixpoint, regardless of the inductive on which they recur,
is translated to well-founded induction,
which is defined via a \CICE fixpoint on accessibility predicates.
Intuitively, the return type of a fixpoint corresponds to the motive of well-founded induction,
while recursion on a strictly smaller size corresponds to the induction hypothesis,
where the motive holds for all strictly smaller sizes.

In the next section, we prove that the translation is type preserving and,
along the way, that the translations of convertible terms are equivalent.
The main challenge is showing that the translations of a fixpoint
and its $\mu$-reduction are equivalent in \CICE,
because this requires showing that the computational behaviour of well-founded induction
is equivalent to that of the fixpoint.
Once that has been established,
showing type preservation of the translation is more or less going through the motions of the proof,
since the remaining \lang terms translate almost directly to their syntactically corresponding terms.

\section{Metatheory and Type Preservation} \label{sec:proofs}

In this section, we outline the architecture of the type preservation proof,
highlighting the interesting cases.
The final proof is done by induction on the typing derivations of \lang,
but since typing depends on subtyping,
subtyping on $\alpha$-cumulativity and closure of reduction,
closure of reduction on reduction, and reduction on substitution,
we need to first prove that they too are all preserved by the translation.
More precisely, we need to show that translation of substitution satisfies a \emph{compositionality} principle,
that the translation of reduced terms are equivalent in \CICE,
and that translated $\alpha$-cumulative terms and subtypes are correspondingly subtypes in \CICE.

These proofs in turn require several well-known metatheoretical properties of \lang and \CICE.
We begin first with these properties before moving on to the preservation proofs.

\subsection{Metatheory}

The metatheoretical properties we need of \lang are
\emph{confluence} (two different reducts of a term further reduce to a coinciding term),
transitivity of $\alpha$-cumulativity and subtyping (since it's not an explicit derivation rule),
\emph{regularity} (well typedness of the type of a well-typed term),
and \emph{subject reduction} (well-typed terms reduce to well-typed terms).
Significant lemmas are introduced as needed.

\begin{theorem}[Confluence] \label{thm:confluence}
If $\red*{\Phi; \Gamma}{e}{e_1}$ and $\red*{\Phi; \Gamma}{e}{e_2}$
then there is some term $e'$ such that
$\red*{\Phi; \Gamma}{e_1}{e'}$ and $\red*{\Phi; \Gamma}{e_2}{e'}$.
\end{theorem}

\begin{proof}
We use the \emph{Z property}~\citep{Z, confluence} technique to prove confluence,
first defining a \emph{complete development} judgement $\develop{\Phi; \Gamma}{e}{e'}$,
then showing that it satisfies the Z property:
if $\red{\Phi; \Gamma}{e_1}{e_2}$ and $\red{\Phi; \Gamma}{e_i}{e'_i}$ for $i = 1, 2$,
then $\red*{\Phi; \Gamma}{e_2}{e'_1}$ and $\red*{\Phi; \Gamma}{e'_1}{e'_2}$.
Confluence then follows from the Z property by \opcit.
Complete development is in essence the deterministic, simultaneous reduction
of all visible redexes in a term from the inside out,
and its complete definition is given in \cref{app:develop}.
\end{proof}

\begin{theorem}[Confluence up to $\alpha$-cumulativity] \label{thm:confluence-acum}
If $\acum{e_1}{e_2}$ and $\red*{\Phi; \Gamma}{e_i}{e'_i}$ for $i = 1, 2$,
then $\red*{\Phi; \Gamma}{e'_i}{e''_i}$ for $i = 1, 2$ and $\acum{e''_1}{e''_2}$.
\end{theorem}

\begin{proof}
By induction on the derivation of $\acum{e_1}{e_2}$,
making use of \nameref{thm:confluence}.
\end{proof}

\begin{lemma}[Transitivity of $\alpha$-cumulativity] \label{lem:acum-trans}
If $\acum{e_1}{e_2}$ and $\acum{e_2}{e_3}$ then $\acum{e_1}{e_3}$.
\end{lemma}

\begin{proof}
By nested induction on the derivations of $\acum{e_1}{e_2}$ and $\acum{e_2}{e_3}$.
\end{proof}

\begin{theorem}[Transitivity of subtyping] \label{thm:subtyping-trans}
If $\subtype{\Phi; \Gamma}{\tau_1}{\tau_2}$ and $\subtype{\Phi; \Gamma}{\tau_2}{\tau_3}$
then $\subtype{\Phi; \Gamma}{\tau_1}{\tau_3}$.
\end{theorem}

\begin{proof}
By cases on the derivation of
$\subtype{\Phi; \Gamma}{\tau_1}{\tau_2}$ and
$\subtype{\Phi; \Gamma}{\tau_2}{\tau_3}$,
making use of \nameref{thm:confluence}, \nameref{thm:confluence-acum},
and \nameref{lem:acum-trans}.
\end{proof}

\begin{lemma} \label{lem:wf-subderiv}
If $\wf{\Phi}{\Gamma_1, \define{x}{\tau}{e}, \Gamma_2}$
then $\type{\Phi; \Gamma_1}{e}{\tau}$ is a subderivation.
\end{lemma}

\begin{proof}
By induction on the derivation of $\wf{\Phi}{\Gamma_1, \define{x}{\tau}{e}, \Gamma_2}$.
\end{proof}

\begin{theorem}[Regularity] \label{thm:regularity}
If $\type{\Phi; \Gamma}{e}{\tau}$, then $\wf{}{\Phi}$, $\wf{\Phi}{\Gamma}$,
and $\type{\Phi; \Gamma}{\tau}{U}$.
\end{theorem}

\begin{proof}
By induction on the derivation of $\type{\Phi; \Gamma}{e}{\tau}$,
using \cref{lem:wf-subderiv} for \rref{var} when the variable refers to a definition.
\end{proof}

\begin{lemma}[Subject reduction] \label{lem:SR}
If $\type{\Phi; \Gamma}{e}{\tau}$
and $\red{\Phi; \Gamma}{e}{e'}$
then $\type{\Phi; \Gamma}{e'}{\tau}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\red{\Phi; \Gamma}{e}{e'}$
and inversion on the derivation of $\type{\Phi; \Gamma}{e}{\tau}$,
using \nameref{thm:subtyping-trans} and \nameref{thm:regularity} as needed.
\end{proof}

\begin{theorem}[Subject reduction] \label{thm:SR}
If $\type{\Phi; \Gamma}{e}{\tau}$
and $\red*{\Phi; \Gamma}{e}{e'}$
then $\type{\Phi; \Gamma}{e'}{\tau}$.
\end{theorem}

\begin{proof}
By induction on the derivation of $\red*{\Phi; \Gamma}{e}{e'}$,
using \nameref{lem:SR} for \rref{red*-once}.
\end{proof}

The metatheory we need of \CICE are \emph{subject equivalence},
or that the two equivalent terms are well typed,
and \emph{consistency}, which take as a postulate.

\begin{theorem}[Subject equivalence] \label{thm:SE}
If $\defeq{\GammaT}{\eT_1}{\eT_2}{\tauT}$
then $\type{\GammaT}{\eT_1}{\tauT}$ and $\type{\GammaT}{\eT_2}{\tauT}$.
\end{theorem}

\begin{postulate}[Consistency] \label{fact:consistency}
There exists no term $\eT$ such that
$\type{\mt}{\eT}{\funtypeT{\PT}{\PropT}{\PT}}$.
\end{postulate}

\subsection{Type Preservation} \label{subsec:preservation}

In the following proofs, we assume well typedness of the preliminary definitions of \cref{subsec:prelim}.
The first few lemmas we need are compositionality of substitution.
Because there are a number of different notions of substitution
(term substitution into a term,
size substitution into a size,
bounded size substitution into a term,
unbounded size substitution into a term),
we need compositionality lemmas for them all.
The proofs are tedious but straightforward.

\begin{lemma}[Term compositionality] \label{lem:compos-term}
If $\type{\Phi; \Gamma_1, \annot{x}{\tau'}, \Gamma_2}{e}{\tau}$
and $\type{\Phi; \Gamma_1}{e'}{\tau'}$ then
$\subst{\compile{e}}{\xT}{\compile{e'}} = \compile{\subst{e}{x}{e'}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\type{\Phi; \Gamma_1, \annot{x}{\tau'}, \Gamma_2}{e}{\tau}$.
\end{proof}

\begin{lemma}[Size compositionality] \label{lem:compos-size}
$\subst{\compile{s}}{\alpha}{\compile{r}} = \compile{\subst{s}{\alpha}{r}}$.
\end{lemma}

\begin{proof}
By induction on the structure of $s$.
\end{proof}

\begin{lemma}[Bounded compositionality of subsizing] \label{lem:compos-subsizing-bounded}
If $\subsizeto{\Phi_1, \bound{\alpha}{r'}, \Phi_2}{s}{r}{\eT}$
and $\subsizeto{\Phi_1}{\sss{s}'}{r'}{\eT'}$
then $\subsizeto{\Phi_1, \subst{\Phi_2}{\alpha}{s'}}{\subst{s}{\alpha}{s'}}{\subst{r}{\alpha}{s'}}{\subst{\eT}{\alphaT, \alphaT^*}{\compile{s'}, \eT'}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\subsizeto{\Phi_1, \bound{\alpha}{r'}, \Phi_2}{s}{r}{\eT}$,
making use of \cref{lem:compos-size}.
\end{proof}

\begin{lemma}[Unbounded compositionality of subsizing] \label{lem:compos-subsizing-unbounded}
If $\subsizeto{\Phi_1, \alpha, \Phi_2}{s}{r}{\eT}$ and $\wf{\Phi_1}{s'}$ then
$\subsizeto{\Phi_1, \subst{\Phi_2}{\alpha}{s'}}{\subst{s}{\alpha}{s'}}{\subst{r}{\alpha}{s'}}{\subst{\eT}{\alphaT}{\compile{s'}}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\subsizeto{\Phi_1, \alpha, \Phi_2}{s}{r}{\eT}$,
making use of \cref{lem:compos-size}.
\end{proof}

\begin{lemma}[Bounded size compositionality] \label{lem:compos-bounded}
If $\type{\Phi_1, \bound{\alpha}{r}, \Phi_2; \Gamma}{e}{\tau}$
and $\subsizeto{\Phi_1}{\sss{s}}{r}{\eT'}$ then
$\subst{\compile{e}}{\alphaT, \alphaT^*}{\compile{s}, \eT'} = \compile{\subst{e}{\alpha}{s}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\type{\Phi_1, \bound{\alpha}{r}, \Phi_2; \Gamma}{e}{\tau}$,
making use of \cref{lem:compos-subsizing-bounded}.
\end{proof}

\begin{lemma}[Unbounded size compositionality] \label{lem:compos-unbounded}
If $\type{\Phi_1, \alpha, \Phi_2; \Gamma}{e}{\tau}$
and $\wf{\Phi_1}{s}$ then
$\subst{\compile{e}}{\alphaT}{\compile{s}} = \compile{\subst{e}{\alpha}{s}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\type{\Phi_1, \alpha, \Phi_2; \Gamma}{e}{\tau}$,
making use of \cref{lem:compos-subsizing-unbounded}.
\end{proof}

Now we are able to prove preservation of reduction,
making use of various compositionality lemmas where substitution is involved.

\begin{lemma}[Preservation of reduction] \label{lem:pres-red}
If $\red{\Phi; \Gamma}{e}{e'}$,
$\type{\Phi; \Gamma}{e}{\tau}$, and
$\type{\compile{\Phi}, \compile{\Gamma}}{\compile{e}}{\tauT}$,
then $\defeq{\compile{\Phi}, \compile{\Gamma}}{\compile{e}}{\compile{e'}}{\tauT}$,
where $\type{\Phi; \Gamma}{e'}{\tau}$ is given by \nameref{lem:SR}.
\end{lemma}

\begin{proof}
By induction on the derivation of $\red{\Phi; \Gamma}{e}{e'}$,
using \nameref{lem:compos-term}, \nameref{lem:compos-bounded}, and \nameref{lem:compos-unbounded}
where term and (un)bounded size substitution are involved.
Inversion on the derivation of $\type{\compile{\Phi}, \compile{\Gamma}}{\compile{e}}{\tauT}$
is used to derive the typing premises needed to construct some of the equivalence derivations.
The majority of cases are straightforward; the interesting case is that of fixpoints,
since they reduce to applications of well-founded induction on sizes.
We therefore cover only that case here.
\begin{itemize}[noitemsep, label=\textbf{Case}, leftmargin=*, labelindent=\parindent]
  \item $\red[]{\Phi; \Gamma}{
      \App{(\fix{f}{\alpha}{\sigma}{e})}{s}
    }{
      \subst{e}{\alpha, f}{s, \Fun<{\beta}{s}{\App{(\fix{f}{\alpha}{\sigma}{e})}{\beta}}}
    }$.\\
    By definition of the translation, we have
    $$\type{\compile{\Phi}, \compile{\Gamma}}{
      \begin{aligned}
      & \app{\wfind}{(\funT{\alphaT}{\SizeT}{\compile{\sigma}})}{\\
      & \quad (\funT{\alphaT}{\SizeT}{\funT{\fT}{\funtypeT{\betaT}{\SizeT}{\arrT*{\betaT \szltT \alphaT}{\subst{\compile{\sigma}}{\alphaT}{\betaT}}}}{\compile{e}}})}{\compile{s}}
      \end{aligned}
    }{\tauT},$$
    where $\wfind$ (and $\wfacc$) are defined in \cref{fig:defns}.
    Because of the sheer volume of the terms involved in the translation, $\wfind$, and $\wfacc$,
    well typedness premises when applying equivalence rules are omitted,
    especially since all of these terms are known to be well typed.
    Do note, however, that by repeated applications of inversion, we have
    $\subtype{\compile{\Phi}, \compile{\Gamma}}{\app{(\funT{\alphaT}{\SizeT}{\compile{\sigma}})}{\compile{s}}}{\tauT}$. \\[\baselineskip]
    Let $\sigmaT$ be $\funT{\alphaT}{\SizeT}{\compile{\sigma}}$,
    and let $\eT$ be $\funT{\alphaT}{\SizeT}{\funT{\fT}{\funtypeT{\betaT}{\SizeT}{\arrT*{\betaT \szltT \alphaT}{\subst{\compile{\sigma}}{\alphaT}{\betaT}}}}{\compile{e}}}$.
    Liberally using transitivity, for the left-hand side we then have
    \begin{align*}
    \compile{\Phi}, \compile{\Gamma} &\vdash \app{\wfind}{\sigmaT}{\eT}{\compile{s}} \\
    &\equiv \app{\wfacc}{\sigmaT}{\eT}{\compile{s}}{(\app{\accessible}{\compile{s}})} \quad \textrm{by $\wfind$} \\
    &\equiv \app{(\fixT{1}{\wfacc*}{\funtypeT{\alphaT}{\SizeT}{\arrT*{\app{\AccT}{\alphaT}}{\app{\sigmaT}{\alphaT}}}}{ \\
      &\phantom{\equiv} \quad \funT{\alphaT}{\any}{\funT{\access}{\any}{\app{\eT}{\alphaT}{(\funT{\betaT}{\SizeT}{\funT{\betaT^*}{\betaT \szltT \alphaT}{ \\
      &\phantom{\equiv} \qquad \app{\wfacc*}{\betaT}{(\matchT*{\access}{(\app{\accT}{\pT} \Rightarrow \app{\pT}{\betaT}{\betaT^*})})}}})}}}})}{\compile{s}}{(\app{\accessible}{\compile{s}})} \quad \textrm{by $\wfacc$} \\
    &\equiv \subst{\compile{e}}{\alphaT, \fT}{\compile{s}, \funT{\betaT^*}{\betaT \szltT \compile{s}}{ \\
      &\phantom{\equiv} \quad \app{\wfacc}{\sigmaT}{\eT}{\beta}{(\matchT*{\app{\accessible}{\compile{s}}}{(\app{\accT}{\pT} \Rightarrow \app{\pT}{\betaT}{\betaT^*})})}}} \quad \textrm{by \rref*{equiv-mu} and $\wfacc$} \\
    &: \app{(\funT{\alphaT}{\SizeT}{\compile{\sigma}})}{\compile{s}}
    \end{align*}
    Meanwhile, for the right-hand side we have

    \begin{align*}
    \allowdisplaybreaks
    &\compile{\subst{e}{\alpha, f}{s, \Fun<{\beta}{s}{\App{(\fix{f}{\alpha}{\sigma}{e})}{\beta}}}} \\
    &= \subst{\compile{e}}{\alphaT, \fT}{\compile{s}, \funT{\betaT}{\SizeT}{\funT{\betaT^*}{\betaT \szltT \compile{s}}{\app{\compile{\fix{f}{\alpha}{\sigma}{e}}}{\betaT}}}} \\
      &\phantom{=} \textrm{by \cref{lem:compos-unbounded} and \cref{lem:compos-term}} \\
    &= \subst{\compile{e}}{\alphaT, \fT}{\compile{s}, \funT{\betaT}{\SizeT}{\funT{\betaT^*}{\betaT \szltT \compile{s}}{\app{\wfind}{\sigmaT}{\eT}{\betaT}}}} \quad \textrm{by translation of $\kw{fix}$} \\
    &= \subst{\compile{e}}{\alphaT, \fT}{\compile{s}, \funT{\betaT}{\SizeT}{\funT{\betaT^*}{\betaT \szltT \compile{s}}{\app{\wfacc}{\sigmaT}{\eT}{\betaT}{(\app{\accessible}{\betaT})}}}} \quad \textrm{by $\wfind$}
    \end{align*}
    The only difference between the left- and right-hand sides now
    is the proof of $\app{\AccT}{\betaT}$ for some $\betaT \szltT \compile{s}$,
    but we know that such proofs are propositionally equal to one another.
    From inversion, we know that $\compile{s}$ is well typed with type $\SizeT$.
    Then we can show that
    \begin{align*}
    &\type{\compile{\Phi}, \compile{\Gamma}, \annotT{\betaT}{\SizeT}, \annotT{\betaT^*}{\betaT \szltT \compile{s}}}{\app{\accIsProp}{\betaT}{(\matchT*{\app{\accessible}{\compile{s}}}{(\app{\accT}{\pT} \Rightarrow \app{\pT}{\betaT}{\betaT^*})})}{(\app{\accessible}{\betaT})}}{\\
    &\phantom{\type{\compile{\Phi}, \compile{\Gamma}, \annotT{\betaT}{\SizeT}, \annotT{\betaT^*}{\betaT \szltT \compile{s}}}{}{}}
    \eq{\matchT*{\app{\accessible}{\compile{s}}}{(\app{\accT}{\pT} \Rightarrow \app{\pT}{\betaT}{\betaT^*})}}{\app{\AccT}{\betaT}}{\app{\accessible}{\betaT}}}.
    \end{align*}
    By \rref{equiv-reflect}, we have
    \begin{align*}
    &\defeq{\compile{\Phi}, \compile{\Gamma}, \annotT{\betaT}{\SizeT}, \annotT{\betaT^*}{\betaT \szltT \compile{s}}}{\matchT*{\app{\accessible}{\compile{s}}}{(\app{\accT}{\pT} \Rightarrow \app{\pT}{\betaT}{\betaT^*})}}{\app{\accessible}{\betaT}}{\app{\AccT}{\betaT}}.
    \end{align*}
    Finally, by congruence, we can equate the left- and right-hand sides,
    and by \rref{equiv-conv}, we obtain our goal.
    \begin{align*}
    \defeq{\compile{\Phi}, \compile{\Gamma}}{\compile{\App{(\fix{f}{\alpha}{\sigma}{e})}{s}}}{\compile{\subst{e}{\alpha, f}{s, \Fun<{\beta}{s}{\App{(\fix{f}{\alpha}{\sigma}{e})}{\beta}}}}}{\tauT}
    \end{align*}
    \qedhere
\end{itemize}
\end{proof}

The remaining preservation proofs are rather straightforward in comparison.
We therefore don't cover any of the cases in detail,
only mentioning where prior lemmas are used in later ones.

\begin{lemma}[Preservation of reflexive, transitive closure of reduction] \label{lem:pres-red*}
If $\red*{\Phi; \Gamma}{e}{e'}$,
$\type{\Phi; \Gamma}{e}{\tau}$, and
$\type{\compile{\Phi}, \compile{\Gamma}}{\compile{e}}{\tauT}$,
then $\defeq{\compile{\Phi}, \compile{\Gamma}}{\compile{e}}{\compile{e'}}{\tauT}$,
where $\type{\Phi; \Gamma}{e'}{\tau}$ is given by \nameref{thm:SR}.
\end{lemma}

\begin{proof}
By induction on the derivation of $\red*{\Phi; \Gamma}{e}{e'}$.
\nameref{lem:pres-red} is used for \rref{red*-once},
while \nameref{thm:SR} and \nameref{thm:SE} are used for \rref{red*-trans}
to ensure that the middle term in transitivity and its translation are well typed.
\end{proof}

\begin{lemma}[Preservation of $\alpha$-cumulativity] \label{lem:pres-acum}
If $\acum{\tau_1}{\tau_2}$,
$\type{\Phi; \Gamma}{\tau_i}{U_i}$ for $i = 1, 2$, and
$\type{\compile{\Phi}, \compile{\Gamma}}{\compile{\tau_i}}{\UT_i}$ for $i = 1, 2$,
then $\subtype{\compile{\Phi}, \compile{\Gamma}}{\compile{\tau_1}}{\compile{\tau_2}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\acum{\tau_1}{\tau_2}$
inverting on the derivations of $\type{\Phi; \Gamma}{\tau_i}{U_i}$
and $\type{\compile{\Phi}, \compile{\Gamma}}{\compile{\tau_i}}{\UT_i}$
to apply the induction hypotheses.
\end{proof}

\begin{lemma}[Preservation of subtyping] \label{lem:pres-subtyping}
If $\subtype{\Phi; \Gamma}{\tau_1}{\tau_2}$,
$\type{\Phi; \Gamma}{\tau_i}{U}$ for $i = 1, 2$, and
$\type{\compile{\Phi}, \compile{\Gamma}}{\compile{\tau_i}}{\compile{U}}$ for $i = 1, 2$,
then $\subtype{\compile{\Phi}, \compile{\Gamma}}{\compile{\tau_1}}{\compile{\tau_2}}$.
\end{lemma}

\begin{proof}
By cases on the derivation of $\subtype{\Phi; \Gamma}{\tau_1}{\tau_2}$,
using \nameref{lem:pres-red*}, \nameref{lem:pres-acum},
\nameref{thm:SR}, and \nameref{thm:SE}.
\end{proof}

\begin{lemma}[Preservation of sizes] \label{lem:pres-size}
If $\wf{}{\Phi}$ then $\wf{}{\compile{\Phi}}$; and
if $\wf{\Phi}{s}$ then $\type{\compile{\Phi}}{\compile{s}}{\SizeT}$.
\end{lemma}

\begin{proof}
By mutual induction on the derivations of $\wf{}{\Phi}$ and $\wf{\Phi}{s}$.
\end{proof}

\begin{lemma}[Preservation of subsizing] \label{lem:pres-subsizing}
If $\subsizeto{\Phi}{r}{s}{\eT}$
then $\type{\compile{\Phi}}{\eT}{\compile{r} \szleT \compile{s}}$.
\end{lemma}

\begin{proof}
By induction on the derivation of $\subsizeto{\Phi}{r}{s}{\eT}$.
\end{proof}

\begin{theorem}[Type preservation] \label{thm:type-pres}
If $\wf{\Phi}{\Gamma}$ then $\wf{}{\compile{\Phi}, \compile{\Gamma}}$; and
if $\type{\Phi; \Gamma}{e}{\tau}$ then $\type{\compile{\Phi}, \compile{\Gamma}}{\compile{e}}{\compile{\tau}}$.
\end{theorem}

\begin{proof}
By mutual induction on the derivations of $\wf{\Phi}{\Gamma}$ and $\type{\Phi; \Gamma}{e}{\tau}$,
using \nameref{lem:pres-size} and \nameref{lem:pres-subsizing}
where the translations of sizes, size environments, and subsizing are involved.
\nameref{lem:pres-subtyping} is used for \rref{conv}.
\end{proof}

Finally, the consistency of \lang follows from the consistency of \CICE and type preservation.

\begin{theorem}[Consistency of \lang] \label{thm:consistency}
There exists no term $e$ such that $\type{\mt \mathbin{;} \mt}{e}{\funtype{P}{\Prop}{P}}$.
\end{theorem}

\begin{proof}
Suppose that there were such a term $e$.
By \nameref{thm:type-pres}, we would have that
$\type{\mt}{\compile{e}}{\funtypeT{\PT}{\PropT}{\PT}}$ holds.
But this contradicts \cref{fact:consistency},
so there must not be such an $e$.
\end{proof}

\section{Discussion} \label{sec:discussion}

\lang is neither flawless nor complete:
the nature of the syntactic model requires that inductives live in a universe
higher than that in which their corresponding unsized types would live,
and it's missing features such as an infinite size.
In this section, we discuss some of these shortcomings,
followed by possible directions for future work.

\subsection{The Infinite Size} \label{subsec:infinity}

In prior sized type systems, the infinite size $\infty$ is applied to sized inductive types
to represent a ``full'' inductive type encompassing that inductive at all sizes,
which essentially corresponds to the usual unsized inductive.
Whereas an inductive of some size $s$ can be thought of as the type of elements
with at most $s$ many layers of constructors,
the full inductive can be thought of as the type of elements with any number of layers of constructors.

The infinite size is characterized by its subsizing behaviour:
$\subsize*{s}{\infty}$ holds for \emph{any} $s$.
This includes its own successor, \ie $\subsize*{\sss{\infty}}{\infty}$,
leading to non--well-founded sequences of strictly ``decreasing'' sizes:
$\dots < \infty < \infty < \infty$.
Naturally, there's no way to model the infinite size as an element of $\SizeT$
given that we've shown that $\SizeT$s \emph{are} well founded.
If there were, then it'd be possible to prove an inconsistency.
Let $\inftyT$ be the translation of $\infty$,
and let $\inftyltinfty$ be the translation of $\subsize*{\sss{\infty}}{\infty}$.
\begin{align*}
&\LetT{\tg{{\neg}wf\inftyT}}{\arrT*{\app{\AccT}{\inftyT}}{\botT}}{\funT{\mathit{acc}}{\app{\AccT}{\inftyT}}{\matchT*{\mathit{acc}}{\app{\accT}{p} \RightarrowT \app{p}{\inftyT}{\inftyltinfty}}}} \\
&\LetT{\tg{false}}{\botT}{\app{\tg{{\neg}wf\inftyT}}{(\app{\accessible}{\inftyT})}}
\end{align*}

In set-theoretic models of sized type systems with an infinite size,
where sizes are modelled as set-theoretic (transfinite) ordinals,
the infinite size isn't modelled as a single ordinal;
instead, for each use of the infinite size,
its set-theoretic interpretation is an ordinal that is ``large enough'' in that context.
For instance, the interpretation of the infinite size of $\N{\infty}$
is the first limit ordinal $\omega$.

This strategy doesn't adapt well to \lang with its size abstractions and syntactic model,
since it requires a non-local translation of sizes.
For instance, given the size application $\App{e}{\infty}$,
what $\infty$ translates to would hypothetically depend on what $e$ translates to,
and likely require further static analysis of $\compile{e}$ beyond a simple translation
over typing derivations.

Since the motivation for having the infinite size is specifically for representing full inductives,
one alternative could be to define the full inductive separately
and provide functions to and from the corresponding sized inductive,
such as the following for $\W*$.
\begin{align*}
& \data{\App{\app{\W*}{(\annot{A}{\Type{i}})}{(\annot{B}{\arr*{A}{\Type{i}}})}}{\infty}}{\Type{i+1}} \\
& \quad \annot{\constr{sup\infty}}{\arr{x}{A}{\arr*{(\arr*{\app{B}{x}}{\app{\App{\W*}{\infty}}{A}{B}})}{\App{\app{\W*}{A}{B}}{\infty}}}}
\end{align*}

Defining a function from $\W{x}{A}{B}{s}$ to $\W{x}{A}{B}{\infty}$ is trivial,
since we're discarding size information.
What about going from $\W{x}{A}{B}{\infty}$ to $\W{x}{A}{B}{s}$?
What should $s$ be?
The size algebra could be augmented to be able to represent transfinite ordinals
so that $s$ is again a size that is ``large enough'',
but we can hardly demand programmers to manipulate ordinals,
and we conjecture that we would lose any hope of deciding $\subsize*{}{}$
without any user intervention.

The key insight is that what's important about an element of a full inductive
isn't its precise size and depth of constructors,
but merely that it has \emph{some} unknown size.
Another alternative to the infinite size, then, could be to represent a full inductive
as an existentially-quantified sized inductive,
\ie $\Pairtype{\alpha}{\N{\alpha}}$ and $\Pairtype{\alpha}{\W{x}{A}{B}{\alpha}}$.
Existential quantification is defined using an encoding for \emph{weak dependent pairs},
whose components can't be projected out, since the first component is a size and not a term.
We omit type annotations when deducible from context.
\begin{align*}
\Pairtype{\alpha}{\tau} &= \funtype{\sigma}{\Type{i}}{\arr*{(\Funtype{\alpha}{(\arr*{\tau}{\sigma})})}{\sigma}} \\
\Pair{s}{e}_{\Pairtype{\alpha}{\tau}} &= \fun{\sigma}{\Type{i}}{\fun{f}{\Funtype{\alpha}{(\arr*{\tau}{\sigma})}}{\app{\App{f}{s}}{e}}} \\
\unpair{\alpha}{x}{\alpha}{\tau}{e_1}{\annot{e_2}{\sigma}} &= \app{e_1}{\sigma}{(\Fun{\alpha}{\fun{x}{\tau}{e_2}})}
\end{align*}

There is still a limitation similar to that in \cref{subsec:examples:limitations}
when trying to represent the constructors of full inductives.
For $\Pairtype{\alpha}{\W{x}{A}{B}{\alpha}}$, we need a ``constructor'' of the following type.
\begin{align*}
\annot{\const{sup'}}{\arr{x}{A}{\arr*{(\arr*{B}{\Pairtype{\alpha}{\W{x}{A}{B}{\alpha}}})}{\Pairtype{\alpha}{\W{x}{A}{B}{\alpha}}}}}
\end{align*}
All we need is a function
$$\annot{\const{ac}}{\arr{x}{A}{\arr*{(\arr*{B}{\Pairtype{\alpha}{\W{x}{A}{B}{\alpha}}})}{\Pairtype{\alpha}{(\arr*{B}{\W{x}{A}{B}{\alpha}})}}}}$$
and we're good to go.
\begin{align*}
\app{\const{sup'}}{x}{f} =
\unpair*{\alpha}{f'}{\app{\const{ac}}{x}{f}}{\Pair{\sss{\alpha}}{\sup{x}{A}{B}{\sss{\alpha}}{\alpha}{x}{f'}}}
\end{align*}

Unfortunately, $\const{ac}$ can't be implemented for weak existentials
and can only be an axiom.
If we were to instead add strong dependent pairs of sizes and types,
$\const{ac}$ would still require a notion of a limit of a function returning sizes
and its subsizing properties, which would render checking subsizing undecidable.

Even so, if we take existentials as a primitive of \lang
and model them by strong dependent pairs in \CICE,
then the \emph{translation} of $\const{ac}$ can be implemented as a function.
In other words, the syntactic model justifies the axiom $\const{ac}$ in the source.
The mechanization of $\compile{\const{ac}}$ in Agda and Coq are given in
\cref{app:mechanization:agda:W} and \cref{app:mechanization:coq:W}, respectively.

Nevertheless, $\const{ac}$ remains a noncomputing axiom
unless the size algebra is augmented to include a limit operator
and size expressions consequently treated as regular terms.
There is no way to represent generalized full inductives as
sized inductives existentially quantified by sizes
and faithfully define their constructors without losing either
decidability of subsizing, due to exposing the underlying ordinal representation of sizes,
or canonicity, due to the inclusion of a noncomputing axiom.
Representing ordinary full inductives (namely naturals) this way,
however, has been previously explored~\citep{guarded, modal-sizes}.

\subsection{Universe Levels of Inductives} \label{subsec:universe-levels}

The universes in which the types of natural numbers and W types of \lang live
are, in a sense, one level higher than is usually expected,
as given by \rref{nat, wft}.
$\N*$ is typically in $\Type{0}$,
while $\W*$ is typically in $U$ rather than $\axioms{U}$.
This is due to how the translation is defined:
$\NatT$ and $\WT$ have a $\SizeT$ as parameter,
the $\limT$ operator quantifies over the type of the domain of its function argument,
and that type must be ``large'' enough to accommodate the correct type.
For $\app{\WT}{\sigmaT}{\tauT}{\sT}$,
the domain is $\app{\tauT}{\aT}$ for some $\aT$\punctstack{,}%
\footnote{For generalized inductives, given a recursive argument in the form of a function,
the domain of $\limT$ should encompass the domain of that function.}
as is the case for the definition of $\compile{\const{ac}}$,
so if its universe is $\TypeT{\iT}$,
then the universe of the type of $\sT$ must be $\TypeT{\tg{i+1}}$,
according to the definition of $\SizeT$.

This is a nonnegotiable condition:
defining $\SizeT$ to be in the same universe as that over which $\limT$ quantifies
leads to $\szltT$ no longer being well founded,
since in this hypothetical scenario, $\SizeT$ itself could be applied to $\limT$
to define an $\inftyT$ size.
\begin{align*}
&\LetT{\inftyT}{\SizeT}{\app{\limT}{\SizeT}{(\funT{\xT}{\SizeT}{\xT})}} \\
&\LetT{\inftyltinfty}{\inftyT \szltT \inftyT}{\app{\coconeT}{\SizeT}{(\app{\sucT}{\inftyT})}{(\funT{\xT}{\SizeT}{\xT})}{(\app{\sucT}{\inftyT})}{(\app{\reflleq}{(\app{\sucT}{\inftyT})})}}
\end{align*}

One way to ``shrink'' the universe of $\SizeT$, so to speak,
could be to parametrize it over the type over which $\limT$ currently quantifies,
yielding the following inductive definition.
\begin{align*}
&\dataT{\app{\SizeT}{(\annotT{A}{\TypeT{\iT}})}}{\TypeT{\iT}} \\
&\quad \annotT{\sucT}{\arrT*{\SizeT}{\SizeT}} \\
&\quad \annotT{\limT}{\arrT*{(\arrT*{A}{\SizeT})}{\SizeT}}
\end{align*}

The problem with this alternative is that for $\app{\WT}{\sigmaT}{\tauT}$,
the parameter of its size parameter would be $\app{\tauT}{\aT}$,
where $\annotT{\aT}{\sigmaT}$ is the third formal argument to its constructor $\supT$,
but this argument is only part of the constructor, not the type.
The intuition is that the parametrized $\SizeT$ is too restrictive
and there aren't ``enough'' sizes to cover all well-founded trees of any particular type.

If having inductive types in the correct universe were more important than
the potential expressibility of infinitude,
we could eliminate $\limT$ altogether and model sizes as ordinary naturals.
Then $\SizeT$ would live in $\Type{0}$, and $\NatT$ and $\WT$ would live in the correct universes,
as would $\N*$ and $\W*$.
Although this would affect the judgements of both \lang and \CICE,
this wouldn't affect the proofs, since the changes are the same for both languages.
However, this would mean giving up $\const{ac}$
and likely any hope of defining any infinitary constructs like $\const{\omega}$
when using this model.

\section{Future Directions}

There is still a long way to go towards a sized dependent type system
that is expressive, consistent, and useable.
Working without an infinite size or full inductives is verbose at best,
requiring tedious manipulation of existentially-quantified sizes,
and impossible at worse, in the case of $\const{\omega}$,
while attempts at including them either involve inconsistency, undecidability, or noncanonicity.
Alternate approaches need to be investigated to circumvent these problems.

While the issue with the universe levels of inductive types appears to be cosmetic
and not affect any important metatheoretical properties,
it might be a mere symptom of a larger issue with how sizes are modelled,
especially since prior sized type systems shown to be consistent
haven't required any similar restrictions.
One possibility is to take inspiration from Agda and
make $\SizeT$ live in a universe $\SizeUnivT$ independent of $\TypeT{}$,
but the consistency of adding $\SizeUnivT$ hasn't been established,
especially when it needs to be slightly impredicative:
$\arrT*{\TypeT{}}{\SizeT}$ would live in $\SizeUnivT$
(as would be the case for the type of $\limT$)
while $\funtypeT{\alphaT}{\SizeT}{\app{\NatT}{\alphaT}}$ would remain in $\TypeT{\tg{0}}$
(as would be the case for the type of $\zeroT$).

Additionally, \lang is missing some important but comparatively simple features
from the perspective of the syntactic model, namely inductive types in general.
They can be added directly to \lang as a generalization of the existing inductives,
and we conjecture that the type preservation proofs would be a straightforward extension.
Alternatively, since there already are well-founded trees,
\lang could instead be augmented with dependent pairs and an equality type,
both of which we also conjecture to be straightforward;
then mutual inductives, indexed inductives~\citep{whynotW}, some nested inductives~\citep{barras},
and even some inductive--inductive types~\citep{ind-ind}
could be encoded, along with their induction principles, using W types and propositional equality~\citep{whynotW}.

Dually, \lang is also missing coinductive types.
The main barrier to a syntactic model of \lang with any coinductive types
is the absence of an established target type theory with coinductive types
with nice properties.
Whereas pCIC and pCuIC lack them,
MetaCoq mechanizes Coq-style coinductive types,
but necessarily cannot prove its own consistency.
Meanwhile, older CICs with coinductive types and cofixpoints guarded by constructors
(\eg \citet{guard}) have issues with subject reduction~\citep{coind-SR},
which is a necessary property for proving type preservation in \cref{subsec:preservation}.
Another potential issue is the translation of cofixpoints into applications of
a well-founded induction principle, which seems suspicious and also requires further investigation.

In terms of metatheory, \lang is missing proof of two desirable properties:
strong normalization and decidability of type checking.
Because \nameref{lem:pres-red} only preserves reduction up to equivalence in \CICE,
not reduction, normalization doesn't hold immediately from the translation.
In particular, the proof of \nameref{lem:pres-red} uses equality reflection
to obtain an equivalence between two proofs of accessibility of a size,
and \citet{SProp} show that this equivalence can lead to nonnormalization in
certain inconsistent environments,
as is the case for $\tg{false}$.

Even so, we conjecture that the translation of an \lang term would never lead to
a \CICE term with a subterm in an inconsistent environment that leads to nonnormalization,
because the translation will never yield an assumption of the form $\sT \szltT \sT$.
By inspection of the translation, the only fitting subsizing relation possible is of the form $\alphaT \szltT \alphaT$,
and the only possible sources $\Funtype<{\alpha}{\alpha}{\tau}$, $\Fun<{\alpha}{\alpha}{e}$ are ill-scoped.
Since fixpoints only reduce when applied to sizes that have a subsize
and there shouldn't be any infinitely decreasing chains of subsizes,
they wouldn't unfold endlessly.

Decidability of type checking, meanwhile, rests not only on strong normalization,
but also on decidability of subsizing, \ie deciding whether $\bound{r}{s}$ holds.
The trickiest rule is transitivity of subsizing,
but we conjecture that subsizing, too, is decidable,
as the size environment only contains a finite number of bounded size variables,
and sizes can only have a finite number of successor operators applied.
Moreover, Agda has transitive subsizing, and hasn't had issues with decidability.

\section{Conclusion}

In this paper, we introduced \lang, a sized dependent type theory
with higher-rank size quantification and bounded size quantification,
but without an infinite size that is strictly greater than itself,
along with sized naturals and well-founded trees.
We gave examples of programming with sized inductives to write recursive programs
that would have otherwise not passed the usual syntactic guard checks,
as well as limitations of programming without the infinite size.
We then reduced the consistency of \lang to that of \CICE,
an extensional dependent type theory, by translating \lang terms to \CICE terms
and proving that the translation is type preserving.
Finally, we discussed the tradeoffs in the design of \lang for this syntactic model to work,
namely the lack of an infinite size and raising the universe levels of the inductives,
as well as potential extensions and future work.

%% Acknowledgments
\begin{acks}
%\grantsponsor{id}{name}{url}
%\grantnum{id}{num}
This research was supported by the Canada Graduate Scholarships -- Master’s (CGS M) programme.
Cette recherche a \'et\'e financ\'ee par le Programme de bourses d'\'etudes sup\'erieures
du Canada au niveau de la maitrise (BESC M).
\end{acks}

%% Bibliography
\bibliography{biblio}

%% Appendix
\clearpage
\appendix
\section{Appendix}

\input{figures/congruence.tex}
\input{figures/takahashi.tex}

\allowdisplaybreaks

\subsection{Well Formedness and Reduction Congruence Rules of \lang} \label{app:cong:red}

\FigWF{fig:wf}
\begin{figure}[h]
\centering
\fbox{$\red{\Phi; \Gamma}{\tau}{\tau}$} \qquad $\cdots$ \hfill
\FigCongRed{fig:cong:red*}
\caption{Reduction congruence rules (1 of 2)}
\label{fig:cong:red*}
\end{figure}

\begin{figure}[h]
\centering
\fbox{$\red{\Phi; \Gamma}{\tau}{\tau}$} \qquad $\cdots$ \hfill
\FigCongRedCase{fig:cong:red*-case}
\caption{Reduction congruence rules (2 of 2)}
\label{fig:cong:red*}
\end{figure}

\clearpage
\subsection{Equivalence, Subtyping, and Typing Rules of \CICE} \label{app:equiv}

\FigEquiv[h]{fig:equiv-cic}
\begin{figure}[h]
\centering
\fbox{$\defeq{\GammaT}{\eT}{\eT}{\tauT}$} \qquad $\cdots$ \hfill
\FigCongEquiv{fig:cong:equiv}
\caption{Equivalence congruence rules}
\label{fig:cong:equiv}
\end{figure}
\begin{figure}[h]
\centering
\begin{mathpar}
\fbox{$\subtype{\GammaT}{\tauT}{\tauT}$}
\and
\inferrule[\rlabel{$\preccurlyeq$-conv}{subtype-conv}]{
  \defeq{\GammaT}{\tauT_1}{\tauT_2}{\UT}
}{
  \subtype{\GammaT}{\tauT_1}{\tauT_2}
}
\and
\inferrule[\rlabel{$\preccurlyeq$-prop}{subtype-prop}]{~}{
  \subtype{\GammaT}{\PropT}{\TypeT{\iT}}
}
\and
\inferrule[\rlabel{$\preccurlyeq$-type}{subtype-type}]{
  \iT \leq \jT
}{
  \subtype{\GammaT}{\TypeT{\iT}}{\TypeT{\jT}}
}
\and
\inferrule[\rlabel{$\preccurlyeq$-trans}{subtype-trans}]{
  \subtype{\GammaT}{\tauT_1}{\tauT_2} \\
  \subtype{\GammaT}{\tauT_2}{\tauT_3}
}{
  \subtype{\GammaT}{\tauT_1}{\tauT_3}
}
\and
\inferrule[\rlabel{$\preccurlyeq$-pi}{subtype-pi}]{
  \defeq{\GammaT}{\sigmaT_1}{\sigmaT_2}{\UT} \\
  \subtype{\GammaT, \annotT{\xT}{\sigmaT_2}}{\tauT_1}{\tauT_2}
}{
  \subtype{\GammaT}{\funtypeT{\xT}{\sigmaT_1}{\tauT_1}}{\funtypeT{\xT}{\sigmaT_2}{\tauT_2}}
}
\end{mathpar}
\caption{Subtyping rules (\CICE)}
\label{fig:subtyping-cic}
\end{figure}
\FigTypingCIC[h]{fig:typing-cic}

\clearpage
\subsection{Rules for Complete Development of \lang} \label{app:develop}

\FigTakahashi{fig:develop}
\begin{figure}[h]
\centering
\fbox{$\develop{\Phi; \Gamma}{e}{e}$} \qquad $\cdots$ \hfill
\FigCongTakahashi{fig:cong:develop}
\label{fig:develop:cong}
\caption{Congruence rules for complete development}
\end{figure}

\clearpage
\setmonofont{iosevka.ttc}
\subsection{Mechanized \CICE Definitions in Coq}

The following type check on Coq 8.15.1.

\subsubsection{Preliminary definitions} \label{app:mechanization:coq:prelim}

\begin{minted}{coq}
From Equations Require Import Equations.
Require Import Coq.Program.Equality.
Require Import Coq.Unicode.Utf8_core.

Reserved Notation "r ≤ s" (at level 70, no associativity).

Inductive Size : Type :=
| suc : Size → Size
| lim : ∀ {A : Type}, (A → Size) → Size.

Inductive Leq : Size → Size → Type :=
| mono : ∀ {r s}, r ≤ s → suc r ≤ suc s
| cocone : ∀ {s A f} (a : A), s ≤ f a → s ≤ lim f
| limiting : ∀ {s A f}, (∀ (a : A), f a ≤ s) → lim f ≤ s
where "r ≤ s" := (Leq r s).

Definition Lt r s : Type := suc r ≤ s.
Notation "r < s" := (Lt r s).

Definition base : Size := lim (False_rect Size).

Definition baseLeq s : base ≤ s :=
  limiting (λ a, (False_rect (_ ≤ s) a)).

Fixpoint reflLeq {s} : s ≤ s :=
  match s with
  | suc s => mono reflLeq
  | lim f => limiting (λ a, cocone a reflLeq)
  end.

Property transLeq {r s t} (rs : r ≤ s) (st : s ≤ t) : r ≤ t.
Admitted.

(*
Derive NoConfusion for Size.
Equations transLeq {r s t : Size} (rs : r ≤ s) (st : s ≤ t) : r ≤ t :=
  transLeq (mono rs) (mono st) := mono (transLeq rs st);
  transLeq rs (cocone a sfa) := cocone a (transLeq rs sfa);
  transLeq (limiting fas) st := limiting (λ a, transLeq (fas a) st);
  transLeq (cocone a rfa) (limiting fat) := transLeq rfa (fat a).
*)

Fixpoint sucLeq s : s ≤ suc s :=
  match s with
  | suc s => mono (sucLeq s)
  | lim f => limiting (λ a, transLeq (sucLeq (f a)) (mono (cocone a reflLeq)))
  end.

Inductive Acc (s : Size) : Prop :=
acc { accLt : ∀ r, r < s → Acc r }.
Arguments accLt {_}.

Axiom funext : ∀ {A} {B : A → Type} {p q : ∀ x, B x},
  (∀ x, p x = q x) → p = q.

Equations accIsProp {s} (acc1 acc2 : Acc s) : acc1 = acc2 :=
| acc _ p, acc _ q =>
  f_equal _ (funext (λ r, funext (λ rs, accIsProp (p r rs) (q r rs)))).

Lemma accLeq : ∀ r s, r ≤ s → Acc s → Acc r.
Proof.
  intros r s rs acc.
  induction acc as [s p IH].
  exact (acc r (λ t tr, p t (transLeq tr rs))).
Qed.

Theorem wf : ∀ s, Acc s.
Proof.
  intros s.
  induction s as [s IH | A f IH].
  - refine (acc (suc s) (λ r rsucs, accLeq r s _ IH)).
    inversion rsucs as [r' s' rs | |].
    exact rs.
  - refine (acc (lim f) (λ r rlimf, _)).
    inversion rlimf as [| r' A' f' a rfa eqr eqA |].
    dependent destruction H.
    destruct (IH a) as [p].
    exact (p r rfa).
Qed.

Definition wfInd P IH s : P s :=
  let wfInd := fix wfAcc s acc {struct acc} :=
    IH s (λ r rs, wfAcc r (acc.(accLt) r rs))
  in wfInd s (wf s).
\end{minted}

\subsubsection{W Types} \label{app:mechanization:coq:W}

\begin{minted}{coq}
Import SigTNotations.

Inductive W (A : Type) (B : A → Type) (s : Size) : Type :=
| sup : ∀ r, r < s → ∀ a, (B a → W A B r) → W A B s.
Arguments sup {_ _ _}.

Definition ac {A B} a (f : B a → {s & W A B s}) : {s & B a → W A B s} :=
  let f' b :=
    match (f b).2 with
    | sup r rs a f => sup r (transLeq rs (cocone b reflLeq)) a f
    end
  in (lim (λ b, (f b).1) ; f').
\end{minted}

\subsection{Mechanized \CICE Definitions in Agda}

The following type check on Agda 2.6.2.

\subsubsection{Preliminary definitions} \label{app:mechanization:agda:prelim}

\begin{minted}{agda}
{-# OPTIONS --without-K #-}

open import Agda.Primitive using (Level; lsuc)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
open import Data.Empty using (⊥; ⊥-elim)

variable
  ℓ ℓ′ : Level
  A C : Set ℓ
  B : A → Set ℓ

infix 30 ↑_
infix 30 ⊔_

data Size {ℓ} : Set (lsuc ℓ) where
  ↑_ : Size {ℓ} → Size
  ⊔_ : {A : Set ℓ} → (A → Size {ℓ}) → Size

data _≤_ {ℓ} : Size {ℓ} → Size {ℓ} → Set (lsuc ℓ) where
  ↑s≤↑s : ∀ {r s} → r ≤ s → ↑ r ≤ ↑ s
  s≤⊔f  : ∀ {s} f (a : A) → s ≤ f a → s ≤ ⊔ f
  ⊔f≤s  : ∀ {s} f → (∀ (a : A) → f a ≤ s) → ⊔ f ≤ s

◯ : Size
◯ = ⊔ ⊥-elim

◯≤s : ∀ {s} → ◯ ≤ s
◯≤s = ⊔f≤s ⊥-elim λ ()

s≤s : ∀ {s : Size {ℓ}} → s ≤ s
s≤s {s = ↑ s} = ↑s≤↑s s≤s
s≤s {s = ⊔ f} = ⊔f≤s f (λ a → s≤⊔f f a s≤s)

s≤s≤s : ∀ {r s t : Size {ℓ}} → r ≤ s → s ≤ t → r ≤ t
s≤s≤s (↑s≤↑s r≤s) (↑s≤↑s s≤t) = ↑s≤↑s (s≤s≤s r≤s s≤t)
s≤s≤s r≤s (s≤⊔f f a s≤fa) = s≤⊔f f a (s≤s≤s r≤s s≤fa)
s≤s≤s (⊔f≤s f fa≤s) s≤t = ⊔f≤s f (λ a → s≤s≤s (fa≤s a) s≤t)
s≤s≤s (s≤⊔f f a s≤fa) (⊔f≤s f fa≤t) = s≤s≤s s≤fa (fa≤t a)

s≤↑s : ∀ {s : Size {ℓ}} → s ≤ ↑ s
s≤↑s {s = ↑ s} = ↑s≤↑s s≤↑s
s≤↑s {s = ⊔ f} = ⊔f≤s f (λ a → s≤s≤s s≤↑s (↑s≤↑s (s≤⊔f f a s≤s)))

_<_ : Size {ℓ} → Size {ℓ} → Set (lsuc ℓ)
r < s = ↑ r ≤ s

record Acc (s : Size {ℓ}) : Set (lsuc ℓ) where
  inductive
  pattern
  constructor acc
  field acc< : (∀ r → r < s → Acc r)
open Acc

accIsProp : ∀ {s : Size {ℓ}} → (acc1 acc2 : Acc s) → acc1 ≡ acc2
accIsProp (acc p) (acc q) =
  cong acc (funext p q (λ r → funext (p r) (q r) (λ r<s →
    accIsProp (p r r<s) (q r r<s))))
  where postulate funext : ∀ (p q : ∀ x → B x) → (∀ x → p x ≡ q x) → p ≡ q

acc≤ : ∀ {r s : Size {ℓ}} → r ≤ s → Acc s → Acc r
acc≤ r≤s (acc p) = acc (λ t t<r → p t (s≤s≤s t<r r≤s))

wf : ∀ (s : Size {ℓ}) → Acc s
wf (↑ s) = acc (λ { _ (↑s≤↑s r≤s) → acc≤ r≤s (wf s) })
wf (⊔ f) = acc (λ { r (s≤⊔f f a r<fa) → (wf (f a)).acc< r r<fa })

wfInd : ∀ (P : Size {ℓ} → Set ℓ′) → (∀ s → (∀ r → r < s → P r) → P s) →
  ∀ s → P s
wfInd P f s = wfAcc s (wf s)
  where
  wfAcc : ∀ s → Acc s → P s
  wfAcc s (acc p) = f s (λ r r<s → wfAcc r (p r r<s))
\end{minted}

\subsubsection{W Types} \label{app:mechanization:agda:W}

\begin{minted}{agda}
open import Data.Product using (proj₁; proj₂; Σ-syntax; _,_)

data W (A : Set ℓ) (B : A → Set ℓ) (s : Size {ℓ}) : Set (lsuc ℓ) where
  sup : ∀ r → r < s → (a : A) → (B a → W A B r) → W A B s

ac : ∀ a → (B a → Σ[ s ∈ Size ] W A B s) → Σ[ s ∈ Size ] (B a → W A B s)
ac a f = ⊔ (λ b → proj₁ (f b)) , f′
  where
  f′ : _
  f′ b with proj₂ (f b)
  ... | sup r r<s a f = sup r (s≤s≤s r<s (s≤⊔f _ b s≤s)) a f
\end{minted}
\end{document}