Defunctionalization with Dependent Types

We use different colours and fonts to distinguish different languages, and we recommend reading or printing this paper in colour as it is easier to read.

Yulong Huang

University of Cambridge

Jeremy Yallop

University of Cambridge

The defunctionalization translation that eliminates
higher-order functions from programs forms a key part of many

However, defunctionalization for dependently-typed languages has not
been formally studied.

We present the first formally-specified defunctionalization translation
for a dependently-typed language and establish key metatheoretical properties
such as soundness and type preservation.

The translation is suitable for incorporation into type-preserving
compilers for dependently-typed languages.

<concept_desc>Software and its engineering General programming languages</concept_desc>
<concept_desc>Social and professional topics History of programming languages</concept_desc>

[500]Software and its engineering General programming languages
[300]Social and professional topics History of programming languages

§ INTRODUCTION

Types are increasingly used not merely for classification
(i.e. in identifying a subset of programs with desirable
properties), but for compilation.

A type-preserving compiler, organised as a series of
translations between two or more typed
languages <cit.>,
can support features such as type-driven elaboration of source
programs into more explicit core
calculi <cit.>,
translation of disparate source features into a simple uniform
core <cit.> and type-driven
optimizations <cit.>.

More generally, type-preserving translations between intermediate
languages can increase confidence in correctness of the compilation
process <cit.>.

As type systems increase in sophistication,
defining type-preserving presents new challenges.

Some of the most significant arise in the compilation of
dependently-typed languages such as
Agda <cit.>,
Idris <cit.>,
and Coq <cit.>,
whose type systems are sufficiently expressive to support arbitrary computation.

It has proved difficult to adapt long-studied translations such as
continuation-passing style conversion, closure
conversion, and conversion into administrative normal form to the dependently-typed
setting <cit.>.

Another such translation, defunctionalization, which eliminates
higher-order functions from programs, forms a key part of compilers
for several higher-order
languages <cit.>.

Type-preserving variants of defunctionalization are available for a
variety of type
systems <cit.>.

Defunctionalization is also useful in the compilation of dependently-typed languages,
such as Idris [<https://github.com/idris-lang/Idris-dev/blob/v1.3.4/src/IRTS/Defunctionalise.hs>].

However, to date no type-preserving variant of the defunctionalization
translation for dependently-typed languages has been developed.

This work meets that need, introducing a typed defunctionalization
translation for a dependently-typed language, and establishing its
fundamental properties.

As with previous work that has adapted similar program translations to
support dependent types, we have encountered and resolved various
difficulties that do not arise in simply-typed settings.

In particular,
the need to preserve universe sizes
(used by dependently-typed languages use to avoid inconsistencies), and
and to preserve reduction
(used to establish type equality)
make a straightforward adaption of the standard defunctionalization unfeasible.

§.§ Contributions

The central contribution of this paper is the first type-preserving
defunctionalization translation for a dependently typed language.  In
more detail,

* <Ref> shows that the type-preserving
defunctionalization translations used for simply typed
languages (<Ref>) do not extend to a
dependently-typed setting (<Ref>),
and presents an abstract translation suited to dependently-typed langauges

* <Ref> has the technical development
of our type-preserving defunctionalization translation.
<Ref> formally defines the abstract translation
and <Ref> and

key meta-theoretical properties such as soundness, type preservation,
and consistency.

Finally, <Ref> describes an implementation of
our translation (included as supplementary material), and
<Ref> summarises related work on
type-preserving compilation and on defunctionalization.

§ OVERVIEW

§.§ Defunctionalization

The defunctionalization translation
turns higher-order programs
into first-order programs,
by replacing the function arrow !- -> -!
with a first-order data type !-  > -!.

replaces each abstraction $\lambda x.e_i$
in the source program
with a constructor application $C_i\;\overline{y}$
where $C_i$ is a constructor of !-  > -!
and $\overline{y}$ are the free variables of the abstraction,

and replaces
each application $f\;x$
with $f\;\$\;x$,
where the infix operator $\$$ maps $C_i$ back to $e_i$.

Here is an example.

The polymorphic !compose! function
three abstractions,
here labeled
F2, and

[inner sep=0pt] (compose)

compose :: (b -> c) -> (a -> b) -> (a -> c)
compose = $\lambda$f$\;$->$\;\;\lambda$g$\;$->$\;\;\lambda$x$\;$->$\;\;$f (g x)

[anchor=south west,rectangle,draw,red,minimum height=3.5ex,minimum width=16ex] (f3) at ($(compose.south west) + (25.5ex,-1.1ex)$)   ;
[anchor=south west,rectangle,draw,red,minimum height=5.6ex,minimum width=24ex] (f2) at ($(compose.south west) + (18.5ex,-2.9ex)$)   ;
[anchor=south west,rectangle,draw,red,minimum height=7.7ex,minimum width=31.5ex] (f1) at ($(compose.south west) + (12ex,-4.7ex)$)   ;
[fill=white] at ($(f1.south) + (0,0.2ex)$) F1 ;
[fill=white] at ($(f2.south) + (0,0.2ex)$) F2 ;
[fill=white] at ($(f3.south) + (0,0.2ex)$) F3 ;

Defunctionalizing !compose! produces a data type ! >! with
one constructor for each abstraction.

Here !->! separates constructor arguments:
!F2! has one argument of type !b  > c!,
corresponding to !f! in F2 above, and
!F3! has two arguments,
corresponding to !f! and !g! in F3.

data ( >) a b where
F1 :: (b  > c)  > (a  > b)  > (a  > c)
F2 :: (b  > c) -> (a  > b)  > (a  > c)
F3 :: (b  > c) -> (a  > b) -> (a  > c)

Following <cit.>, the data type ! >! produced by defunctionalization is a generalized algebraic data type (GADT),
in which
the return type of each constructor
can have a distinct instantiation of the type parameters, and
constructor types can involve type variables
(such as !b! in the type of !F3!)
that do not appear in return types.

Defunctionalization also produces an operator !$\$$!
that maps the constructors of ! >! to the bodies
of the corresponding abstractions:

($\$$) :: (a  > b) -> a -> b
F1     $\$$ f = F2 f
F2 f   $\$$ g = F3 f g
F3 f g $\$$ x = f $\$$ (g $\$$ x)

Here !$\$$! maps !F1! and the argument $x$ to !F2 x!,
since the body of the abstraction F1 is F2, with !x! free.

Similarly, it maps !F3! to !f $\$$ (g $\$$ x)!
because the body of F3 is !f (g x)!.

Finally, defunctionalization
!->! with ! >! and
F1 with !F1!
in !compose! itself:

compose_ :: (b  > c)  > (a  > b)  > (a  > c)
compose_ = F1

Previous work on defunctionalization in typed settings has examined a variety of languages,
simply-typed <cit.> and
monomorphizable <cit.>
to fully polymorphic <cit.>.

In each case,
defunctionalization represents functions
using inductive data types,
from simple algebraic datatypes for simply-typed functions,
to the more powerful generalized algebraic data types for polymorphism.

Might the same approach,
extended to yet more powerful data types,
support defunctionalization of dependently-typed programs?

Polymorphic functions abstract over types
and defunctionalize to GADTs indexed by types.

By analogy, might dependent functions,
which abstract over expressions,
defunctionalize to inductive families indexed by expressions?

§.§ Inductive families

We briefly recall inductive families and their associated

Inductive families <cit.> generalize both
ordinary inductive data types and generalized algebraic data types by
permitting indexing by expressions.

The constructor of each inductive family may return an instantiation
of the family instantiated with arbitrary indexes.

For example, in the following Agda <cit.> definition the
constructors of the inductive family of finite sets, Fin,
are indexed by natural numbers n:

The constructor fzero constructs an element of type
Fin (suc n) for any n, while fsuc
constructs an element of type Fin (suc n) from an
element of type Fin n.

In general, inductive families (without parameters) have the following form:

data D : (y₁ : T₁) → … → (yₙ : Tₙ) → Setᵈ where
c₁ : A₁
c₁ : A₂

where D is an inductive family in Setᵈ indexed by
expressions of type T₁, $\ldots$, Tₙ.

For each constructor cᵢ,
it takes a number of arguments $(\AgdaBound{zᵢ}\;\AgdaSymbol{:}\;\AgdaDatatype{Sᵢ})$
and constructs an element of type $\AgdaDatatype{D}\;\AgdaBound{t₁}\;\ldots\;\AgdaBound{tₙ}$,
where each tᵢ is an expression of type Tᵢ.

Concretely, each Aᵢ takes the following form:

(z₁ : S₁) → … → (zₘ : Sₘ) → D t₁ … tₙ.

The arguments to D and c are dependently typed:
T$_{i+1}$ can mention y$_1$$\;\ldots\;$y$_i$,
and S$_{i+1}$ can mention z$_1$$\;\ldots\;$z$_i$.

are not bound in

To ensure that inductive family definitions are consistent, Agda imposes additional restrictions.

First, universe checking rejects inductive definitions with
impredicative constructors — that is, definitions whose constructors
inhabit a larger universe than the data types themselves.

More concretely, for a data type such as D above, the
universe of every argument type S$_i$ (i.e. the type of
S$_i$) should be smaller than Set$_d$ to
pass the universe check.

Without this restriction, inductive families can be used to encode
Girard's paradox.

Second, positivity checking rejects inductive families that
contain references to themselves in non-strictly-positive positions.

Without this restriction, inductive families such as the following
Fix can be used to build recursive definitions
that violate consistency, such as bad:

Strict positivity imposes two conditions on the constructor types
A$_i$ of an inductive family definition

First, where D appears, it must
not be indexed by expressions involving D itself.

Second, in the argument types S$_i$,
D must not occur to the left of function arrows.

These requirements around strict positivity and universes are shared
by many dependently-typed languages that support inductive families,
like Coq's Gallina <cit.>,
Lean <cit.>,
and Timany and Sozeau's
pCuIC <cit.>.

§.§ Problems extending defunctionalization to dependent types

At first glance, extending defunctionalization to support dependent
functions, targeting inductive families, appears straightforward.

As an example, we consider the defunctionalization of the following fully-dependent
compose function, written in Agda, with all arguments explicit for clarity:

Adapting Pottier and Gauthier's recipe, we start
by defining an inductive family $\Pi$ to represent dependent functions,
just as the GADT ! >! represents non-dependent functions:

Each dependent function type $\Pi x{:}A.f x$ (written !(x : A) $\to$ f x! in Agda) in the original program will be defunctionalized
to !$\Pi$ A f!.

Next, we add a constructor to $\Pi$ for each lambda abstraction in the
original program.

For example, the !F6! constructor corresponds to the
innermost abstraction, with free variables !A!,
!B!, !C!, !f! and !g!:

Finally, we add a case for each constructor to the definition of

<Ref> gives the full definitions.

Unfortunately, although these definitions are type-correct,
they do not satisfy Agda's additional checks.

First, universe checking rejects the definition of !F6! because
in the type of B the second argument of $\Pi$ (i.e. $\lambda \_ \to\;$Set)
inhabits the universe Set$_1$, which is larger than Set.

Second, positivity checking rejects the definition of
!F6! because in the type of C, $\Pi$ is indexed by an expression involving $\Pi$.

Finally, Agda's termination checking rejects the definition of
!$\$$! because the case for F6 is
not structurally terminating.

§.§.§ A simpler example

The example above suggests that although defunctionalization
apparently extends naturally to dependent types, the extension suffers
from consistency problems.

In fact, the situation is more grave: even if we do not make use of
dependency, the same problems with universe universes and positivity arise.

For example, here is a definition of a simply-typed
compose function, based on three fixed types
A, B, and

Defunctionalizing compose produces an inductive family
↝ and corresponding apply
function $:

Unfortunately, the simple definition ↝
suffers from the same problems as the more dependent $\Pi$.

First, universe checking rejects the constructor F1, because
the type B↝C
inhabits the universe Set$_1$, which is larger than Set.

Second, in the type of F1,
↝ is indexed by
↝ itself, so the definition fails positivity checking.

Finally, the F3 case of
$ fails termination checking because
the arguments to the recursive call are not structurally smaller than
the parameters.

§.§.§ An expressivity mismatch

§.§ Abstract defunctionalization

The examples above suggest that the extension of defunctionalization
to dependent types is type-preserving

It is also possible to show that it is meaning-preserving

observe, when
defunctionalization produces a single polymorphic apply function, it
coincides with the untyped defunctionalization translation.

Pottier and Gauthier use this coincidence to prove that the typed
translation is meaning-preserving by lifting a proof about the untyped

We might similarly lift the proof to the dependently-typed setting to
establish the correctness of the extended translation.

Since the extended defunctionalization translation appears to preserve
types and meanings, it is disappointing that it falls foul of various

How might we build a translation that does not violate these checks?

We might We might note
that the Agda's restrictions are only fairly crude syntactic approximations
of semantic properties,
that programs that breach them are not necessarily “incorrect”, and
that we have good reason to believe that the programs generated by
defunctionalizing correct programs are also correct.

A similar approach has been taken
by <cit.> (for universe checking), and
by <cit.> (for all three checks), among

However, we do not favour taking off the safety guards in this way for
the code generated by defunctionalization.

In our view, the fact that Agda rejects the inductive families
generated by defunctionalization suggests that inductive families are
not well ill suited to the task.

For example, the universe restriction that rejects the constructors of
$\Pi$ $\Pi$ does not apply to the closures that correspond to those
constructors in the source program: there is nothing requiring a free
variable in an abstraction body to inhabit a smaller universe than the
function itself.

The additional restriction arises from an expressivity mismatch: the
universe restriction is only needed when inductive families are not
used in a closure-like fashion — for example, e.g. when constructor
arguments are extracted.

§.§ Abstract defunctionalization

The examples above suggest that the extension of defunctionalization
to dependent types is type-preserving.

It is also possible to show that it is meaning-preserving.

observe, when
defunctionalization produces a single polymorphic apply function, it
coincides with the untyped defunctionalization translation.

Pottier and Gauthier use this coincidence to prove that the typed
translation is meaning-preserving by lifting a proof about the untyped

We might similarly lift the proof to the dependently-typed setting to
establish the correctness of the extended translation.

Since the extended defunctionalization translation appears to preserve
types and meanings, it is disappointing that it falls foul of Agda's
various restrictions.

How might we build a translation that does not violate these checks?

We consequently choose to follow instead the direction taken by
<cit.> and
<cit.> for closure conversion, and study
defunctionalization for a dependently typed language in an abstract

We introduce an abstract type of labels
for the target language
, which are less expressive than inductive families, and consequently do not require the same restrictionsabstract closure conversion,
which studies closure conversion for a specialized target language
with new constructs for representing closures and closure types.

Defunctionalization into these labels Closure conversion into these constructs captures the essence of the
translation, while avoiding the unnecessary restrictions imposed by more
concrete settings.

Similarly, we will define a target language, the
Defunctionalized Calculus of Constructions (DCC), in the style
of lambda calculus, but with a new construct for defunctionalized
labels (representing indexes into a label context) in
place of lambda abstractions.

shows the result of defunctionalizing
the simply-typed

function to DCC [We assume that $A$, $B$, and
$C$ are base types here.], which looks and behaves like the
conventional defunctionalization presented in

In our translation into DCC, each abstraction $\lambda x.e_i$ is
replaced with a label expression $ \target{\flabel_  i  }   \ottsym{\{}   \target{\overline{ \target{y} } }   \ottsym{\}}$ where $\target{\flabel_i}$ is
the label's identifier and $\target{\overline{y}}$ are the
abstraction's free variables.

The function body $e_i$ is stored in a separate label context
$\target{\fdef}$ indexed by the label identifier, along with its
typing information.

, the label context $\target{\fdef}$ has
three entries, one for each abstraction in the original

Each entry corresponds to one case of the $\$$ function in the
conventional defunctionalization.  For example, $ \target{\flabel_ \ottsym{3} } $ arises from the translation of $\lambda x \mathrel{:} A .\ f\ (g\ x)$,
and corresponds to the

case in the definition of $\$$:
it has two free variables $\target{f} \mathrel{:} \target{B} \rightarrow \target{C} $ and
$\target{g} \mathrel{:} \target{A} \rightarrow \target{B}$,
a bound variable $\target{x}$, and a body $ \target{f} \,\target{ \mathop{@} }\,  (  \target{g} \,\target{ \mathop{@} }\, \target{x}  )  $.

As we shall see, a label application $  \target{\flabel_ \ottsym{3} }   \ottsym{\{}  \target{f}  \ottsym{,}  \target{g}  \ottsym{\}} \,\target{ \mathop{@} }\, \target{N} $
reduces to $ \target{f} \,\target{ \mathop{@} }\,  (  \target{g} \,\target{ \mathop{@} }\, \target{N}  )  $, just as the application

!(F3 f g) $\$$ x!

reduces to the corresponding right hand
!f $\$$ (g $\$$ x)!

Defunctionalized simply-typed composition

It is straightforward to add dependent types to this scheme,
but some care is needed to define the transformation and
show that it has the desired meta-theoretical properties.

In particular, as we shall see, the transformation needs to consider
the entire derivation tree rather than just the source language expression (

and we need to use a version of the source language with explicit substitutions (
to make the type-preservation proof go through.

These challenges arise only in defunctionalization in a dependently typed setting,
which has not been previously studied.

§ DEFUNCTIONALIZING WITH DEPENDENT TYPES

Having informally introduced the key concepts and motivated our abstract
defunctionalization translation, we now turn to the technical details.

The next few sections introduce
our source language, the calculus of constructions (<Ref>),
our target language, the defunctionalized calculus of constructions (<Ref>),
and the defunctionalizion translation that links them (<Ref>).

After presenting the translation we establish its soundness We then establish the soundness of the translation (<Ref>)
and prove the consistency of the target language (

§.§ Calculus of Constructions

Our source language is a variant of the Calculus of Constructions
(CC) <cit.>, an expressive
dependently-typed lambda calculus that serves as a basis for several
programming languages and proof assistants.

Our main departure from the original presentation of CC is in following the
approach taken by <cit.>, and by many
dependently-typed languages such as Agda, Lean, Coq, and F*, by extending
CC with a Martin-Löf style hierarchy of universes.

Here is an example CC definition, $\text{compose}$, which represents the fully dependent composition
function for functions $f$ and $g$:

\[
\begin{array}{rcl}
\text{compose} &::=& \lam{A}{U_0}
{\enspace \lam{B}{(\pitype{x}{A}{U_0})}
{\enspace \lam{C}{(\pitype{x}{A}{\pitype{y}{B\ x}{U_0}})}{} }}\\
&& \quad \lam{f}{(\pitype{y}{A}{(\pitype{z}{B\ y}{C\ y\ z})})}
{\enspace \lam{g}{(\pitype{x}{A}{B\ x})}{} }\\
&& \qquad \lam{x}{A}{\enspace f\ x\ (g\ x)}
\end{array}
\]

The expression component $\lambda A. \lambda B. \lambda C. \lambda f. \lambda g. \lambda x. f\;x\;(g\;x)$ of this definition  is unremarkable;
all the interest is in the dependencies of types on arguments.

In particular, the result type $C\ y\ z$ of $f$ depends on $f$'s arguments $y$ and $z$
the result type $B\ x$ of $g$ depends on $g$'s argument $x$.

(In a practical programming language, both $y$ and the type arguments
$A$, $B$ and $C$ would be passed implicitly,
but our minimal calculus does not support implicit arguments.)

Expressions     A,B,L,M,N      ::=     x  |U  |Πx  :  A . B   |L   M  |λx  :  A . M

Universes       U           ::=     U_i

Contexts     Γ     ::=     ·|Γ,  x  :  A

[red]$M  \mathrel{\triangleright}  N$Reduction

[ty]$\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$Typing

[wf]$\vdash  \Gamma$Well-formedness

Context formation

[eq]$\vdash  \ottnt{M}  \equiv  \ottnt{N}$Equivalence

The Calculus of Constructions (CC)

<Ref> shows the syntax of CC.

The expressions of CC are variables $\ottmv{x}$ (drawn from an infinite set of names), universes $U$, dependent function types $ \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $, applications $ \ottnt{L} \; \ottnt{M} $, and abstractions $ \lambda  \ottmv{x}  {:}  \ottnt{A} . \ottnt{M} $. A CC context $\Gamma$ is a telescope of variable-expression pairs.

CC has four judgements:

* reduction (<Ref>)

\[
M  \mathrel{\triangleright}  N
\]

* type membership (<Ref>)

\[
\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}
\]

* context formation (<Ref>)

\[
\vdash  \Gamma
\]

* equivalence (<Ref>)

\[
\vdash  \ottnt{A}  \equiv  \ottnt{B}
\]

There is a single reduction rule (<Ref>), for  $\beta$-reduction, $  (  \lambda  \ottmv{x}  {:}  \ottnt{A} . \ottnt{N}  )  \; \ottnt{M}  \mathrel{\triangleright}  \ottnt{N} [  \ottnt{M}  \ottsym{/}  \ottmv{x}  ] $.

We write $\ottnt{L}  \triangleright^*  \ottnt{M}$ to mean that $\ottnt{L}$ reduces to $\ottnt{M}$ in a sequence with zero or more steps.

CC's rules for typing (<Ref>) and context formation (<Ref>) are defined by mutual induction.

The type of a variable $x$ is $A$ if $x:A$ is present in the well-formed context $\Gamma$ (*ty-Var).

The type of a universe $U_i$ is $U_{i+1}$ (*ty-Universe),

and the type of $ \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $ is the higher universe among universes of $A$ and $B$ (*ty-Pi).

If $M$ has type $B$ in some context $\Gamma$ extended with $x{:}A$,
then $ \lambda  \ottmv{x}  {:}  \ottnt{A} . \ottnt{M} $ has the dependent function type $ \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $ (*ty-Lambda).

Applications have types $B[N/x]$, since the output of a function type may depend on the argument $N$ (*ty-Apply).

Finally, if an expression $M$ has type $A$ and $A$ is equivalent to $B$, then $M$ also has type $B$ (*ty-Equiv).

A context $\Gamma$ is well-formed (written $\vdash  \Gamma$) if
every variable in it is associated with a valid type — that is, the
associated expression’s type is a universe in the context $\Gamma$.

We make use of two shorthands, writing $\Gamma  \vdash  \ottnt{A}  \ottsym{:}  \ottnt{U}$ to mean that $\Gamma  \vdash  \ottnt{A}  \ottsym{:}  \ottnt{U_{\ottmv{i}}}$ for some $i$ (which means that $A$ is a type),
and $\ottnt{A} \to \ottnt{B}$ to stand for the $\Pi$-type $ \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $ where $B$ does not depend on $x$.

For simplicity, we omit base types such as the unit type $1$ and the
natural numbers $\Bbb{N}$ from the formal definition, but we will use
them freely in examples.

In CC, two expressions are equivalent (<Ref>) if they reduce to the same expression (*eq-Reduce) or are $\eta$-equivalent
as defined by two symmetric rules *eq-Eta1 and *eq-Eta2.

Under rule *eq-Eta1, $L$ and $M$ are equivalent if $L$ reduces to an abstraction $ \lambda  \ottmv{x}  {:}  \ottnt{A} . \ottnt{L'} $, $M$ reduces to some $M'$, and $\ottnt{L'} \equiv  \ottnt{M'} \; \ottmv{x} $, and rule *eq-Eta2 corresponds symmetrically

One useful property of CC is as follows: if $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$, then $\Gamma  \vdash  \ottnt{A}  \ottsym{:}  \ottnt{U}$, and so the derivation tree of $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$ must contain a sub-derivation of $\Gamma  \vdash  \ottnt{A}  \ottsym{:}  \ottnt{U}$.

Furthemore, CC is type safe and consistent, and type-checking in CC is decidable <cit.>.

§.§ Defunctionalized Calculus of Constructions

Universes       U            ::=     U_i

Expressions     A,B,L,M,N      ::=
| x  A  B

Type contexts     Γ     ::=

Label contexts          ::=
|  ,      ({   x     :    A    } ,  x  :  A    →↦M  :  B )

DCC contexts

[d-red]$\target{\fdef}  \vdash  \target{M}  \mathrel{\triangleright}  \target{N}$

[d-ty]$\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$Typing

[d-wf]$\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma}$Well-formedness

Context and label context formation

[d-eq]$\target{\fdef}  \vdash  \target{M}  \equiv  \target{N}$Equivalence

The Defunctionalized Calculus of Constructions (DCC)

<Ref> shows the syntax of our target language, the
Defunctionalized Calculus of Constructions (DCC).

As in CC, DCC expressions include
variables $\target{x}$,
universes $\target{U}$,
dependent function types $ \targetpi{ \target{x} }{ \target{A} }{ \target{B} } $,
applications $\targetapp{L}{M}$.

Unlike CC, DCC contains first-class function labels
$ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$ instead of lambda abstractions.

A label expression $ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$ is a label name
$\target{\flabel}$ supplied with a list of zero or more expressions
$\target{\overline{M}}$ (standing for $\target{M_1}, \cdots,
\target{M_n}$) assigned to its free variables.

Label names $\target{\flabel_1}, \target{\flabel_2}, \cdots$ are
disjoint from variable names, as we emphasize using a different font.

There are two varieties of context in DCC.

As in CC, type contexts $\target{\Gamma}$ associate variables
$\target{x}$ with types $\target{A}$.

Label definition contexts $\target{\fdef}$ pair label names with their associated data:
$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} ) $$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} ) $.

Here $ \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } } $ records the type of the (possibly empty)
telescope of free variables that the label takes, $\target{x}
\mathrel{\target{:}} \target{A} \to \target{B}$ $(\target{x}
\mathrel{:} \target{A}) \to \target{B}$ specifies the label type, and
$\target{M}$ is the expression to which the label reduces when applied to
an argument.
Note that types in a type context $\target{\Gamma}$
may refer to labels $\target{\flabel_1}, \target{\flabel_2}, \cdots$
in the label context $\target{\fdef}$, but not vice versa.

DCC has four judgements:

* reduction (<Ref>)

\[
\target{\fdef}  \vdash  \target{M}  \mathrel{\triangleright}  \target{N}
\]

* type membership (<Ref>)

\[
\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}
\]

* context formation (<Ref>)

\[
\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma}
\]

* equivalence (<Ref>)

\[
\target{\fdef}  \vdash  \target{A}  \equiv  \target{B}
\]

§.§.§ Reduction

There is a single reduction rule (<Ref>), for label
application: the application of the label
$ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$ to the argument $\target{N}$ reduces to
$\target{L}  \ottsym{[}   \target{\overline{ \target{M} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{,}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$,
where $\target{L}$ is the body of the entry for $ \target{\flabel} $ in the label context
and $ \target{\overline{ \target{M} } } $ is the closure of $ \target{\flabel} $.
A reduction sequence is noted
as $\target{\fdef}  \vdash  \target{M}  \triangleright^*  \target{N}$, which means
$\target{M}$ reduces to $\target{N}$ in zero or more steps.

Substitutions for variables, universes, $\Pi$-types and applications
in DCC follow the conventional definition. Substitutions for labels

\begin{equation*}
\target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]} \triangleq  \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}  \ottsym{\}},
\end{equation*}

where $ \target{\overline{ \target{M} } }   \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$ is a syntactic sugar for
$\target{M_1}\targetsub{N}{x}, \cdots, \target{M_n}\targetsub{N}{x}$.

§.§.§ Type judgements

DCC's type judgements are of the form $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$,
and typing rules are given in Figure <ref>
Rules for variables, universes, $\Pi$-types, applications,
and conversion are identical to their counterpart rules in CC, so we
focus on the rule for labels. A label term
$ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$  is well-typed in $\targetcon$ if the
following conditions are satisfied.

* The context $\targetcon$ is well-formed.

* $  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} ) $ $  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} ) $ is present in $\target{\fdef}$.

* The length of the two lists $\target{\overline{M}}$ and
$\itemtype{\overline{x}}{\overline{A}}$ are equal.

* All expressions in $\target{\overline{M}}$ are well-typed,
and their types match the specified types of free variables

Specifically, condition (4) means:

\begin{align*}
&\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash   \target{ \target{M} _ \ottsym{1} }   \ottsym{:}   \target{ \target{A} _ \ottsym{1} } , \DIFdelbegin %DIFDELCMD < \\
%DIFDELCMD <   %%%
\DIFdelend \DIFaddbegin \\[-0.1ex]
\DIFaddend &\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash   \target{ \target{M} _ \ottsym{2} }   \ottsym{:}   \target{ \target{A} _ \ottsym{2} }   \ottsym{[}   \target{ \target{M} _ \ottsym{1} }   \ottsym{/}   \target{ \target{x} _ \ottsym{1} }   \ottsym{]}, \DIFdelbegin %DIFDELCMD < \\
%DIFDELCMD <   %%%
\DIFdelend \DIFaddbegin \\[-0.1ex]
\DIFaddend &\cdots,\DIFdelbegin %DIFDELCMD < \\ %%%
\DIFdelend \DIFaddbegin \\[-0.1ex] \DIFaddend \
&\targetcon \vdash
\itemtype{M_n}{A_n}[\target{M_1} \slash \target{x_1},
\cdots, \target{M_{n-1}} \slash \target{M_{n-1}}].
\end{align*}

Each $\target{A_{i+1}}$ depends on $\target{x_1}, \cdots,
\target{x_i}$, so $\target{M_1}, \cdots, \target{M_i}$ need to be
substituted in $\target{A_{i+1}}$ in the type judgement for
The type of $ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$ is $ \targetpi{ \target{x} }{  \target{A}  \ottsym{[}   \target{\overline{ \target{M} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{]}  }{  \target{B}  \ottsym{[}   \target{\overline{ \target{M} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{]}  } $.

Note that values of free variables $\target{\overline{M}}$ are substituted
in $ \targetpi{ \target{x} }{ \target{A} }{ \target{B} } $, the specified type of the label. We use
$\targetsub{\overline{M}}{\overline{x}}$ as a syntactic sugar of
$[\target{M_1}\slash\target{x_1}\sfcomma \cdots\sfcomma
\target{M_n}\slash\target{x_n}]$, and conditions (3) and (4) are
abbreviated to $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash   \target{\overline{ \target{M} } }   \ottsym{:}   \target{\overline{ \target{A} } } $ as a

The DCC judgement for well-formed contexts is $\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma}$
and its rules are given in Figure <ref>
A context is well-formed if every variable in the type context
is associated with a valid type (in the previous context $\targetcon$),
and every label is associated with a well-typed data.
In other words, if we have $  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} ) $$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} ) $,
$\target{M}$ should have the type $\target{B}$ as specified
in the context formed by the previous label context and the free variables in $\target{M}$
(namely $\target{\fdef} ;  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }   \ottsym{,}  \target{x}  \ottsym{:}  \target{A}$).

Two terms $\target{L}$ and $\target{M}$ are equivalent (Figure <ref>
) if they
both reduce to the same term $\target{N}$ in a reduction sequence or
they are $\eta$-equivalent. DCC's $\eta$-equivalence rules are similar
to that of CC.  Rule (*d-eq-Eta1) defines that
$\target{L}$ and $\target{M}$ are equivalent if
$\target{L}$ reduces to a label $ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{N} } }   \ottsym{\}}$,
$\target{M}$ reduces to $\target{M'}$,
$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{N}  :  \target{B} ) $ $  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{N}  :  \target{B} ) $ is found in the label context $\target{\fdef}$,
and $ \target{M}' \,\target{ \mathop{@} }\, \target{x} $ is equivalent to $\target{N}  \ottsym{[}   \target{\overline{ \target{N} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{]}$.
Rules (*d-eq-Eta1) and (*d-eq-Eta2) are

Both the type context and the label context have the weakening property– : a well-typed expression is still well-typed in an extended type or label context (by induction on the type derivation rules).

If $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$, $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{B}  \ottsym{:}   \target{U}_{\target{  i  } } $, and $\target{x}$ is fresh,
then ${\target{\fdef}  \ottsym{;}  \target{\Gamma}  \ottsym{,}  \target{x}  \ottsym{:}  \target{B}  \vdash  \target{M}  \ottsym{:}  \target{A}}$.

If  $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{C}$, $\target{\fdef}  \ottsym{;}   \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }   \ottsym{,}  \target{x}  \ottsym{:}  \target{A}  \vdash  \target{N}  \ottsym{:}  \target{B}$, and $ \target{\flabel_  i  } $ is fresh,
then ${\target{\fdef}  \ottsym{,}    \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{N}  :  \target{B} )   \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{C}}$${\target{\fdef}  \ottsym{,}    \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{N}  :  \target{B} )   \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{C}}$.

DCC is type-safe and consistent
(we establish these properties in

In addition, it is sufficiently expressive to support the $\text{compose}$ function,
but we must write it in defunctionalized style, since the calculus
does not support lambda abstraction.

There is one entry in the label context $\target{\fdef}$ for each $\lambda$ in the CC definition of $\text{compose}$:

and the definition of $\text{compose}$ itself is simply a projection of a closed label from the context:

\targettext{compose}  &::=&  \target{\flabel_ \ottsym{0} }   \ottsym{\{}      \ottsym{\}}\\
\end{array}$

The full definition appears in <Ref>.

§.§ The Defunctionalization Translation

[t]$\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}  \leadsto  \target{M}$Expression transformation

Defunctionalization of expressions

[d]$\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}  \leadsto_d  \target{\fdef}$Function extraction

Extraction of function definitions

The Defunctionalization Translation

<Ref> shows the translation. It consists of two parts: a transformation $\bbracket{-}$ for expressions and a meta-function $\bbracket{-}_d$ that extracts function definitions from the source program. The expression transformation produces the target program and the meta-function $\bbracket{-}_d$ gives a label context.

§.§.§ Expression transformation

We define the  The expression transformation $\bbracket{-}$
using a takes a well-typed term in CC and an implicit argument of that term's type derivation.
We define $\bbracket{M} \triangleq \target{M}$, where $\target{M}$ is given by a new judgement
of the form $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}  \leadsto  \target{M}$ . Figure <ref> gives the derivation rules of this judgement.

The transformation simply transcribes the variables, universes, $\Pi$-types, applications, and base types and values in CC to their counterparts in DCC compositionally. Functions in the source language are translated into labels in the target language.

Defunctionalization requires a unique correspondence between each label and each source-program function.
We use a convention that every function lambda in the transformation's input $M$ is tagged with a unique identifier $i$ ($i \in \mathbb{N}$), and its corresponding label's name is $\target{\flabel_i}$.
Furthermore, $\alpha$-equivalent functions are assigned the same tag.

The transformation turns a function $ \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M} $ into a label $ \target{\flabel_  i  }   \ottsym{\{}   \target{\overline{ \target{x} } }   \ottsym{\}}$, where $\target{\overline{x}}$ come from the function's free variables $\overline{x}$ (*t-Lambda). The meta-function FV (see Definition <ref>
) computes all free variables and their types involved in a well-typed CC-expression. Note that FV is different from fv, the conventional free variable function that computes all the unbound variables in an expression. In dependently typed languages, the type of a free variable may contain other free variables, and their types may still contain other free variables, and so on! Therefore, FV$(M)$ must recursively work out all the variables needed for $M$ to be well-typed.

FV$(M)$ takes $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$, the type judgement of $M$, as an implicit argument. It firstly computes all the unbound variables $x_1, \cdots, x_n$ in $M$ and in $A$, then calls itself recursively on types of these variables, and finally returns the union of all free variables and their types it found.

\begin{equation*}
\DIFdelbegin %DIFDELCMD < \renewcommand{\arraystretch}{1.3}
%DIFDELCMD < %%%
\DIFdelend \DIFaddbegin \renewcommand{\arraystretch}{1.1}
\DIFaddend \begin{array}{l l l}
\text{FV}(M) & = & \text{FV}(A_1) \cup \cdots \cup \text{FV}(A_n) \cup \Gamma_{fv}\\
& \text{where} & \emph{fv }(M) \cup \emph{fv }(A) = x_1, \cdots, x_n\\
& & \Gamma \vdash x_1 \goodcolon A_1, \cdots, \Gamma \vdash x_n \goodcolon A_n\\
& & \Gamma_{fv} \triangleq x_1 \goodcolon A_1, \cdots, x_n \goodcolon A_n.\\
\end{array}
\end{equation*}

Here, the union of two type contexts ${\Gamma_1} \cup {\Gamma_2}$ is ${\Gamma_1}$ appended with all the variable-expression pairs ${x} \goodcolon {A}$ that only appear in ${\Gamma_2}$, preserving their order.

Intuitively, $ FV( \ottnt{M} ) $ computes all the variables needed to correctly type $M$.
Therefore, $M$ is still well-typed in its free-variable context $ FV( \ottnt{M} ) $.

If $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$, then $ FV( \ottnt{M} )   \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$.

§.§.§ Extracting function definitions

The expression transformation is not a complete definition of
defunctionalization, since it turns functions into labels and simply
discards function bodies.

We also need a meta-function $\bbracket{-}_d$, that builds a label
context from a CC-expression.

$\bbracket{-}_d$ takes a well-typed CC term and implicitly its type derivation.
We define $\bbracket{M}_d \triangleq \target{\fdef}$, where $\target{\fdef}$ is given by a new judgement
of the form $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}  \leadsto_d  \target{\fdef}$ (

In a simply typed system, the only thing $\bbracket{-}_d$ has to do is
finding every function $ \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M} $ in the source program
and placing them in the label context $\target{\fdef}$ contains the implementation of that function as an
item of the following form
, in the following form

\begin{equation*}
\DIFadd{\target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} )

$\{\itemtype{\overline{x}}{\overline{A}}\}$, $\target{x} :
\target{A}$, $\target{M}$, and $\target{B}$ respectively correspond to the free variables
$(\overline{x} \mathrel{:} \overline{A})$ in the function, the bound
variable $x : A$, the function body $M$, and the return type $B$.

({   x     :    A    } ,  x  :  A    →M  :  B )

Function extraction is more subtle than expression transformation. Functions may

Alas, types may index over functions in our dependent type theory, and
functions may appear in the type of an expression,
even if the expression itself does not contain that function!
For example, consider the following CC context and expression (with base type natural numbers $Nat$).
triple $(\Gamma,M,N)$ in CC
(with built-in natural numbers and addition).

\begin{align*}
\Gamma\ & \triangleq\ \cdot,\ A \goodcolon (Nat \rightarrow Nat) \rightarrow U_0,\
a \goodcolon\ \DIFdelbegin %DIFDELCMD < \pitype{f}{(Nat \rightarrow Nat)}{A\ (\lam{n}{Nat}{(f\ n) + 1})} %%%
\DIFdelend \DIFaddbegin \pitype{f}{(Nat \rightarrow Nat)}{A\ (\lam{n}{Nat}{1 + (f\ n)})} \DIFaddend \\
M\ & \triangleq\ a\ (\DIFdelbegin %DIFDELCMD < \lam{x}{Nat}{x+1}%%%
\DIFdelend \DIFaddbegin \lam{x}{Nat}{1+x}\DIFaddend ) \DIFaddbegin \\
\DIFadd{N\ }& \DIFadd{\triangleq A\ (}\lam{n}{Nat}{2+n}\DIFadd{)
}\DIFaddend \end{align*}

$A$ is a family of types indexed by functions of type $Nat \rightarrow Nat$ functions and
$a\ f$ constructs an element of type $A\ (\lam{n}{Nat}{(f\ n) + 1})$$A\ (\lam{n}{Nat}{1 + (f\ n)})$.
According to the rule (*ty-Apply), the inferred type of $M$ is

\begin{align*}
& (A\ (\DIFdelbegin %DIFDELCMD < \lam{n}{Nat}{(f\ n) + 1}%%%
\DIFdelend \DIFaddbegin \lam{n}{Nat}{1 + (f\ n)}\DIFaddend ))\DIFdelbegin %DIFDELCMD < \sub{(\lam{x}{Nat}{x+1})}{f}%%%
\DIFdelend \DIFaddbegin \sub{(\lam{x}{Nat}{1 + x})}{f}\DIFaddend \\
=\ & A\ (\DIFdelbegin %DIFDELCMD < \lam{n}{Nat}{((\lam{x}{Nat}{x+1})\ n) + 1}%%%
\DIFdelend \DIFaddbegin \lam{n}{Nat}{(1 + (\lam{x}{Nat}{1 + x})\ n)}\DIFaddend )\DIFdelbegin \DIFdel{.
}\DIFdelend \DIFaddbegin \DIFadd{,
}\DIFaddend \end{align*}

Hence, a new function definition appeared in the type of
which reduces to $A\ (\lam{n}{Nat}{2+n})$.

We have $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{N}$, yet $N$ contains a function that is not
in $\Gamma$ or $M$as the
result of a substitution.

This new function should be included in the label context
We should include this new function in $\target{\fdef}$so that it can be typed. Extracting function
definitions in $M$ involes finding every function that appeared in the
type derivation of $M$.
as it guarantees that we will never be in a situation
where we need a non-existent label in $\bbracket{M}_d$
to type $\bbracket{M}$.

In other words, the transformation
defunctionalizes not just the source-language expression, but its
entire type derivation tree.

We define $\bbracket{-}_d$ with a new judgement of the form $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}  \leadsto_d  \target{\fdef}$, and $\bbracket{M}_d \triangleq \target{\fdef}$. Figure <ref> gives the derivation rules of this judgement.

Variables do not contain function definitions , so the definitions in Hence, we arrive at the rules in

Type derivations of universes do not involve functions at all (*d-Universe).

Function definitions in a variable $x$ are just the definitions in its type $A$ (*d-Var).  Type derivations of universes do not involve functions at all (
). Definitions in a dependent function type $\pitype{x}{A}{B}$ are the union of definitions in $A$ and $B$ (*d-Pi). The union here is defined in the same way as the union of contexts (see Definition <ref>
), and there is no ambiguity since different functions correspond to different label names.

Definitions in an application $ \ottnt{M} \; \ottnt{N} $ are the union of definitions in $M$, $N$, and $B\sub{N}{x}$,
since substitution creates the substitution $B\sub{N}{x}$ may create new function definitions (*d-Apply).
For a lambda abstraction $ \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M} $, the definitions it contains are the union of definitions in $M$ and in $A$ appended with $\target{\flabel_i}$, the definition of itself (*d-Lambda).
If $M$ has type $B$ by the conversion rule, then the definitions involved in the derivation of $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$ are the union of definitions in the derivation of $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$ and definitions in $B$ (*d-Equiv).

We define the subset relation of label contexts to help state further definitions and theorems.

For two well-formed label contexts $\target{\fdef}_{{\mathrm{1}}}$ and $\target{\fdef}_{{\mathrm{2}}}$, $\target{\fdef}_{{\mathrm{1}}} \subseteq \target{\fdef}_{{\mathrm{2}}}$
if for all
$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{N}  :  \target{B} ) $
$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{N}  :  \target{B} ) $
$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{N}  :  \target{B} ) $
$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{N}  :  \target{B} ) $
is also in

The notion of subsets gives a stronger weakening property to DCC: a well-typed expression is still well-typed in a larger label context.

If $ \target{ \target{\fdef} _ \ottsym{1} }   \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$, $\vdash   \target{ \target{\fdef} _ \ottsym{2} } $, and $  \target{ \target{\fdef} _ \ottsym{1} }   \subseteq   \target{ \target{\fdef} _ \ottsym{2} }  $,
then $ \target{ \target{\fdef} _ \ottsym{2} }   \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$.

Since the transformation defunctionalizes the entire type derivation tree of an expression,
if $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$, then all elements in $ \bbracket{ \ottnt{A} }_d $ are also in $ \bbracket{ \ottnt{M} }_d $.
We can prove this property by induction on the type derivation rules.

For any well-typed expression $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$ in CC, $  \bbracket{ \ottnt{A} }_d   \subseteq   \bbracket{ \ottnt{M} }_d  $.

By induction on rules defined in <Ref>.

Case (*d-Lambda). The goal is to show that $  \bbracket{  \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B}  }_d   \subseteq   \bbracket{  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  }_d  $.
By assumption,

\begin{equation*}
\Gamma  \vdash   \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}   \ottsym{:}   \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B}   \leadsto_d    \target{ \target{\fdef} _ \ottnt{A} }   \cup    \target{ \target{\fdef} _ \ottnt{M} }   \ottsym{,}    \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \DIFdelbegin \DIFdel{\rightarrow  }\DIFdelend \DIFaddbegin \DIFadd{\mapsto  }\DIFaddend \target{M}  :  \target{B} )   .
\end{equation*}

In other words, $ \bbracket{  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  }_d  =   \bbracket{ \ottnt{A} }_d   \cup   \bbracket{ \ottnt{M} }_d  $ with definition of function $\lambda^i$ appended to it.
By definition, $ \bbracket{  \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B}  }_d  =   \bbracket{ \ottnt{A} }_d   \cup   \bbracket{ \ottnt{B} }_d  $. We have $  \bbracket{ \ottnt{A} }_d   \subseteq   \bbracket{  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  }_d  $ and $  \bbracket{ \ottnt{B} }_d   \subseteq   \bbracket{  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  }_d  $ by the induction hypothesis (since $\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{A}  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$, $  \bbracket{ \ottnt{B} }_d   \subseteq   \bbracket{ \ottnt{M} }_d  $).

Other cases are either trivial or follows simply from definitions.

The expression transformation and the process of extracting function definitions ($\bbracket{-}$ and $\bbracket{-}_d$) act pointwise on CC contexts. In other words,

\begin{equation*}
\begin{array}{l @{\qquad} l}
\bbracket{\cdot}\ \triangleq\ \target{\cdot},\  & \bbracket{\Gamma, x \goodcolon A}\ \triangleq \bbracket{\Gamma}\sfcomma \target{x} \goodcolon \bbracket{A},\\
\bbracket{\cdot}_d \triangleq\ \target{\cdot},\  & \bbracket{\Gamma, x \goodcolon A}_d \triangleq \bbracket{\Gamma}_d\cup\bbracket{A}_d.\\
\end{array}
\end{equation*}

Now, we can see that the (tagged) composition function
$\lambda^0 A. \lambda^1 B. \lambda^2 C. \lambda^3 f. \lambda^4 g. \lambda^5 x. f\;x\;(g\;x)$
transforms to $ \target{\flabel_ \ottsym{0} }   \ottsym{\{}      \ottsym{\}}$, a label with no free variables supplied,
since the function is closed.
The label context $\target{\fdef}$ for composition can be derived from the function extraction judgements
with the sketch derivation tree shown below.

$A, B, C, f, g \vdash \lambda^5x.f\;x\;(g\;x)
\leadsto_d \target{\flabel_5}(\{\target{A},\target{B},\target{C},\target{f},\target{g}\}, \target{x}:\_ \mapsto    (  \target{f} \,\target{ \mathop{@} }\, \target{x}  )  \,\target{ \mathop{@} }\, \target{g}  \,\target{ \mathop{@} }\, \target{x}  : \_ )

$A, B, C, f \vdash \lambda^4g.\lambda^5x.f\;x\;(g\;x)
\leadsto_d \cdots, \target{\flabel_4}(\{\target{A},\target{B},\target{C},\target{f}\}, \target{g}:\_ \mapsto  \target{\flabel_ \ottsym{5} }   \ottsym{\{}  \target{A}  \ottsym{,}  \target{B}  \ottsym{,}  \target{C}  \ottsym{,}  \target{f}  \ottsym{,}  \target{g}  \ottsym{\}} : \_ )

$A, B, C \vdash \lambda^3f.\lambda^4g.\lambda^5x.f\;x\;(g\;x)
\leadsto_d \cdots, \target{\flabel_3}(\{\target{A},\target{B},\target{C}\}, \target{f}:\_ \mapsto  \target{\flabel_ \ottsym{4} }   \ottsym{\{}  \target{A}  \ottsym{,}  \target{B}  \ottsym{,}  \target{C}  \ottsym{,}  \target{f}  \ottsym{\}} : \_ )

$A, B\vdash \lambda^2C.\lambda^3f.\lambda^4g.\lambda^5x.f\;x\;(g\;x)
\leadsto_d \cdots, \target{\flabel_2}(\{\target{A},\target{B}\}, \target{C}:\_ \mapsto  \target{\flabel_ \ottsym{3} }   \ottsym{\{}  \target{A}  \ottsym{,}  \target{B}  \ottsym{,}  \target{C}  \ottsym{\}} : \_ )

$A \vdash \lambda^1B.\lambda^2C.\lambda^3f.\lambda^4g.\lambda^5x.f\;x\;(g\;x)
\leadsto_d \cdots, \target{\flabel_1}(\{\target{A}\}, \target{B}:\_ \mapsto  \target{\flabel_ \ottsym{2} }   \ottsym{\{}  \target{A}  \ottsym{,}  \target{B}  \ottsym{\}} : \_ )

$\cdot \vdash \lambda^0A.\lambda^1B.\lambda^2C.\lambda^3f.\lambda^4g.\lambda^5x.f\;x\;(g\;x)
\leadsto_d \cdots, \target{\flabel_0}(\{\}, \target{A}:\_ \mapsto  \target{\flabel_ \ottsym{1} }   \ottsym{\{}  \target{A}  \ottsym{\}} : \_ )

§.§ Soundness

\begin{equation*}
Expressions \quad ::= \quad \cdots\ |\  \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} }
\end{equation*}

[s-ty]$\helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}  \helper{A}$Typing

[s-red]$\helper{M}  \mathrel{\triangleright}  \helper{N}$Reduction

[s-eq]$\vdash  \helper{M}  \equiv  \helper{N}$Equivalence

New syntax and rules in

We consider dependently typed defunctionalization correct if for all base types $A$, values $v$,
and programs $M$ of type $A$,

\begin{equation*}
\cdot   \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A} \land \ M\ \triangleright^* v\ \Longrightarrow\
\target{\fdef_{\Gamma}} \cup \target{\fdef_{M}} \vdash \target{M}\ \triangleright^* \target{v'} \text{ where } \target{v'} \equiv \target{v}.
\end{equation*}

In other words, if a closed program $M$ evaluates to a base-type value $v$, then $\target{M}$ evaluates to a base-type value $\target{v'}$ that is equivalent to $\target{v}$. This property follows as a corollary of the preservation of reduction sequences, which states that

\begin{align*}
M\ \triangleright^* N\ \Longrightarrow\
& \target{\fdef_{\Gamma}} \cup \target{\fdef_{M}} \cup \target{\fdef_{N}} \vdash
\target{M}\ \triangleright^* \target{M'},\\
&\text{ where } \target{\fdef_{\Gamma}} \cup \target{\fdef_{M}} \cup \target{\fdef_{N}} \vdash \target{M'} \equiv \target{N}.
\end{align*}

Ideally, we could show this property by showing that the
transformation preserves all small-step reductions $M\mathrel{\triangleright}N$, followed by an induction on the number of
reduction steps in a sequence. However, CC's meta-language
substitution $(\lam{x}{A}{M})\sub{N}{y}$ creates a new function
definition when it substitutes an expression into a free variable of a
function.  So, for a reduction sequence $M_1\ \triangleright \cdots \ \triangleright\ M_n$ in CC, some $M_i$ may contain function
definitions that do not exist in $M_1$ or $M_n$. Consequently, not
all $M_i$ translate into well-typed DCC expressions $\target{M_i}$ in $\sfpl \target{\fdef_{\Gamma}} \cup \target{\fdef_{M_1}} \cup \target{\fdef_{M_n}} \sfpr \semicolon \target{\Gamma}$, which makes
the standard approach infeasible. Moreover, preservation of reduction
sequences is a key lemma for showing type preservation, since CC's
typing rules involve equivalence and the equivalence rule (*eq-Reduce)
is defined with reductions.

Fortunately, meta-theoretic substitution is the only means of creating
new function definitions in CC's reduction sequences. There would be
no problem if the source language did not evaluate substitutions into
functions but kept them as primitive expressions. To apply
this observation we define a helper language , which is an
extension of CC with explicit
substitutions <cit.>. In addition,
does not reduce substitutions of expressions into functions.

Since  extends CC, every CC expression is trivially a  expression. We denote this trivial transformation from CC to  as $\sigma$. Then, we define the defunctionalization transformation from  to DCC in a similar way as that from CC to DCC – an expression transformation $\hbracket{-}$ and a meta-function $\hbracketd{-}$ for extracting definitions. Next, we show that $\sigma$ and defunctionalization for  preserve reduction sequences and they commute with the transformation from CC into DCC. As a corollary, defunctionalization from CC to DCC preserves reduction sequences. In other words, we show that the following diagram commutes for all CC-expressions $M$ and $N$ (contexts omitted).

M [d, "σ"] [dd, "-"', bend right, shift right=2] [rr, "▹^*"]                                                       N [d, "σ"'] [dd, "-", bend left, shift left=2]

M [r, "▹^*"] [d, "-"]                                               M' [r, "≡"] [d, "-"]     N [d, "-"']

M [r, "▹^*"]                                                                        M' [r, "≡"]                    N

\[
%DIF >  https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRBgH0BGEAX1PSZc+QigBM5KrUYs2nMXwEgM2PASJkuU+s1aIQAHQPYA5gFs6ACk5cAlIsGqRRLqS3Uds-UYAWMBmgwAE7AMLwOykJqosgS7tK6bEamFtYcYvb8jsLqKGRi2jJ6hgY4dEEmMDih3OFZkU65yK4FHkVJpeWV1WERKjkxEq0JXiVlFVU1YnVSMFCVCCigAGZBEGZIZCA4EEgSI8XJWOZ0INQMdABG-gAKUc76DDDLOBGr65vUO0gArG2J3gMl0uQToAGMANaTAC04XOV1u91yICCxx8r2o1zAUCQ0IAzFs4D4sC82Ap6u8Nogtt9EK4Dh0cKi6GATE9USZ0QA9ABUZxAF2uDDujVEAuerwpayp9NpABZ-qMjid+YLEaK2Bz0W9pUhZbtEAB2RWHIEg8FQ6qw1UI4VIsVPUmYmDYpAE6hEkmvRDQ6ZKSl7L4GvEmxnM1nstE4Xk2oUigZsR2S-26xD7Wl-BmAnzmyEwuEC23x6KJiU6j6IEPbA0KrMlGAARyYWBosfVCceZalFdrtONdd8uctwGt8Lj9s1UfLVMztIAbKHAUysCy2cEozGx+2S53Sd2qQvq0h+55TY3m62t3aNbvkytU1X51fiw9xU66wAPPgUXhAA
\DIFadd{\begin{tikzcd}
M \arrow[d, "\sigma"] \arrow[dd, "\bbracket{-}"', bend right, shift right=2] \arrow[rr, "\triangleright^*"] }&                                               & \DIFadd{N \arrow[d, "\sigma"'] \arrow[dd, "\bbracket{-}", bend left, shift left=2] }\\
\DIFadd{\helper{M} \arrow[r, "\triangleright^*"] \arrow[d, "\hbracket{-}"]                                           }& \DIFadd{\helper{M'} \arrow[r, "\equiv"] \arrow[d, "\hbracket{-}"] }& \DIFadd{\helper{N} \arrow[d, "\hbracket{-}"']                                       }\\
\DIFadd{\target{M} \arrow[r, "\triangleright^*"]                                                                    }& \DIFadd{\target{M'} \arrow[r, "\equiv"]                }& \DIFadd{\target{N}
\end{tikzcd}

{\ccs} is an extension of CC with new syntax, type derivation rules,
reduction rules, and equivalence rules (\DIFdelbegin \DIFdel{Figure~\ref{fig:ccs}}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{fig:ccs}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend ). We write
{\ccs} expressions in a $\helper{teal, mathematical}$ $\helper{font}$
to avoid ambiguity. {\ccs} extends the CC syntax with
\emph{syntactic substitutions} of the form
$ \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} } $.

% Type rules
Type rules for variables, universes, $\Pi$-types, functions, and
equivalence in {\ccs} are the same as the standard rules in CC, except
that the type of an application $ \helper{ \helper{M} } \ \helper{ \helper{N} } $ is
$ \helper{  \helper{B}  \{  \helper{x}  \mapsto  \helper{N}  \} } $ with the syntactic substitution.  The type of
a substitution $ \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} } $ is the type of
$\helper{M}$ with $\helper{x}$ substituted by $\helper{N}$

% Reductions and equivalence
{\ccs} has five reduction rules for
substitutions, which are the standard meta-theoretic substitution
rules for variables, universes, $\Pi$-types, and applications being
internalised into the language. Note that the meta-theoretic
substitution in the CC's original beta-reduction rule
$ \helper{  (   \helper{\lambda  \helper{x} } {:} \helper{ \helper{A} . \helper{M} }   )  } \ \helper{ \helper{N} }   \mathrel{\triangleright}   \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} } $
is also replaced by the syntactic one. {\ccs} does not reduce
substitutions into functions, but it $\beta$-reduces them when they
are applied to arguments (\rref*{s-red-Closure}).
We write
$\helper{M}\helper{\{x_1 \mapsto N_1, x_2 \mapsto N_2\}}$ for a
substitution followed by another substitution
$(\helper{M}\hsub{N_1}{x_1})\hsub{N_2}{x_2}$, and
$\helper{M}\hsub{\overline{N}}{\overline{y}}$ for a sequence of substitutions
$(((\helper{M}\hsub{N_1}{y_1})\hsub{N_2}{x_2}) \cdots

Like in CC, two terms in {\ccs} are equivalent if they $\beta$-reduce to
the same expression or are $\eta$-equivalent.
In addition, {\ccs} has two symmetric rules
(\rref*{s-eq-Closure1}) and (\rref*{s-eq-Closure2}) for determining when a
sequence of substitutions into a function
$ \helper{   (   \helper{\lambda  \helper{x} } {:} \helper{ \helper{A} . \helper{M} }   )   \{   \helper{\overline{ \helper{y} } }   \mapsto   \helper{\overline{ \helper{N} } }   \} } $
is equivalent to another expression. This is essentially a variant of
the $\eta$-equivalence rules that is compatible with substitutions --
$ \helper{   (   \helper{\lambda  \helper{x} } {:} \helper{ \helper{A} . \helper{M} }   )   \{   \helper{\overline{ \helper{y} } }   \mapsto   \helper{\overline{ \helper{N} } }   \} } $ is equivalent to
$\helper{N}$ if applying $\helper{N}$ to $\helper{x}$ is
equivalent to the function body $\helper{M}$ with $\helper{\overline{y}}$
being substituted for $\helper{\overline{N}}$.

Now, we define the defunctionalization transformation from {\ccs} to
DCC, which is the transformation from CC to DCC extended with the
following two rules. We use $\hbracket{-}$ and $\hbracketd{-}$ to stand
for the expression transformation and the metafunction for extracting
function definitions, and we apply the convention of tagging lambdas
with unique identifiers $i\ (i \in \mathbb{N})$ as usual.

\begin{drulepar}[s-t]{$\helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}  \helper{A}  \helper{\leadsto}  \target{M}$}{Expression transformation}
\drule{Subst}
\end{drulepar}

\begin{drulepar}[s-d]{$\helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}  \helper{A}  \helper{\leadsto_d}  \target{\fdef}$}{Function extraction}
\drule{Subst}
\end{drulepar}

The transformation turns a syntactic substitution in {\ccs} into a
meta-theoretic substitution in DCC (\rref*{s-t-Subst}); the function
definitions in a substitution $ \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} } $ are the
union of the definitions in $\helper{M}$ and $\helper{N}$
(\rref*{s-d-Subst}).  Since substitutions into functions do not reduce
in {\ccs}, the transformation from it into DCC have the following
strong properties by definition, which are not true for the
transformation from CC into DCC.
\begin{align}
\label{reduction def}
\helper{M}  \triangleright^*  \helper{N} \Longrightarrow\ \helper{\bbracket{N}_d} \subseteq\ \helper{\bbracket{M}_d}\\
\label{ccs substitution}
\hbracket{ \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} } } = \hbracket{\helper{M}}\sub{\hbracket{\helper{N}}}{\target{x}}.
\end{align}

Next, we show that the transformation preserves small step reductions
in {\ccs} -- if a {\ccs} program $\helper{M}$ reduces to
$\helper{N}$ in one step, then the translated program $\target{M}$
evaluates to $\target{N}$ in a sequence.

\begin{lemmarep}[Preservation of small step reductions]\label{lemma:ss-reduction-preservation}
If $\helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}  \helper{A}$ and $\helper{M}  \mathrel{\triangleright}  \helper{N}$, then
$\helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d} \vdash \target{M}\ \triangleright^* \target{N}$.
\end{lemmarep}
\begin{appendixproof}
By induction on the reduction rules of {\ccs}.

\begin{description}
\item[Case (\rref*{s-red-Beta}).] Assuming
$(\helper{\lambda^i x} \goodcolon \helper{A} . \helper{M})\ \helper{N}\ \triangleright\ \helper{M\hsub{N}{x}}$, the goal is to show that
\[
\target{\fdef}  \vdash    \target{\flabel_  i  }   \ottsym{\{}   \target{\overline{ \target{x} } }   \ottsym{\}} \,\target{ \mathop{@} }\, \target{N}   \triangleright^*  \target{M}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]},
\]
where $\target{\fdef} = \helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d}$
and $\target{\overline{x}}$ corresponds to the free variables in $\helper{\lambda^i}$.
By definition of $\hbracketd{-}$, we have \DIFdelbegin \DIFdel{$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\_}  \}\,,  \target{x}  \!:\!   \target{\_}   \, \rightarrow  \target{M}  :   \target{\_}  )  \, \in \, \target{\fdef}$
}\DIFdelend \DIFaddbegin \DIFadd{$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\_}  \}\,,  \target{x}  \!:\!   \target{\_}   \, \mapsto  \target{M}  :   \target{\_}  )  \, \in \, \target{\fdef}$
}\DIFaddend (ignoring type information).
So, $\target{\fdef}  \vdash    \target{\flabel_  i  }   \ottsym{\{}   \target{\overline{ \target{x} } }   \ottsym{\}} \,\target{ \mathop{@} }\, \target{N}   \mathrel{\triangleright}  \target{M}  \ottsym{[}   \target{\overline{ \target{x} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{,}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]} = \target{M}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$.
\item[Case (\rref*{s-red-Beta-Eta}).] Similar.
\end{description}

Other cases are trivial.

\end{appendixproof}

The transformation preserves sequences of reductions, and the proof follows from a trivial induction on the number of small steps in the sequence.

\begin{lemma}[Preservation of reduction sequences ({\ccs})]\label{lem:ccs prev sequence}
If $\helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}  \helper{A}$ and $\helper{M}  \triangleright^*  \helper{N}$,
then $\helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d} \vdash \target{M}\ \triangleright^* \target{N}$.
\end{lemma}

The transformation is also coherent, i.e.~it preserves the equivalence
relation in {\ccs}.

\begin{lemmarep}[Coherence ({\ccs})]
\label{lem:ccs coherence}
If $ \helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}  \helper{A} $, $ \helper{\Gamma}  \vdash  \helper{N}  \ottsym{:}  \helper{A} $, and $\vdash  \helper{M}  \equiv  \helper{N}$,
then $\target{\fdef}  \vdash  \target{M}  \equiv  \target{N}$, where
$\target{\fdef} = \helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d} \cup \helper{\bbracket{N}_d}$.
\end{lemmarep}
\begin{appendixproof}
By induction on the equivalence rules of {\ccs}.

\begin{description}
\item[Case (\rref*{s-eq-Reduce}).] By \Cref{lem:ccs prev sequence}.
\item[Case (\rref*{s-eq-Eta1}).] Assume that we have $\helper{\Gamma}  \vdash  \helper{M}  \ottsym{:}   \helper{\Pi  \helper{x} }{:}\helper{ \helper{A} .\, \helper{B} } $, $\helper{\Gamma}  \vdash  \helper{N}  \ottsym{:}   \helper{\Pi  \helper{x} }{:}\helper{ \helper{A} .\, \helper{B} } $, and $\vdash  \helper{M}  \equiv  \helper{N}$ by \rref{s-eq-Eta1},
then we must have $\helper{M}  \triangleright^*   \helper{\lambda^{  i  } }  \helper{x}  {:}  \helper{A} .\, \helper{M}' $, $\helper{N}  \triangleright^*  \helper{N}'$, and $\vdash  \helper{M}'  \equiv   \helper{ \helper{N}' } \ \helper{ \helper{x} } $.

By \Cref{lem:ccs prev sequence}, we have
$ \target{ \target{\fdef} _ \ottsym{1} }   \vdash  \target{M}  \triangleright^*   \target{\flabel_  i  }   \ottsym{\{}   \target{\overline{ \target{x} } }   \ottsym{\}}$,
$ \target{ \target{\fdef} _ \ottsym{2} }   \vdash  \target{N}  \triangleright^*  \target{N}'$,
where $\target{\fdef_1} = \helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d}$,
$\target{\fdef_2} = \helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{N}_d}$,
and \DIFdelbegin \DIFdel{$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\_}  \}\,,  \target{x}  \!:\!   \target{\_}   \, \rightarrow  \target{M}  :   \target{\_}  )  \, \in \,  \target{ \target{\fdef} _ \ottsym{1} } $}\DIFdelend \DIFaddbegin \DIFadd{$  \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\_}  \}\,,  \target{x}  \!:\!   \target{\_}   \, \mapsto  \target{M}  :   \target{\_}  )  \, \in \,  \target{ \target{\fdef} _ \ottsym{1} } $}\DIFaddend .
By the induction hypothesis, $ \target{ \target{\fdef} _ \ottsym{3} }   \vdash  \target{M}'  \triangleright^*   \target{N}' \,\target{ \mathop{@} }\, \target{x} $,
where $\target{\fdef_3} = \hbracketd{\helper{\Gamma}} \cup \helper{\bbracket{M'}_d} \cup \helper{\bbracket{N'}_d}$.

The goal is to show that $\target{\fdef}  \vdash  \target{M}  \equiv  \target{N}$ using \rref{d-eq-Eta1} (shown below).
\begin{center}
\drule{d-eq-EtaOne}
\end{center}

We already have all the premises like $\target{M}\ \triangleright^* \targetlab{\flabel_i}{\overline{x}}$, etc., but they are not judged in the desired label context $\target{\fdef} = \helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d} \cup \helper{\bbracket{N}_d}$. We only need to show that $\target{\fdef_1}$, $\target{\fdef_2}$, and $\target{\fdef_3}$ are subsets of $\target{\fdef}$ and to apply the weakening theorem. $\target{\fdef_1}$ and $\target{\fdef_2}$ are clearly subsets of $\target{\fdef}$. By \eqref{reduction def}, we have
$\hbracketd{\helper{M'}} \subseteq \hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{M}}$ and
$\hbracketd{\helper{N'}} \subseteq \hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{N}}$.
Therefore, $\target{\fdef_3}$ is also a subset of $\target{\fdef}$.
\item[Case (\rref*{s-eq-Clo1}).] Similar, but more tedious.
\item[Case (\rref*{s-eq-Eta2, s-eq-Clo2}).] By symmetry.
\end{description}

(Note that rules \rref*{s-eq-Reduce}, \rref*{s-eq-Eta1}, and \rref*{s-eq-Eta2} are not listed in \Cref{fig:ccs}, but they are exactly the same as \rref*{eq-Reduce}, \rref*{eq-Eta1}, and \rref*{eq-Eta2} in \Cref{fig:cc}).

\end{appendixproof}

Recall that $\sigma$ denotes the trivial transformation from CC to {\ccs}. This trivial transformation commutes with the two term transformations by definition.
\begin{equation}
\hbracket{\sigma(M)} = \bbracket{M}
\label{eq:commute}
\end{equation}
In addition, function definitions in $\hbracketd{\sigma(M)}$ is a subset of the definitions in $\bbracket{M}_d$, because new function definitions appear in CC's type derivation trees as results of substitutions, but this does not happen in {\ccs}.
\begin{equation}
\hbracketd{\sigma(M)} \subseteq \bbracket{M}_d
\label{eq:commute_d}
\end{equation}
We show that $\sigma$ also preserves sequences of reductions. As a convention, we write $\helper{M}$ for $\sigma(M)$ when there is no ambiguity.

\begin{lemmarep}[Preservation of reduction sequences ($\sigma$)]
\label{lem:sigma prev sequence}
If $\Gamma \vdash M\ \triangleright^* N$, then
$\helper{\Gamma} \vdash \helper{M}\ \triangleright^* \helper{M'} \text{ where } \helper{\Gamma} \vdash \helper{M'} \equiv \helper{N}$.
\end{lemmarep}
\begin{appendixproof}

We firstly proof that $\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{A}  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$ and $\Gamma  \vdash  \ottnt{N}  \ottsym{:}  \ottnt{A}$ implies that
$\vdash \sigma(M\sub{N}{x}) \equiv \helper{M\hsub{N}{x}}$. We prove this by induction on the type derivations of $M$.

\begin{description}
\item[Case (\rref*{ty-lambda}).] By definition, $  (  \lambda  \ottmv{y}  {:}  \ottnt{A} . \ottnt{M}  )  [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  =  \lambda  \ottmv{y}  {:}   \ottnt{A} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  .  \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  $.
So, $\sigma(  (  \lambda  \ottmv{y}  {:}  \ottnt{A} . \ottnt{M}  )  [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] ) = \helper{\lambda y :}\sigma( \ottnt{A} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] )\helper{.}\sigma( \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] )$.
We have
\[
\helper{  (   \helper{   (   \helper{\lambda  \helper{y} } {:} \helper{ \helper{B} . \helper{M} }   )   \{  \helper{x}  \mapsto  \helper{N}  \} }   )  } \ \helper{ \helper{y} }  \triangleright  \helper{   (   \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} }   )   \{  \helper{y}  \mapsto  \helper{y}  \} }
\equiv  \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} } .
\]
By the induction hypothesis, $ \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} }  \equiv \sigma( \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] )$. Hence, we have
$\sigma(  (  \lambda  \ottmv{y}  {:}  \ottnt{B} . \ottnt{M}  )  [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] ) \equiv  (   \helper{   (   \helper{\lambda  \helper{y} } {:} \helper{ \helper{B} . \helper{M} }   )   \{  \helper{x}  \mapsto  \helper{N}  \} }   )  $ by \rref{s-eq-Eta1}.
\end{description}

Other cases are trivial. Using this result, we have
$ \helper{  (   \helper{\lambda  \helper{x} } {:} \helper{ \helper{A} . \helper{M} }   )  } \ \helper{ \helper{N} }   \mathrel{\triangleright}   \helper{  \helper{M}  \{  \helper{x}  \mapsto  \helper{N}  \} }  \equiv \sigma( \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] )$,
so, $\sigma$ preserves small step reductions. Again, the preservation of reduction sequences follows immediately from this.
\end{appendixproof}

We can finally prove the preservation of reduction sequences for
dependently typed defunctionalization (from CC to DCC) using the
lemmas above.

\begin{lemmarep}[Preservation of reduction sequences]
\label{lem:prev sequence}
For all $M$ and $N$, if $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$ and $\ottnt{M}  \triangleright^*  \ottnt{N}$, then we have
\begin{align}
&    \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }    \vdash  \target{M}  \triangleright^*  \target{M}',\\
&    \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }    \vdash  \target{M}'  \triangleright^*  \target{N}
\end{align}
for some $\target{M}'$ where
$(   \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }  )$ =
$( \bbracket{ \Gamma }_d ,  \bbracket{ \ottnt{M} }_d ,  \bbracket{ \ottnt{N} }_d )$ and
$(\target{M}, \target{N})$ = $( \bbracket{ \ottnt{M} } ,  \bbracket{ \ottnt{N} } )$
\end{lemmarep}
\begin{appendixproof}
Suppose that $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$ and $\ottnt{M}  \triangleright^*  \ottnt{N}$. Then, we have
$\vdash \helper{M}\ \triangleright^* \helper{M'} \text{ and } \vdash \helper{M'} \equiv \helper{N}$ for some $\helper{M'}$, since $\sigma$ preserves reduction sequences. By \Cref{lem:ccs prev sequence} and \Cref{lem:ccs coherence},
\begin{align*}
\hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{M}} &\vdash
\target{M} \triangleright^* \target{M'}\\
\hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{M}} \cup \hbracketd{\helper{N}} &\vdash \target{M'} \equiv \target{N}.
\end{align*}
Finally, since $(\hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{M}})$ and $(\hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{M}} \cup \hbracketd{\helper{N}})$ are both subsets of $(   \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }  )$, we have
$   \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }    \vdash  \target{M}  \triangleright^*  \target{M}'$ and
$   \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }    \vdash  \target{M}'  \triangleright^*  \target{N}$
by weakening.
\end{appendixproof}

Since ground types and values do not contain functions,
$\bbracket{v}_d = \target{\cdot}$, and the correctness of the
transformation is just a special case of \DIFdelbegin \DIFdel{Lemma~\ref{lem:prev
sequence}}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{lem:prev
}\DIFaddend .

\begin{cororep}(Correctness)\label{coro:correctness}
For all ground types $A$ and values $v$ of type $A$,
\begin{equation*}
\cdot   \vdash  \DIFdelbegin \DIFdel{M \goodcolon A \ }\DIFdelend \DIFaddbegin \ottnt{M}  \ottsym{:}  \ottnt{A} \DIFaddend \land \DIFdelbegin \DIFdel{\
M\ }\DIFdelend \DIFaddbegin \ottnt{M}  \DIFaddend \triangleright^*  \DIFdelbegin \DIFdel{v\ }\DIFdelend \DIFaddbegin \ottmv{v}
\DIFaddend \Longrightarrow
\DIFdelbegin \DIFdel{\
}%DIFDELCMD < \target{\fdef_{\Gamma}} %%%
\DIFdelend \DIFaddbegin \target{ \target{\fdef} _ \Gamma }   \DIFaddend \cup   \DIFdelbegin %DIFDELCMD < \target{\fdef_{M'}} %%%
\DIFdelend \DIFaddbegin \target{ \target{\fdef} _ \ottnt{M} }    \DIFaddend \vdash  \DIFdelbegin %DIFDELCMD < \target{M'}%%%
\DIFdel{\ }\DIFdelend \DIFaddbegin \target{M}  \DIFaddend \triangleright^*  \DIFdelbegin %DIFDELCMD < \target{v'} %%%
\DIFdelend \DIFaddbegin \target{v}\DIFadd{'
}\DIFaddend \text{ where } \DIFdelbegin %DIFDELCMD < \target{v'} %%%
\DIFdelend \DIFaddbegin \target{v}\DIFadd{' }\DIFaddend \equiv \target{v}.
\end{equation*}
\end{cororep}

The proof of type-preservation requires three lemmas:
\emph{substitution}, \emph{preservation of reduction sequences}, and
\emph{coherence}. \Cref{lem:prev sequence} established that
dependently-typed defunctionalization preserves reduction sequences
with the help of {\ccs}, and now we prove the remaining two lemmas in
a similar way. The substitution lemma states that defunctionalization
is compatible with substitutions.

\begin{lemmarep}[Substitution]
\label{lem:sub}
If $\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{A}  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$ and $\Gamma  \vdash  \ottnt{N}  \ottsym{:}  \ottnt{A}$, then $\target{\fdef}  \vdash   \bbracket{  \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  }   \equiv  \target{M}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$,
where $\target{\fdef} =     \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }    \cup   \target{ \target{\fdef} _  \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  }  $.
\end{lemmarep}
\begin{appendixproof}
From the proof of \Cref{lem:sigma prev sequence}, we know that
$\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{A}  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$ and $\Gamma  \vdash  \ottnt{N}  \ottsym{:}  \ottnt{A}$ implies that
$\sigma(M\sub{N}{x}) \equiv \helper{M\hsub{N}{x}}$.
This further implies that $\target{\fdef'} \vdash \hbracket{\sigma(M\sub{N}{x})} \equiv \hbracket{\helper{M\hsub{N}{x}}}$, where
$\target{\fdef'} = \hbracketd{\helper{\Gamma}} \cup \hbracketd{\helper{M}} \cup \hbracketd{\helper{N}} \cup \hbracketd{\sigma(M\sub{N}{x})}$.

By (\DIFdelbegin \DIFdel{\ref{eq:commute_d}}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{eq:commute_d}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend ), $\target{\fdef'} \subseteq \target{\fdef}$. Also, $\hbracket{\sigma(M\sub{N}{x})} = \bbracket{M\sub{N}{x}}$, $\hbracket{\helper{\Gamma}} = \target{\Gamma}$, and $\hbracket{\helper{M}}\sub{\hbracket{\helper{N}}}{\target{x}} = \target{M}\targetsub{N}{x}$ by \eqref{ccs substitution} and \eqref{eq:commute}.
Therefore, we have $\target{\fdef}  \vdash   \bbracket{  \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  }   \equiv  \target{M}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$ by weakening.
\end{appendixproof}

The coherence lemma states that defunctionalization is compatible with CC's coherence judgements.

\begin{lemmarep}[Coherence]
\label{lem:coherence}
If $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$, $\Gamma  \vdash  \ottnt{N}  \ottsym{:}  \ottnt{A}$, and $\vdash  \ottnt{M}  \equiv  \ottnt{N}$, then $\target{\fdef}  \vdash  \target{M}  \equiv  \target{N}$,
where $\target{\fdef} =    \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }  $.
\end{lemmarep}
\begin{appendixproof}
Assume that $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$, $\Gamma  \vdash  \ottnt{N}  \ottsym{:}  \ottnt{A}$, and $\vdash  \ottnt{M}  \equiv  \ottnt{N}$.
We have $\vdash \helper{M} \equiv \helper{N}$ by definition,
since the source language does not contain explicit substitution.
By \Cref{lem:ccs coherence}, we have $\target{\fdef}'  \vdash  \target{M}  \equiv  \target{N}$, where
$\target{\fdef'} = \helper{\bbracket{\Gamma}_d} \cup \helper{\bbracket{M}_d} \cup \helper{\bbracket{N}_d}$.
Since $\target{\fdef'} \subseteq \target{\fdef}$, we have $\target{\fdef}  \vdash  \target{M}  \equiv  \target{N}$ by weakening.
\end{appendixproof}

Finally, we show type preservation with an induction on CC's type derivation rules.

\begin{theoremrep}[Type preservation]
\label{theorem:type preservation}
For all well-typed programs $\ottnt{M}$,
\begin{equation*}
\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A} \Longrightarrow   \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A},
\end{equation*}
where $( \target{ \target{\fdef} _ \Gamma } ,  \target{ \target{\fdef} _ \ottnt{M} } ) = ( \bbracket{ \Gamma }_d ,  \bbracket{ \ottnt{M} }_d )$ and
$(\target{\Gamma}, \target{M}, \target{A}) = (\bbracket{\Gamma},  \bbracket{ \ottnt{M} } ,  \bbracket{ \ottnt{A} } )$.
\end{theoremrep}
\begin{appendixproof}
By proving the following two statements together with a simultaneous induction on mutually-defined judgements
$\vdash  \Gamma$ and $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$.
\begin{enumerate}
\item $\vdash  \Gamma \Longrightarrow\ \vdash   \target{ \target{\fdef} _ \Gamma }   \ottsym{;}  \target{\Gamma}$.
\item $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A} \Longrightarrow   \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$.
\end{enumerate}
Statement $1$ follows trivially from the inductive hypothesis. We look at the cases for statement $2$.
\begin{description}
\item[Case (\rref*{ty-Var, ty-Universe, ty-Pi}).] Trivial by the induction hypothesis.

\item[Case (\rref*{ty-Apply})] Suppose $\Gamma  \vdash   \ottnt{M} \; \ottnt{N}   \ottsym{:}   \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] $. The goal is to show that
$\targetcon \vdash \targetapp{M}{N} \goodcolon \bbracket{B\sub{N}{x}}$, where
$\target{\fdef} = \sfpl \target{\fdef_{\Gamma}} \cup \bbracket{M\ N}_d \sfpr$.
We have
$  \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}   \targetpi{ \target{x} }{ \target{A} }{ \target{B} } $ and
$  \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{N} }    \ottsym{;}  \target{\Gamma}  \vdash  \target{N}  \ottsym{:}  \target{A}$ by the induction hypothesis.
By \rref{d-ty-Apply} and weakening,
$ \target{ \target{\fdef} _ \Gamma }   \ottsym{;}  \target{\Gamma}  \vdash   \target{M} \,\target{ \mathop{@} }\, \target{N}   \ottsym{:}  \target{B}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$.
By the substitution lemma,
$\target{\fdef}'  \vdash  \target{B}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}  \equiv   \bbracket{  \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  } $,
where $\target{\fdef}' =     \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{B} }    \cup   \target{ \target{\fdef} _ \ottnt{N} }    \cup   \target{ \target{\fdef} _  \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  }  $.
We have the goal if $ \target{\fdef}'  \subseteq  \target{\fdef} $.
\begin{enumerate}
\item $  \target{ \target{\fdef} _ \Gamma }   \subseteq  \target{\fdef} $ by def.
\item $  \target{ \target{\fdef} _ \ottnt{N} }   \subseteq  \target{\fdef} $ since $  \target{ \target{\fdef} _ \ottnt{N} }   \subseteq   \bbracket{  \ottnt{M} \; \ottnt{N}  }_d  $ by def.
\item $  \target{ \target{\fdef} _  \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  }   \subseteq  \target{\fdef} $ since $  \target{ \target{\fdef} _  \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ]  }   \subseteq   \bbracket{  \ottnt{M} \; \ottnt{N}  }_d  $ by def.
\item $  \target{ \target{\fdef} _ \ottnt{B} }   \subseteq  \target{\fdef} $, because $  \target{ \target{\fdef} _ \ottnt{N} }   \subseteq   \bbracket{  \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B}  }_d  $ by def.,
$  \bbracket{  \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B}  }_d   \subseteq   \target{ \target{\fdef} _ \ottnt{M} }  $ by $\Gamma  \vdash  \ottnt{M}  \ottsym{:}   \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $ and \Cref{lemma:type-label-subset},
and $  \target{ \target{\fdef} _ \ottnt{M} }   \subseteq  \target{\fdef} $ by def.
\end{enumerate}

\item[Case (\rref*{ty-Lambda})] Suppose $\Gamma  \vdash   \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}   \ottsym{:}   \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $.
The goal is $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash   \target{\flabel_  i  }   \ottsym{\{}   \target{\overline{ \target{x} } }   \ottsym{\}}  \ottsym{:}   \targetpi{ \target{x} }{ \target{A} }{ \target{B} } $, where
\DIFdelbegin \DIFdel{$\target{\fdef} =    \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }     \ottsym{,}     \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} )  $}\DIFdelend \DIFaddbegin \DIFadd{$\target{\fdef} =    \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }     \ottsym{,}     \target{\flabel_  i  }  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} )  $}\DIFaddend .
We have $\Gamma  \vdash   \overline{ \ottmv{x} }   \ottsym{:}   \overline{ \ottnt{A} } $ since $\overline{x}$ are well-typed free variables, therefore,
we have $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash   \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } } $ by the inductive hypothesis and weakening.
The definition of $ \target{\flabel_  i  } $ is in $\target{\fdef}$.

If $\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma}$, then we have our goal by \rref{d-ty-Label}.
We have $\vdash    \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \ottsym{;}  \target{\Gamma}$ by the induction hypothesis and our assumption that
$\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{A}  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$.
Letting $ \target{\Gamma_{fv} }  =  \target{\cdot}   \ottsym{,}   \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } } $, if the following statements are true,
then we have $\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma}$ by \rref{d-wf-Label} and weakening.

\begin{enumerate}
\item[(a)] $  \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \ottsym{;}   \target{\Gamma_{fv} }   \vdash   \targetpi{ \target{x} }{ \target{A} }{ \target{B} }   \ottsym{:}  \target{U} $.
\item[(b)] $  \target{ \target{\fdef} _ \Gamma }   \cup   \target{ \target{\fdef} _ \ottnt{M} }    \ottsym{;}   \target{\Gamma_{fv} }   \ottsym{,}  \target{x}  \ottsym{:}  \target{A}  \vdash  \target{M}  \ottsym{:}  \target{B} $.
\end{enumerate}

By \Cref{lem:fv}, $ FV(  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  )   \vdash   \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}   \ottsym{:}   \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $,
so, $ FV(  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  )   \vdash   \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B}   \ottsym{:}  \ottnt{U}$, and
$ FV(  \lambda^{  i  } x {:}  \ottnt{A} . \ottnt{M}  )   \ottsym{,}  \ottmv{x}  \ottsym{:}  \ottnt{A}  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{B}$.
Therefore, conditions (a) and (b) are true by the induction hypothesis and weakening.

\item[Case (\rref*{ty-Equiv}).] By the coherence lemma.
\end{description}

\end{appendixproof}

\subsection{\DIFdelbegin \DIFdel{The Backwards Translation}\DIFdelend \DIFaddbegin \DIFadd{Consistency and Type Safety of DCC}\DIFaddend }
\DIFdelbegin %DIFDELCMD < \label{section:backwards}
%DIFDELCMD < %%%
\DIFdelend \DIFaddbegin \label{section:consistency}
\DIFaddend

\begin{figure}[ht]

\begin{drulepar}[b]{$\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}  \leadsto_b  \ottnt{M}$}{Backward transformation}
\drule{Var}

\drule{Universe}

\drule{Pi}

\drule{Label}

\drule{Apply}

\drule{Equiv}
\end{drulepar}

\caption{Backward transformation}
\label{fig:backward transformation}
\end{figure}

As a dependent type theory, DCC should be type-safe when it acts as a
programming language and consistent when interpreted as a logic.
Following \citet{DBLP:conf/cpp/BoulierPT17} and \citet{DBLP:conf/pldi/BowmanA18},
we prove these properties in this section by defining a
\emph{backward transformation} from DCC to CC and showing that it
preserves reduction sequences, so that reducing an expression in DCC is
equivalent to reducing an expression in CC.
The transformation is type-preserving and turns the logical
interpretation of \emph{false} in DCC into that of CC, so that valid
proofs (i.e.~well-typed programs) in DCC correspond to valid proofs in CC.
This reduces the problem of proving the type safety and consistency of
DCC to proving that of CC, which is a standard result~\cite{DBLP:journals/iandc/CoquandH88}.
In other words, we show that DCC can be modelled by CC in a consistent
and meaning-preserving way.
Type preservation for the backward transformation also requires the
\emph{substitution}, \emph{preservation of reduction sequences},
and \emph{coherence} lemmas, similar to the proof of
\Cref{theorem:type preservation}, whose proofs are

We define the backward transformation $\bluebr{-}$ with a new
judgement (\Cref{fig:backward transformation}) of the form
$\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}  \leadsto_b  \ottnt{M}$ and
$\bluebr{\target{M}} \triangleq M$.
The translation maps variables, universes, $\Pi$-types, and
applications back to their corresponding forms in CC,
and maps label expressions \DIFdelbegin \DIFdel{$ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{x} } }   \ottsym{\}}$ where
$  \target{\flabel}  (\{ \target{\Gamma} \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} )  \, \in \, \target{\fdef}$,
}\DIFdelend \DIFaddbegin \DIFadd{$ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$ where
$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} )  \, \in \, \target{\fdef}$
}\DIFaddend into
$ \lambda  \ottmv{x}  {:}   \ottnt{A} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  $ --- a
function with all of its free-variable values substituted in, where
$A$, $M$, and $\overline{M}$ stand for $\bluebr{\target{A}}$,
$\bluebr{\target{M}}$, and $\bluebr{\target{\overline{M}}}$ respectively
Intuitively, $\bluebr{-}$ decompiles a label back to the function it
The backward transformation also acts pointwise on type contexts.

In CC, the interpretation of the logical \emph{false} is $ \Pi  \ottmv{x}  {:}   U_{  \ottsym{0}  }  . \ottmv{x} $. There is no closed expression with the \emph{false} type. In DCC, the interpretation of \emph{false} is $\targetpi{\target{x}}{\target{U_0}}{\target{x}}$, so the backward transformation preserves falseness by definition.

Next, we show that the backward transformation is compatible with
As a convention in this section, we write $M$ for
$\bluebr{\target{M}}$ when there is no ambiguity.

\begin{lemmarep}[Backward transformation compatible with substitutions]\label{lemma:back-trans-compat}
If $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \ottsym{,}  \target{x}  \ottsym{:}  \target{A}  \vdash  \target{M}  \ottsym{:}  \target{B}$ and $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{N}  \ottsym{:}  \target{A}$,
then $\bluebr{\target{M}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}} =  \ottnt{M} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] $.
\end{lemmarep}
\begin{appendixproof}
By induction on the type derivation of $\target{M}$.
\begin{description}
\item[Case (\rref*{d-ty-Label}).] Assume that $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \ottsym{,}  \target{y}  \ottsym{:}  \target{C}  \vdash   \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}  \ottsym{:}   \targetpi{ \target{x} }{ \target{A} }{ \target{B} } $,
\DIFdelbegin \DIFdel{$  \target{\flabel}  (\{ \target{\Gamma} \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} )  \, \in \, \target{\fdef}$}\DIFdelend \DIFaddbegin \DIFadd{$  \target{\flabel}  (\{ \target{\Gamma} \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} )  \, \in \, \target{\fdef}$}\DIFaddend , and $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{N}  \ottsym{:}  \target{C}$.
The goal is to show that $\bluebr{  \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}   \ottsym{[}  \target{N}  \ottsym{/}  \target{y}  \ottsym{]}} =   (  \lambda  \ottmv{x}  {:}   \ottnt{A} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]   )  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ] $.
Indeed, we have
\[
\bluebr{  \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}   \ottsym{[}  \target{N}  \ottsym{/}  \target{y}  \ottsym{]}} = \bluebr{ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{[}  \target{N}  \ottsym{/}  \target{y}  \ottsym{]}  \ottsym{\}}}
=  \lambda  \ottmv{x}  {:}   \ottnt{A} [   (   \overline{ \ottnt{M} }  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  )   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   (   \overline{ \ottnt{M} }  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  )   \ottsym{/}   \overline{ \ottmv{x} }   ]
\]
by the induction hypothesis, and
\begin{align*}
(  \lambda  \ottmv{x}  {:}   \ottnt{A} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]   )  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  &=
\lambda  \ottmv{x}  {:}   (   (  \ottnt{A} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  )  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  )  .  (   (  \ottnt{M} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  )  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  )  \\
&=  \lambda  \ottmv{x}  {:}   \ottnt{A} [   (   \overline{ \ottnt{M} }  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  )   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   (   \overline{ \ottnt{M} }  [  \ottnt{N}  \ottsym{/}  \ottmv{y}  ]  )   \ottsym{/}   \overline{ \ottmv{x} }   ]
\end{align*}
since $y$ is not free in $A$ and in $M$ ($\overline{x}$ are all the free variables in them).
\end{description}

Ohter cases are either trivial or follows directly from the induction hypothesis.

\end{appendixproof}

%DIF >  YH: We can move these lemmas to appendix, if we are short of space.
Similar to proofs in Section \Cref{section:soundness}, we show preservation of reduction sequences by showing that the transformation preserves small-step reductions.
Using that, we show the coherence lemma for the backward transformation,
and then the type preservation.
\begin{lemmarep} If $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$ and $\target{\fdef}  \vdash  \target{M}  \triangleright^*  \target{N}$, then $\ottnt{M}  \triangleright^*  \ottnt{N}$.
\DIFdelbegin %DIFDELCMD < \label{lem:back prev sequence}
%DIFDELCMD < %%%
\DIFdelend \DIFaddbegin \label{lem:back-prev-sequence}
\DIFaddend \end{lemmarep}
\begin{appendixproof}
We firstly show by induction that the backward transformation preserves small-step reductions. The only case is \rref{d-red-Beta}.

\begin{description}
\item[Case (\rref*{d-red-Beta}).] Assume that $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash    \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}} \,\target{ \mathop{@} }\, \target{M}'   \ottsym{:}  \target{B}$,
\DIFdelbegin \DIFdel{$  \target{\flabel}  (\{ \target{\Gamma} \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{N}  :  \target{B} )  \, \in \, \target{\fdef}$}\DIFdelend \DIFaddbegin \DIFadd{$  \target{\flabel}  (\{ \target{\Gamma} \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{N}  :  \target{B} )  \, \in \, \target{\fdef}$}\DIFaddend , and $\target{\fdef}  \vdash    \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}} \,\target{ \mathop{@} }\, \target{N}   \triangleright^*  \target{N}  \ottsym{[}   \target{\overline{ \target{M} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{,}  \target{M}'  \ottsym{/}  \target{x}  \ottsym{]}$.
We have $\bluebr{  \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}} \,\target{ \mathop{@} }\, \target{M}' } =  \lambda  \ottmv{x}  {:}   \ottnt{A} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  $ by definition. Indeed, we have
\begin{align*}
(  \lambda  \ottmv{x}  {:}   \ottnt{A} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{M} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]   )  \; \ottnt{M'}  &\triangleright\
(  \ottnt{N} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  )  [  \ottnt{M'}  \ottsym{/}  \ottmv{x}  ] \\
&=  \ottnt{N} [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   \ottsym{,}  \ottnt{M'}  \ottsym{/}  \ottmv{x}  ]  \text{ since $x$ is not free in $\overline{M}$}\\
&= \bluebr{\target{N}  \ottsym{[}   \target{\overline{ \target{M} } }   \ottsym{/}   \target{\overline{ \target{x} } }   \ottsym{,}  \target{M}'  \ottsym{/}  \target{x}  \ottsym{]}} \text{ by \Cref{lemma:back-trans-compat}.}
\end{align*}
\end{description}

Therefore, the backward transformation preserves reduction sequences by a trivial induction on the number of small steps in a reduction sequence.

\end{appendixproof}

\begin{lemmarep}If $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$, $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{N}  \ottsym{:}  \target{A}$, and $\target{\fdef}  \vdash  \target{M}  \equiv  \target{N}$,
then $\vdash  \ottnt{M}  \equiv  \ottnt{N}$.
\label{lemma:back-trans-coherence}
\end{lemmarep}
\begin{appendixproof}
By induction on DCC's equivalence rules.
\begin{description}
\item[Case (\rref*{d-eq-Reduce}).] By \DIFdelbegin \DIFdel{\mbox{%DIFAUXCMD
\Cref{lem:back prev sequence}}\hspace{0pt}%DIFAUXCMD
}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{lem:back-prev-sequence}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend .
\item[Case (\rref*{d-eq-Eta1}).] Assume that we have
\[
\drule{d-eq-EtaOne}.
\]
Our goal is to show that $\vdash  \ottnt{L}  \equiv  \ottnt{M}$.
By \DIFdelbegin \DIFdel{\mbox{%DIFAUXCMD
\Cref{lem:back prev sequence}}\hspace{0pt}%DIFAUXCMD
}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{lem:back-prev-sequence}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend ,
$\ottnt{L}  \triangleright^*   (  \lambda  \ottmv{x}  {:}   \ottnt{A} [   \overline{ \ottnt{N} }   \ottsym{/}   \overline{ \ottmv{x} }   ]  .  \ottnt{N} [   \overline{ \ottnt{N} }   \ottsym{/}   \overline{ \ottmv{x} }   ]   ) $ and $\ottnt{M}  \triangleright^*  \ottnt{M'}$.
By the induction hypothesis and \Cref{lemma:back-trans-compat},
$\vdash   \ottnt{N'} [   \overline{ \ottnt{N} }   \ottsym{/}   \overline{ \ottmv{x} }   ]   \equiv   \ottnt{M'} \; \ottmv{x} $.
Therefore, $\vdash  \ottnt{L}  \equiv  \ottnt{M}$ by CC's \rref{eq-Eta1}.
\item[Case (\rref*{d-eq-Eta2}).] By symmetry.
\end{description}

\end{appendixproof}

\begin{lemmarep} If $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$, then $\Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$.
\label{lemma:back-type-preservation}
\end{lemmarep}
\begin{appendixproof}
By proving the following two statements together with a simultaneous induction on mutually-defined judgements
$\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma}$ and $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A}$.
\begin{enumerate}
\item $\vdash  \target{\fdef}  \ottsym{;}  \target{\Gamma} \Longrightarrow\ \vdash  \Gamma$.
\item $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash  \target{M}  \ottsym{:}  \target{A} \Longrightarrow\ \Gamma  \vdash  \ottnt{M}  \ottsym{:}  \ottnt{A}$.
\end{enumerate}
Statement $1$ follows trivially from the inductive hypothesis. We look at the cases for statement $2$.
\begin{description}
\item [Case (\rref*{d-ty-Var, d-ty-Universe, d-ty-Pi}).] Trivial by induction.
\item [Case (\rref*{d-ty-Apply}).] Assume that $\target{\fdef}  \ottsym{;}  \target{\Gamma}  \vdash   \target{M} \,\target{ \mathop{@} }\, \target{N}   \ottsym{:}  \target{B}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}$, the goal is to show that
$\Gamma \vdash M N : \bluebr{\target{B}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}}$. By the induction hypothesis, we have $\Gamma  \vdash  \ottnt{M}  \ottsym{:}   \Pi  \ottmv{x}  {:}  \ottnt{A} . \ottnt{B} $
and $\Gamma  \vdash  \ottnt{N}  \ottsym{:}  \ottnt{A}$, which implies that $\Gamma  \vdash   \ottnt{M} \; \ottnt{N}   \ottsym{:}   \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] $. By \Cref{lemma:back-trans-compat},
$\bluebr{\target{B}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}} \equiv  \ottnt{B} [  \ottnt{N}  \ottsym{/}  \ottmv{x}  ] $. Therefore, we have $\Gamma \vdash M N : \bluebr{\target{B}  \ottsym{[}  \target{N}  \ottsym{/}  \target{x}  \ottsym{]}}$
by \rref{Equiv}.
\item [Case (\rref*{d-ty-Label}).] Similar.
\item [Case (\rref*{d-ty-Equiv}).] By \Cref{lemma:back-trans-coherence}
\end{description}

\end{appendixproof}

As a corollary \DIFaddbegin \DIFadd{of \mbox{%DIFAUXCMD
\Cref{lem:back-prev-sequence} }\hspace{0pt}%DIFAUXCMD
and \mbox{%DIFAUXCMD
\Cref{lemma:back-type-preservation}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend ,
DCC is type-safe and consistent since CC is.

\DIFaddbegin \begin{theoremrep}[Type safety] \DIFadd{If $\target{\fdef}  \ottsym{;}   \target{\cdot}   \vdash  \target{M}  \ottsym{:}  \target{A}$, then $\target{\fdef}  \vdash  \target{M}  \triangleright^*  \target{v}$
for some irreducible value $\target{v}$.
\end{theoremrep}

\DIFadd{That is, type safety guarantees that every well-typed closed DCC term reduces
to a value in a finite number of steps.

\begin{theoremrep}[Consistency] \DIFadd{There is no pair of a label context $\target{\fdef}$ and DCC term $\target{M}$ such that $\target{\fdef}  \ottsym{;}   \target{\cdot}   \vdash  \target{M}  \ottsym{:}    \targetpi{ \target{A} }{ \target{U} }{ \target{A} }  $.
\end{theoremrep}

\DIFadd{Interpreting DCC as a logic, the term $ \targetpi{ \target{A} }{ \target{U} }{ \target{A} } $ (which
produces a term of any type $\target{A}$) corresponds to }\emph{\DIFadd{false}}\DIFadd{; it
is backward-transformed to $\Pi A {:} U . A$, the representation of
}\emph{\DIFadd{false}} \DIFadd{in CC.  Consistency of DCC means that there is no closed
term of type $ \targetpi{ \target{A} }{ \target{U} }{ \target{A} } $; if there were, then translation
would yield a corresponding term in CC, and CC would also be

\DIFaddend \section{Implementation}
\label{section:implementation}

\DIFdelbegin \DIFdel{In supplementary material we }\DIFdelend \DIFaddbegin \DIFadd{We }\DIFaddend provide a portable standalone implementation of the
defunctionalization translation of
\Cref{section:cc-defunctionalization}, written in OCaml and compiled
to run in a web browser using
\verb!js_of_ocaml!~\cite{DBLP:journals/spe/VouillonB14}.
The implementation performs
type checking of CC (\Cref{section:cc})
and DCC (\Cref{section:dcc}) terms,
abstract defunctionalization (\Cref{section:translation}) and
backwards translation from DCC to CC (\DIFdelbegin \DIFdel{\mbox{%DIFAUXCMD
\Cref{section:backwards}}\hspace{0pt}%DIFAUXCMD
}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{section:consistency}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend ),
allowing the interested reader to experiment with the effects of the translation on real examples.
We include several ready-made examples, including dependent
composition, dependent pairs and finite sets.

\section{Related Work}
\label{section:related}

\paragraph{Type-preserving compilation}

Type-preserving compilation was initially developed for optimizing
compilation and verifying the compiled code; it has been used
extensively in compilers of simply-typed and \DIFdelbegin \DIFdel{polymorpihc }\DIFdelend \DIFaddbegin \DIFadd{polymorphic }\DIFaddend languages,
and occasionally for \DIFdelbegin \DIFdel{ependently-typed }\DIFdelend \DIFaddbegin \DIFadd{dependently-typed }\DIFaddend languages.
For example, \citet{DBLP:conf/pldi/TarditiMCSHL96} present TIL (typed
intermediate language), an ML compiler featuring type-directed code
optimization of loops, garbage collections, and polymorphic function
calls, and \citet{DBLP:journals/toplas/MorrisettWCG99} study a
type-preserving translation from System F to the typed assembly
language TAL.
\citet{DBLP:conf/icfp/XiH01} later extended TAL to DTAL, an assembly
language with a limited form of dependent types that serves as a
compilation target for Dependent ML.

\citet{DBLP:conf/icfp/GuillemetteM08} also present a type-preserving
compiler from System F, but take a different approach, building typed
intermediate representations using generalized algebraic data types
and using the type system of the host language (GHC Haskell) to verify
that each compiler phase preserves types.
Embedding typed transformations in this way is a popular technique in
the functional programming community, exemplified in work by
\citet{DBLP:journals/jfp/CaretteKS09}, which presents type-preserving
CPS transformations of an embedded language along with type-preserving optimizations
based on partial evaluation.

\citet{DBLP:conf/popl/Necula97}'s proof-carrying code is another early
method for generating reliable executables. It relies on an external
logical framework to check the correctness of proofs attached with the

Bowman and collaborators have developed several type-preserving
translations for dependently-typed languages, including
\DIFdelbegin \DIFdel{a
type-preserving }\DIFdelend CPS
\DIFdelbegin \DIFdel{a
type-preserving }\DIFdelend closure
conversion~\DIFdelbegin \DIFdel{\mbox{%DIFAUXCMD
\cite{DBLP:journals/pacmpl/BowmanCRA18,DBLP:conf/pldi/BowmanA18}}\hspace{0pt}%DIFAUXCMD
}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\cite{DBLP:conf/pldi/BowmanA18}
}\DIFaddend (building on \DIFdelbegin \DIFdel{a }\DIFdelend typed closure conversion for System F
by~\citet{DBLP:conf/popl/MinamideMH96}), and
\DIFdelbegin \DIFdel{a type preserving
}\DIFdelend translation to ANF~\cite{koronkevich_rakow_ahmed_bowman_2022}.

\paragraph{Defunctionalization}

Defunctionalization was first presented by
\citet{DBLP:conf/acm/Reynolds72} as a programming technique to
translate a higher-order interpreter into a first-order
It has been used in a variety of applications,
from ML
to type-safe garbage collectors~\cite{DBLP:conf/popl/WangA01}, and
encodings of higher-kinded

Defunctionalization was originally presented as an untyped
Using a family
of monomorphic \emph{apply} functions to make simply-typed defunctionalization type-preserving is
a standard workaround  in the

\citet{DBLP:conf/ppdp/DanvyN01} survey more examples of
defunctionalization in practice.

Formalization of defunctionalization has up to this point focused on
proving type preservation and correctness of the transformation.
\citet{DBLP:conf/icfp/BellBH97}~have shown that the translation for
simply typed programs is type preserving.
\citet{nielsen2000denotational} \DIFdelbegin \DIFdel{have }\DIFdelend \DIFaddbegin \DIFadd{has }\DIFaddend proved its partial correctness with
denotational semantics, and \citet{DBLP:conf/tacs/BanerjeeHR01} have
established total correctness using operational
semantics. \citet{DBLP:conf/popl/PottierG04} have formalized
type-preserving polymorphic defunctionalization in System F extended
with GADTs.

\DIFaddbegin \paragraph{\DIFadd{Closure conversion}}

\DIFadd{Like defunctionalization, the }\emph{\DIFadd{closure conversion}} \DIFadd{transformation also
involves representing a closure as a first-order value that pairs a
kind of code identifier with a collection of free variables.
%DIF >
The formulations of closure conversion in the work referenced
\cite{DBLP:conf/popl/MinamideMH96,DBLP:conf/pldi/BowmanA18}
differ markedly from defunctionalization: while defunctionalization
involves a globally-defined map indexed by code identifiers (such as
an }\emph{\DIFadd{apply}} \DIFadd{function or our label environment), these closure
conversions instead transform functions locally into
code-and-environment pairs that can then be applied using a standard
elimination rule.
%DIF >
%DIF > % As in
%DIF > % previous formulations of defunctionalization, DCC-terms cannot create
%DIF > % new labels, while terms in target languages of closure conversion can
%DIF > % create closures.
However, in other formulations of closure
\cite{DBLP:books/cu/Appel1992,essence-closure-conversion}}\hspace{0pt}%DIFAUXCMD
where functions are lifted to top-level, the distinction is less sharp.

%DIF > % %% \begin{itemize}
%DIF > % %% \item
%DIF > % %% but reviewer B says:
%DIF > % %% \begin{quotation}
%DIF > % %% That is a too narrow characterization of closure conversion. The
%DIF > % %% literature on closure conversion is much larger than just Minamide
%DIF > % %% and Bowman \& Ahmed. It's quite common for closure conversion to
%DIF > % %% target a language with function pointers that refer to the code
%DIF > % %% stored on the heap, which certainly counts as a globally-defined
%DIF > % %% map. For example, see Andrew Appel's seminal book "Compiling with
%DIF > % %% Continuations" chapter 10 titled "Closure Conversion", especially
%DIF > % %% section 10.9 about lifting functions to the top level.
%DIF > % %% \end{quotation}
\DIFadd{Closure conversion plays a key role in compilers for many functional
languages, including Scheme~\mbox{%DIFAUXCMD
\cite{rabbit}}\hspace{0pt}%DIFAUXCMD
\cite{DBLP:conf/lfp/MaunyS86}}\hspace{0pt}%DIFAUXCMD
Standard ML~\mbox{%DIFAUXCMD
\cite{DBLP:conf/esop/CejtinJW00}}\hspace{0pt}%DIFAUXCMD
\cite{DBLP:conf/iccS/LeshchinskiyCK06} }\hspace{0pt}%DIFAUXCMD
and others.
%DIF >
Recent work has focused on establishing sophisticated semantic properties, such
as correctness of closure conversion in the presence of mutable state
and control effects (even when linked with foreign-language
\cite{DBLP:conf/ppdp/MatesPA19}}\hspace{0pt}%DIFAUXCMD
, and preservation of time and
space properties~\mbox{%DIFAUXCMD
\cite{DBLP:journals/pacmpl/Paraskevopoulou19}}\hspace{0pt}%DIFAUXCMD

\DIFaddend \paragraph{Refunctionalization}

Our backward translation (See \DIFdelbegin \DIFdel{\mbox{%DIFAUXCMD
\Cref{section:backwards}}\hspace{0pt}%DIFAUXCMD
}\DIFdelend \DIFaddbegin \DIFadd{\mbox{%DIFAUXCMD
\Cref{section:consistency}}\hspace{0pt}%DIFAUXCMD
}\DIFaddend )
is related to \emph{refunctionalization} \cite{DBLP:journals/scp/DanvyM09},
the left-inverse of defunctionalization.
As in refunctionalization,
we replace target applications $ \target{M} \,\target{ \mathop{@} }\, \target{N} $
with source applications $ \ottnt{M} \; \ottnt{N} $,
and labels $ \target{\flabel}   \ottsym{\{}   \target{\overline{ \target{M} } }   \ottsym{\}}$ with abstractions $  (  \lambda  \ottmv{x}  {:}  \ottnt{A} . \ottnt{M}  )  [   \overline{ \ottnt{M} }   \ottsym{/}   \overline{ \ottmv{x} }   ] $
based on their implementations \DIFdelbegin \DIFdel{$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \rightarrow  \target{M}  :  \target{B} ) $ }\DIFdelend \DIFaddbegin \DIFadd{$  \target{\flabel}  (\{  \target{\overline{ \target{x} } }   \ottsym{:}   \target{\overline{ \target{A} } }  \}\,,  \target{x}  \!:\!  \target{A}  \, \mapsto  \target{M}  :  \target{B} ) $ }\DIFaddend in the label context.

\begin{acks}
We thank David Sheets, Andr{\'a}s Kov{\'a}cs, and Marcelo Fiore for helpful comments.
\end{acks}

%% Bibliography
\bibliography{defun}

\newpage
\appendix

\section{Dependent defunctionalization in Agda}
\label{appendix:agda-defun}

\begin{code}%
\>[0]\AgdaSymbol{\{-\#}\AgdaSpace{}%
\AgdaKeyword{OPTIONS}\AgdaSpace{}%
\AgdaPragma{--type-in-type}\AgdaSpace{}%
\AgdaSymbol{\#-\}}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
\>[0]\AgdaKeyword{infixl}\AgdaSpace{}%
\AgdaNumber{9}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}\$\AgdaUnderscore{}}}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}\$\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{∀}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{p}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{p}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{p}\AgdaSpace{}%
\AgdaBound{x}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaSymbol{\{-\#}\AgdaSpace{}%
\AgdaKeyword{NO\AgdaUnderscore{}POSITIVITY\AgdaUnderscore{}CHECK}\AgdaSpace{}%
\AgdaSymbol{\#-\}}\<%
\\
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{Π}%
\>[8]\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[3]\AgdaInductiveConstructor{F1}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[41I]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[.][@{}l@{}]\<[41I]%
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{z}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{z}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)))))))}\<%
\\
\>[3]\AgdaInductiveConstructor{F2}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[113I]\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[.][@{}l@{}]\<[113I]%
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{z}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{z}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))))))}\<%
\\
\>[3]\AgdaInductiveConstructor{F3}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[184I]\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[.][@{}l@{}]\<[184I]%
\>[8]\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{z}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{z}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)))))}\<%
\\
\>[3]\AgdaInductiveConstructor{F4}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[254I]\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[.][@{}l@{}]\<[254I]%
\>[8]\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaSymbol{(}\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{z}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{z}\AgdaSymbol{)))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))))}\<%
\\
\>[3]\AgdaInductiveConstructor{F5}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[323I]\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[.][@{}l@{}]\<[323I]%
\>[8]\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaSymbol{(}\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{))))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{z}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{y}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{z}\AgdaSymbol{))))}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaDatatype{Π}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\<%
\\
\>[8]\AgdaBound{C}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\$}}\AgdaSpace{}%