# AdapTT: Functoriality for Dependent Type Casts

Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard

► To cite this version:

Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard. AdapTT: Functoriality for Dependent Type Casts. Proceedings of the ACM on Programming Languages, 2026, 10 (POPL), pp.628-658. 10.1145/3776664. hal-05167997v2

HAL Id: hal-05167997

https://hal.science/hal-05167997v2

Submitted on 8 Dec 2025

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

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

<figure><img src="image_1.png" /></figure>
# AdapTT: Functionality for Dependent Type Casts

ARTHUR ADJEDJ, ENS Paris-Saclay - Université Paris-Saclay, France

MEVEN LENNON-BERTRAND, Université Paris Cité, INRIA, CNRS, IRIF, France

THIBAUT BENJAMIN, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, France

KENJI MAILLARD, Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France

The ability to *cast* values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive *functoriality* of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of *adapters* relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.

CCS Concepts: • **Theory of computation** → **Type theory**; *Categorical semantics*; *Type structures*.

Additional Key Words and Phrases: Dependent types, Natural models, Inductive types

## 1 Introduction

*Type casting* is a fundamental operation in typed programming languages, turning a value of one type into a value of another to mediate between superficially different types. In the setting of proof assistants and dependent type systems, where types are extremely rich and precise, the need for such mediation is particularly dire. Proof assistants thus offer many type casting mechanisms: concussions [70] are heavily employed in RocQ [78] and Lean [55], in particular to deal with hierarchies of structures [29, 20]; predicate subtyping [71] is a central tool for verifying properties in PVS [60], the Russel sub-language of RocQ [72], and $F^*$ [75]; and cumulativity [49], present by default in RocQ and optionally in Agda [4], greatly simplifies the management of universe levels.

A particularly attractive feature of type casting is to be *structural*, meaning that type casts can be systematically lifted through type formers. Structural type casts can be applied deeply in types, rather than be confined to the top level, which makes them much more powerful and modular. And indeed, failures of typecast to properly lift through type formers manifest as painful errors that can be hard to debug [44, p.35] or expressivity limitations [35]. Structural type casting is an important feature in recent work such as Observational Type Theory (TT<sup>obs</sup>) [9, 67], dependent type theories with coercive subtyping (MLTT<sub>coe</sub>) [51, 45], or cast calculi for gradual dependent types (CastCIC) [46]. Figure 1 shows the structural type casts between function types (II) in these three systems. Although the exact mechanisms differ, in all cases the cast of a function *f* proceeds by first casting its argument before passing it to *f*, and finally casting the result back. Such striking similarities can be observed with structural casts for other type formers too. In this paper, we argue that this common core is no coincidence, but emerges from a deeper structure:

**Structural type casts arise from functorial type formers.**

Authors' Contact Information: Arthur Adjedj, ENS Paris-Saclay - Université Paris-Saclay, Gif-sur-Yvette, France, arthur.adjedj@ens-paris-saclay.fr; Meven Lennon-Bertrand, Université Paris Cité, INRIA, CNRS, IRIF, Paris, France, meven.bertrand@inria.fr; Thibaut Benjamin, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, France, thibaut.benjamin@universite-paris-saclay.fr; Kenji Maillard, Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, Rennes, France, kenji.maillard@inria.fr.

<figure><img src="image_2.png" /></figure>
$$ \frac{\Gamma \vdash e : \Pi x : A.B = \Pi x : A'.B' \quad \Gamma \vdash f : \Pi x : A.B \quad \Gamma \vdash a' : A' \quad a := \text{cast}(A', A, \text{fst}(e), a')}{\Gamma \vdash \text{cast}(\Pi x : A.B, \Pi x : A'.B', e, f) \ a' \equiv \text{cast}(B[a], B'[a'], \text{snd}(e), f a) : B[a]} $$

$$ \frac{\Gamma \vdash A' \le A \quad \Gamma, x : A' \vdash B[\text{coe}_{A',A} x] \le B' \quad \Gamma \vdash f : \Pi x : A.B \quad \Gamma \vdash a' : A' \quad a := \text{coe}_{A',A} a'}{\Gamma \vdash (\text{coe}_{\Pi x : A.B, \Pi x : A'.B'} f) a' \equiv \text{coe}_{B[a], B'[a']} (f a) : B'[a']}

$$ \frac{\Gamma \vdash A \quad \Gamma \vdash A' \quad \Gamma, x : A \vdash B \quad \Gamma, x : A' \vdash B' \quad \Gamma \vdash f : \Pi x : A.B \quad \Gamma \vdash a' : A' \quad a := \langle A \Leftarrow A' \rangle a'}{\Gamma \vdash (\langle \Pi x : A'.B' \Leftarrow \Pi x : A.B \rangle f) a' \equiv \langle B'[a'] \Leftarrow B[a] \rangle (f a) : B'[a']}

<caption>Fig. 1. Casts between Π types in observational equality, subtyping and cast calculi for gradual typing.<fnref n="1" /></caption>

Indeed, the three examples of Fig. 1 all rely on a functor structure on the Π type former, a structure independently described in any model of MLTT by Castellan et al. [16, Lemma 4.8]. In each case, this functorial structure applies to different notions of morphisms between types: observational equalities in TT<sup>obs</sup>, subtyping coercions in MLTT<sub>coe</sub> and arbitrary cast in CastCIC. This approach extends far beyond Π: Laurent et al. [45] observe that many usual type formers (Π, Σ, Id, W, +, List, ...) can be equipped with a functorial action on functions that definitionally satisfies functoriality equations, while keeping decidability of definitional equality and typing.

*Challenges of structural type casting.* Multiple difficulties arise if one tries to unify diverse instances of structural type casts. First, type casting can apply to varied notions of morphism between types, as shown in the previous examples, and a unifying framework ought to allow for this diversity. Second, type formers can introduce contravariant type casts, as exemplified by the domain of function types, and mixing variance and type dependency quickly becomes a subtle matter. Third, Laurent et al. [45] observed a strong obstruction to derive the functoriality of general inductive types encoded via the composition of atomic type formers (Π, Σ, W, ...). The last two difficulties hamper the design of a general schema for inductive type formers —as can be found in day-to-day proof assistants (ROCQ, LEAN, AGDA)— that moreover supports structural type cast.

*Introducing AdapTT.* To attack these challenges, we take a step back and provide a solid and general framework to understand cast operations, functoriality of type formers, and the relationship between the two. The dependent type theory we develop, AdapTT, comes equipped with a primitive notion of type morphisms, adapters [53], which capture the data necessary to construct a cast. The action of adapters on terms —type casting— is functorial with respect to the categorical structure adapters give to types. As a design principle, any type former in AdapTT should respect this structure as well, i.e. be functorial.

We show that AdapTT is able to encompass the above examples of type theories with structural type casts. We provide a corresponding notion of model, a variant of natural models [12] dubbed NatMod<sub>DOS</sub>, and exhibit multiple instances of this structure. Moreover, we establish a correspondence with the works of Coraglia and Emmenegger [23] and Najmaei et al. [56] that develop related semantic notions based on comprehension categories [36].

<footnote n="1">¹To highlight their similarity, we express these rules as definitional equalities, which are inter-derivable with the original rules from Pujet [64], Laurent et al. [45], and Lennon-Bertrand et al. [46] in presence of $\beta$ and $\eta$ for functions.</footnote>
*Functorial type formers with $AdapTT_2$. While AdapTT provides an adequate framework to state that a given type former is functorial on a case-by-case basis, it does not provide the means to gener- ically represent the categories with respect to which a type former is functorial, nor to derive that complex, composite types are structurally functorial. We thus extend AdapTT with type variables which provides an internalization of type formers, including their action on adapters. Contexts in this extension, $AdapTT_2$, naturally exhibit a 2-categorical structure, which harmoniously interacts with our category of types and adapters.*

AdapTT₂ gives us the tools we need to construct a theory of signatures in the style of Kaposi, Kovács et al. [43, 40, 39] to describe general inductive type formers. An inductive type described with such a signature is by construction functorial with respect to its parameters, described as a context in $AdapTT_2$, entailing a well-behaved notion of structural casts. We illustrate the expres- sivity of our signatures by describing many standard examples, and their functorial structure: lists, sum types, W types, or the inductive identity type.

*Contributions.* We bring the following to the study of type casts in dependent type theory:

• In Section 2, we introduce AdapTT, a type theory with type casts, and NatMod<sub>DO</sub>, a categorical structure in which it interprets, which we relate to previous work [23, 56];

• Section 3 extends AdapTT to a 2-dimensional type theory, $AdapTT_2$, giving the ability to internalize type formers using type variables, and exhibiting important constraints on the allowed interactions of type variance and dependency;

• We moreover show in Section 3.3 that the 2-category of (Cat-valued) presheaves on such a NatMod<sub>DO</sub> C naturally interprets $AdapTT_2$, giving rise to functorial type former on C.

• Finally, Section 4 describes a variance-aware theory of signatures, deriving structural type casts for inductive types through their inherent functorial action on adapters.

We have type checked most<sup>2</sup> rules of the paper in AGDA [3]. The point of this formalisation was not to verify properties of the system, rather, AGDA was used as a guide to ensure the numerous rules were type-correct. This only provides partial support for our work, but we still believe AGDA’s roles was valuable enough to be acknowledged.

This is the long version, with appendices, of an article [2] published at POPL '26.

# 2 A Category of Types

This section introduces AdapTT, a dependent type theory with extra structure for type casts. Section 2.1 presents its syntax while Section 2.2 defines its categorical models, with examples. Section 2.3 relates AdapTT to an existing notion of model for (relevant) subtyping: gCwF [23].

## 2.1 AdapTT, Syntactically

AdapTT, presented in Fig. 2, extends a type theory à la Martin-Löf with a judgment $\Gamma \vdash \Box : A \Rightarrow B$ for *adapters* between two types. This terminology, borrowed from McBride and Nordvall Forsberg [53], emphasizes that adapters provide information to transform values from one type to another.

The rules at the top of Fig. 2 govern the standard judgments, omitting some standard rules given in Appendix A. Overloading notations, ◇ denote both the empty context (CTXEMP) and empty substitution (SUBEMP), ▷ is used for extension of contexts (CTXEXT) and of substitutions (SUBEXT), and action of substitutions an all objects is written [·] (SUBTy, SUBTm, SUBAD). Variables use de Bruijn indices [25], generated by the $\emptyset^{\text{tm}}$th variable and the weakening substitution ↑. For instance, the named judgment $\Gamma, x: A, y: A \vdash x: A$ corresponds to $\Gamma \triangleright A \triangleright A[\uparrow] \vdash \emptyset^{\text{tm}}[\uparrow] : A[\uparrow][\uparrow]$.

<footnote n="2"><sup>2</sup>We managed to check most rules in isolation, but dire performance issues prevented us from checking them all together.</footnote>
<figure><img src="image_3.png" /></figure>

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

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

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

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

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

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

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

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

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

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

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

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

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

<figure><img src="image_17.png" /><figcaption>Fig. 2. Judgments and rules for AdapTT (excerpt, see Appendix A)</figcaption></figure>

There is an identity adapter at any type (ID), and adapters compose (COMP). With equations IDLEFT, IDRIGHT and ASSOC, types in each context form a category, preserved by substitution (SUBAD, ADAPTSUB, IDSUB, COMPSUB). The cast $a(f)$ lets an adapter $f: A \Rightarrow B$ act on a term $a: A$ to yield a term of type $B$ (ADAPT). Casts preserve identities (ADAPTID) and composition (ADAPTCOMP): these functor laws are crucial to ensure the coherence of adapters' action.<fnref n="3" />

*Example 2.1 (Function type in AdapTT).* AdapTT provides the judgments to state functoriality of type formers when adding them to the system. Illustrating this process on Π-types, for which we assume the usual MLTT rules, one can express the data required to build an adapter and how

<footnote n="3">³In the context of structural subtyping, Laurent et al. [45] show that coherent elaboration from (implicit) subsumptive subtyping to (explicit) coercive subtyping requires exactly these functorial laws.</footnote>
this adapter acts on terms of Π type, which constitute the common core of Fig. 1.

$$ \frac{\Gamma \vdash a : A' \Rightarrow A \qquad \Gamma \vdash f : \Pi A.B \quad \Gamma \vdash u : A' \qquad \Gamma \vdash a : A' \Rightarrow A \qquad \Gamma \vdash A' \vdash b : B[\emptyset^{\text{tm}}\langle a \rangle] \Rightarrow B' \qquad \Gamma \vdash (f \langle \Pi[\emptyset \vdash b] \rangle) u \equiv (f(u\langle a \rangle))\langle b[u] \rangle : B'[u]}{\Gamma \vdash \Pi[\emptyset \vdash a \vdash b] : \Pi A.B \Rightarrow \Pi A'.B'} $$

Each of the examples of Fig. 1 can be represented by making a different choice for what constitutes an adapter, which is made possible by having a separate, dedicated sort of adapters.

For datatypes, structural adapters behave like generalized map functions, so for instance

$$ (h :: t)\langle \text{List}(f) \rangle \equiv (h(f)) :: (t\langle \text{List}(f) \rangle) $$

Our goal in Section 4.2 will be to derive these functorial adapters for large classes of datatypes, together with the appropriate computation rules such as the above.

## 2.2 Models for AdapTT

AdapTT is naturally interpreted in a variation on natural models [12], which we introduce. For a category C, we write Psh(C) = $C^{\text{op}} \to \text{Set}$ for the presheaves over C, and Pst(C) = $C^{\text{op}} \to \text{Cat}$ the 2-category of Cat-valued presheaves (or pre-stacks) over C.

**Definition 2.2 (NatMod<sub>DO</sub>).*** A natural model with discrete opfibration (NatMod<sub>DO</sub>) consists of a category Ctx with a terminal object $\diamond$, two Cat-valued presheaves Ty, Tm : Ctx<sup>op</sup> $\to$ Cat and a representable natural transformation $p : Tm \to$ Ty equipped with a discrete opfibration structure in the 2-category Pst(Ctx).

By forgetting some of its structure, any NatMod<sub>DO</sub> is also a natural model in the standard sense. The representability of $p$, a key insight of Awodey [12] (and, independently, Fiore [28]), characterizes context extension $\vdash$, weakening $\uparrow$ and the variable $\emptyset^{\text{tm}}$, as a pullback in Pst(Ctx):

$$ \begin{array}{ccc} y(\Gamma \vdash A) & \xrightarrow{\emptyset^{\text{tm}}} & Tm \\ y \uparrow \downarrow & \xrightarrow{\searrow} & \downarrow p \\ y \Gamma & \xrightarrow{A} & Ty \end{array} $$

where $y : \text{Context} \to \text{Pst}(\text{Context})$ is the Yoneda embedding.<fnref n="4" /> Unfolding the definition of a discrete opfibration shows that $p$ is a discrete opfibration objectwise, together with a naturality condition. The objectwise structure gives, for any context $\Gamma : \text{Context}$ and term $t : \text{Tm}(\Gamma)$, an adapter $a : p_{\Gamma} t \to A'$ in $\text{Ty}(\Gamma)$ uniquely lifts through $p_{\Gamma}$, inducing some $\tilde{a} : t \to t'$ in $\text{Tm}(\Gamma)$ that maps to $a$ through $p_{\Gamma}$. The existence of the lifting interprets Rule ADAPT, with $t'$ above being $t\langle a \rangle$, while the uniqueness validates Rule ADAPTID and ADAPTCOMP. The naturality condition of $p$ in the discrete opfibration structure in the 2-category $\text{Pst}(\text{Context})$ corresponds exactly to the validation of Rule ADAPTSUB. Collecting these observations, we obtain the following theorem.

**THEOREM 2.3 (INTERPRETATION OF ADAPTT).** AdapTT interprets soundly into any NatMod<sub>DO</sub>.

**PROOF.** AdapTT can be presented as a Second-Order Generalized Algebraic Theory (SOGAT) (see Fig. 12) that makes very explicit that it consists of a sort of types equipped with a category structure, and a functorial action on the dependent sort of terms. The presentation of Fig. 2 has been obtained with an explicit SOGAT-to-GAT translation [41]. Following Uemura [80], a model of that SOGAT consists of a small category Ctx with a terminal object, together with a presheaf

<footnote n="4">⁴The fact that $p$ is a discrete opfibration in the 2-category $\text{Pst}(C)$ ensures that the strict pullback is a 2-pullback [74], so that all 2-categorical constructions are well-behaved.</footnote>
of types $Ty : Psh(Ctx)$ equipped with an internal category structure, a presheaf $Tm : Psh(Ctx)$, and a natural transformation $Tm \to Ty$ equipped with the structure of an internal discrete opfibration. To finish the proof, observe that internal categories in $Psh(Ctx)$ are equivalent to Cat-valued presheaves $Pst(Ctx)$, so this data exactly amounts to that of Definition 2.2. $\square$

The proof of Theorem 2.3 also shows a form of completeness of AdapTT since the notion of models of AdapTT in its SOGAT presentation coincides with NatMod<sub>DO</sub>. A notion of completeness including initiality of the syntax would require a discussion of morphisms of models that could preserve all the structure on the nose or only up to an isomorphism.

NatMod<sub>DO</sub> have many interesting examples. The admissible rules that we identify for some of these models (Examples 2.8 and 2.9) could more directly be used to *define* type theories with structural type casts, using AdapTT as a framework informing their design.

**Example 2.4 (Natural models are discrete NatMod<sub>DO</sub>)**. Since any set is trivially a category with only identity morphisms, any natural model is trivially a NatMod<sub>DO</sub> with only identity adapters. Indeed, if $Ty(\Gamma)$ is a discrete category, $p$ is automatically a discrete opfibration.

**Example 2.5 (Set as a NatMod<sub>DO</sub>)**. The standard natural model on Set extends to a non-discrete NatMod<sub>DO</sub>. Setting $Cxt := Set$, contexts are interpreted as sets and substitutions as functions. Types over a set $\Gamma$ are functors $Ty(\Gamma) := \text{discr} \Gamma \to Set$ from the discrete category $\text{discr} \Gamma$ to Set. Terms over $\Gamma$ are functors $Tm(\Gamma) := \text{discr} \Gamma \to Set$, to the category of pointed set, and $p$ is the post-composition by the functor $Set \to Set$ forgetting the point. Context extension is inherited from the natural model: the extension of a set $\Gamma$ with a family $A : \Gamma \to Set$ is given by the set $\Sigma(\gamma : \Gamma).(A \gamma)$. Expliciting the morphisms of $\text{discr} \Gamma \to Set$, an adapter $\Gamma \vdash f : A \Rightarrow B$ between $A, B : Ty(\Gamma)$ is a natural transformation $A \to B$, thus a family of functions $f : (\gamma : \Gamma) \to A \gamma \to B \gamma$ since $\Gamma$ is discrete.

**Example 2.6 (Cat as a NatMod<sub>DO</sub>)**. The NatMod<sub>DO</sub> structure on Set extends to the 1-category Cat, substituting all instances of a discrete category $\text{discr} \Gamma$ by an arbitrary one $\Gamma : Cat$. Context extension is given by the Grothendieck construction<sup>5</sup> [37, p. 1.10.1] of a type $A : \Gamma \to Set$ and the naturality condition on adapters $\Gamma \vdash f : A \Rightarrow B$ between $A, B : \Gamma \to Set$ becomes non-trivial.

**Example 2.7 (Full NatMod<sub>DO</sub>)**. In a NatMod<sub>DO</sub>, an adapter $a$ from $A$ to $B$ induces a term $\Gamma \triangleright A \vdash \Theta[a[\uparrow]] : B[\uparrow]$, and this preserves the categorical structure given by the identity adapter and adapter composition. A full NatMod<sub>DO</sub> is one where this embedding is an isomorphism, i.e. any open term induces an adapter. Any natural model $C$ can be equipped with a full NatMod<sub>DO</sub> structure by taking $\Gamma \vdash f : A \Rightarrow B := \Gamma \triangleright A \vdash f : B[\uparrow]$ and $t(f) := f[id_{\Gamma} \triangleright t]$. The identity adapter is given by the variable $\Theta^{tm}$, and composition by substitution.

Examples 2.4 and 2.7 relate to the two well-known ways to turn a natural model into a comprehension category [36, 22], either discrete or full, by making either no or all terms into arrows in the category of types. Examples 2.5 and 2.6 are instances of the latter construction.

**Example 2.8 (Subtyping)**. Coercive subtyping can be expressed with adapters: MLTT<sub>coe</sub> [45] is an instance of NatMod<sub>DO</sub> where an adapter $\Gamma \vdash f : A \Rightarrow B$ is a witness that $A$ is a subtype of $B$. Since there is at most one subtyping witness between two types, this NatMod<sub>DO</sub> validates the following “adapter irrelevance” rule, meaning that the category of types is a mere poset

$$ \text{ADIRREL} \frac{\Gamma \vdash f : A \Rightarrow B \quad \Gamma \vdash f' : A \Rightarrow B}{\Gamma \vdash f \equiv f' : A \Rightarrow B} $$

<footnote n="5">⁵The Grothendieck construction $\int_{\Gamma} A$ we consider here for $A: \Gamma \to Set$ yield an opfibration $\pi_{\Gamma}: \int_{\Gamma} A \to \Gamma$ and not a fibration. In this particular instance, the Grothendieck construction is simply a category of elements.</footnote>
For an adapter $\Gamma \vdash f : A \Rightarrow B$, the cast $a\langle f \rangle$ is given by the coercion operation $coe_{A,B} a$.

*Example 2.9 (TT<sup>obs</sup> as a NatMod<sub>DO</sub>).* Observational Type Theory (TT<sup>obs</sup>) [9] is a type theory where the operation cast : A ~<sub>U</sub> B → A → B associated to the identity type A ~<sub>U</sub> B computes structurally. Pujet and Tabareau's [66] version of TT<sup>obs</sup> is a NatMod<sub>DO</sub> instance, by taking:

$$ \mathop{\text{EQAD}} \frac{\Gamma \vdash e : A \sim_U B}{\Gamma \vdash e' : A \Rightarrow B} \qquad \mathop{\text{ADEQ}} \frac{\Gamma \vdash e : A \sim_U B \quad \Gamma \vdash a : A}{\Gamma \vdash a \langle e \rangle \equiv \text{cast } ea : B} \qquad \mathop{\text{EQREFLID}} \frac{\Gamma \vdash A}{\Gamma \vdash \underline{\text{refl}} \equiv \text{id}_A : A \Rightarrow A} $$

By Rule EQAD, any proof of observational equality between types entails an adapter with action on term given by cast (ADEQ). Casts along reflexivity proofs are identities by Rule EQREFLID, and Pujet et al. [65] show that adding this equation preserves decidability of conversion.<fnref n="6" />

It is tempting to add a similar rule for composition (where trans is transitivity of equality)

$$ \mathop{\text{EQCOMPTRANS}} \frac{\Gamma \vdash e : A \sim_U B \quad \Gamma \vdash e' : B \sim_U C}{\Gamma \vdash \underline{e} \circ \underline{e}' \equiv \underline{\text{trans}} e e' : A \Rightarrow C} $$

However, Laurent et al. [45, Appendix A] show that, using this rule, we can construct a model of pure $\lambda$-calculus in the system, by working in a context with a hypothesis $e : A = A \to A$. To avoid this obstacle to decidability of conversion, we can instead remove this equation and instead interpret composition freely: adapters are chains of equalities $\underline{e_1} \circ \dots \circ \underline{e_n}$.

*Example 2.10 (CastCIC as a NatMod<sub>DO</sub>).* CastCIC [46] has been proposed as a foundation for gradual dependent types. In CastCIC, any two types A, B are related by an adapter $\Gamma \vdash (A \Rightarrow B) : A \Rightarrow B$. Non-diagonal casts such as $\mathcal{O}(\langle \text{Nat} \Rightarrow \text{Bool} \rangle)$ reduce to runtime errors following the exceptional type theory of Pédrot and Tabareau [62]. Lennon-Bertrand et al.'s [46] fire triangle, which shows that normalization cannot hold in a system satisfying the gradual guarantees, is another avatar of the obstruction exposed by Laurent et al. regarding the above rule for transitivity.

## 2.3 Comparison with Generalized Categories with Families (gCwF)

NatMod<sub>DO</sub>, our model of AdapTT, is closely related to the generalized categories with families (gCwF) of Coraglia and Emmenegger [23]. gCwF, initially introduced under the name of “plain dependent type theories” [24], were used by Coraglia and Emmenegger [22] to establish a connection between two formalisms to model type theory: categories with families/natural models, and comprehension categories. The same authors then remarked [23] that, despite not being their original purpose, gCwF support some flavor of subtyping, without explicitly deriving a type cast operation. Najmaei et al. [56] propose a sound syntax to work in comprehension categories, and further the analysis of subtyping, deriving type casts for $\Pi$, $\Sigma$ and $\mathrm{Id}$ types. Clarifying further the status of type casts, we establish a correspondence between gCwFs and NatMod<sub>DO</sub>.

Let us start with a review of Coraglia and Emmenegger's [23] notations and terminology. Natural models can be reformulated as the following diagram [80, p. 3.1.11] where $u$ and $\dot{u}$ are discrete fibrations, and $\Sigma$ is a fibration morphism with right adjoint $\Delta$ (which is not a fibration morphism)

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

<footnote n="6">⁶Thanks to proof irrelevance, Rule EQREFLID implies the stronger rule where refl is replaced by an arbitrary proof of $A \sim A$, because such a proof is always convertible to refl.</footnote>
The base category $\mathcal{B}$ should be understood as that of contexts and substitutions, while $\mathcal{U}$ is the category of types in contexts, and $\mathcal{U}$ that of typed terms in a context. The functors $u$ and $\dot{u}$ project the underlying context of a type and a term. The discrete fibration property of $u$ and $\dot{u}$ gives the action of substitutions on types and terms. gCwF generalize the above, merely requiring $u$ and $\dot{u}$ to be fibration, without dicreteness.

Dropping the discreteness condition is relevant to model type casts. Indeed, considering an object $\Gamma$ of $\mathcal{B}$, and two objects $A, B$ of $\mathcal{U}$ in the fiber over $\Gamma$ (i.e. two types in a context $\Gamma$), it allows for non-trivial vertical morphisms $f: A \to B$ in $\mathcal{U}$, those such that $u(f) = \text{id}_\Gamma$. These play precisely the role devoted to adapters in a NatMod$_{\text{DO}}$. However, it also relaxes the structure too much to interpret AdapTT, as it makes the action of morphisms of $\mathcal{B}$ onto the fibers in $\mathcal{U}$ pseudo-functorial instead of functorial. In particular, the equations $A[\sigma \circ \tau] \equiv A[\sigma][\tau]$ and $A[id] \equiv A$ and their counterparts on terms are not valid in a gCwF. To account for this, we restrict our attention to a subclass of gCwF that we call split gCwF.

*Definition 2.11.* A split gCwF equips $u$ and $\dot{u}$ as above with a functorial choice of lifts, preserved by $\Sigma$ and $\Delta$, such that the unit and counit are componentwise the chosen lift of their projection.

To model coercive subtyping with gCwF, Coraglia and Emmenegger [23] define an additional judgment $\Gamma \vdash a : f B$ interpreted as the existence of a term $a$ of type $A$ in context $\Gamma$ together with a vertical morphism $f: A \to B$. But they do not derive a proper type cast corresponding to Rule ADAPT: assuming this data, we need to construct an element $t\langle a \rangle$ of $\mathcal{U}$ such that $\Sigma(t\langle a \rangle) = B$. The following proposition, proven in Appendix B, resolves this discrepancy.

**PROPOSITION 2.12.** Split gCwF support a cast operation: the functor $\Sigma$ induces a discrete opfibration between Cat-valued presheaves, from the presheaf of fibers of $\dot{u}$ to the presheaf of fibers of $u$.

**THEOREM 2.13.** Split gCwFs are equivalent to NatMod$_{\text{DOS}}$.

**PROOF SKETCH.** The proof closely parallels the correspondence between discrete gCwF and natural models, while additionally accounting for adapters. We briefly spell out the correspondence here and refer to Appendix B for the complete proof.

From a split gCwF, we define a NatMod$_{\text{DO}}$ with $\mathcal{B}$ as the category of contexts. The categories of types and terms in a context $\Gamma$ are respectively given by the fiber of $u$ and $\dot{u}$ over $\Gamma$. The morphism of fibrations $\Sigma$ induces the natural transformation $p: \text{Tm} \xrightarrow{\hspace{1em}} \text{Ty}$. Its right adjoint $\Delta$ then gives the context extension operation. Finally Proposition 2.12 shows that $p$ is a discrete opfibration.

Conversely, from a NatMod$_{\text{DO}}$, we define a split gCwF by defining the base category $\mathcal{B} = \text{Ctx}$, the split fibrations $u : \mathcal{U} \to \mathcal{B}$ and $\dot{u} : \mathcal{U} \to \mathcal{B}$ are obtained respectively as the Grothendieck construction of the functor $\text{Ty} : \text{Ctx}^{\text{OP}} \to \text{Cat}$, and of the functor $\text{Tm} : \text{Ctx}^{\text{OP}} \to \text{Cat}$. The natural transformation $p: \text{Tm} \xrightarrow{\hspace{1em}} \text{Ty}$ then induces a morphism of fibrations $\Sigma : \mathcal{U} \to \mathcal{U}$. The right adjoint $\Delta$ to $\Sigma$ is given by the context extension operation and the action of adapters on terms. $\square$

### 3 Representing type formers

AdapTT, as introduced in the previous section, provides a judgmental structure to capture type casts. As it stands, however, the type theory does not give good tools to uniformly describe functorial type formers. Indeed, to be able to talk about functoriality, we need to have categories between which a type former maps. We have just worked to make the codomain clear: it is the category of types and adapters. However, the domain can be much more complex: as shown by Example 2.1, it can involve multiple types, dependency, and variance information.

In the standard setting, the description of type formers' domain typically relies on universes. In AGDA, for instance, the type former for lists would be declared by:
### data List (X : Set) : Set

The universe `Set` provides a (partial) internalization of the judgment for well-formed types. In `AdapTT`, however, this will not do. As adapters are a type-level notion only, and terms form a mere set, universes in `AdapTT` could internalize types, but not their categorical structure, and are thus ill-suited to describe the category that is the domain of a type former.

To address this, we extend `AdapTT` to a theory `AdapTT₂` with a primitive notion of type variables. `AdapTT₂` will be used to satisfactorily describe the parameters of inductive types, such as `List` above, in Section 4. We start in Section 3.1 by distilling how these type variables ought to work, to explain the design of `AdapTT₂`. Then, Section 3.2 formally describes the type theory per se, while Section 3.3 builds a model of it on top of a model of `AdapTT`, providing a formal construction of functorial type formers for `AdapTT` out of `AdapTT₂`'s ones.

## 3.1 What do we want of type variables?

In this section, we motivate our choice of considering type variables and the form of the rules we provide for them by looking at examples and expected features. For the sake of presentation, we use an informal, named syntax with implicit weakenings. We switch back to a formal, name-free version in Section 3.2. Moreover, none of the rules presented here are defining a theory, but rather they constitute desiderata for rules that must be derivable in our proposed theory. For this reason some are left unnamed, and many are presented in a simplified variant.

### 3.1.1 Lists: type variables and transformations.
As we see for `List` above, the input of a type former is specified by a context. In that case, this context consists of a single type variable: $\Gamma_{\text{List}} := (X : \text{Ty})$. This is sufficient to capture the `List` type former, given by Rule `LISTUNIV` below. Indeed, by the general Rule `SUBTy`, Rule `LISTSUBS` is derivable. Moreover, a substitution $\Delta \vdash \sigma : \Gamma_{\text{List}}$ consists of a single type: $\sigma \equiv \diamond \triangleright X[\sigma]$. We hence obtain the more standard Rule `LISTTy`. Conversely, instantiating Rule `LISTSUBS` with $\text{id}_{\Gamma_{\text{List}}}$ or Rule `LISTTy` with $(X: \text{Ty}) \vdash X$, we recover Rule `LISTUNIV`.<fnref n="7" /> As all three versions are equivalent, we favor the less verbose style of Rule `LISTUNIV`.

$$ \Gamma_{\text{List}} := (X : \text{Ty}) \quad \text{LISTUNIV} \quad \frac{\Gamma_{\text{List}} \vdash \text{List}}{} \quad \text{LISTSUBS} \quad \frac{\Delta \vdash \sigma : \Gamma_{\text{List}}}{\Delta \vdash \text{List}[\sigma]} \quad \text{LISTTy} \quad \frac{\Delta \vdash A}{\Delta \vdash \text{List}(A)} $$

Type variables are given by a context extension operation $\triangleright$, given by the rules below. Any well-formed context can be extended with a type variable, which can then be accessed to yield a type. A substitution into an extension $\Gamma \triangleright (X : \text{Ty})$ is built out of a substitution into $\Gamma$ together with a well-formed type instantiating the type variable.

$$ \frac{\Gamma \vdash \Gamma}{\vdash \Gamma \triangleright (X : \text{Ty})} \qquad \frac{\Gamma \vdash \Gamma}{\Gamma \triangleright (X : \text{Ty}) \vdash X} \qquad \frac{\Gamma \vdash A}{\Gamma \triangleright (X : \text{Ty}) \vdash A} \qquad \frac{\Gamma \vdash \sigma : \Delta \quad \Gamma \vdash A}{\Gamma \vdash \sigma \triangleright A : \Delta \triangleright (X : \text{Ty})} $$

But there is more happening. Indeed, consider two substitutions $\Delta \vdash \sigma, \tau : \Gamma_{\text{List}}$, amounting to two types $X[\sigma], X[\tau]$. We have an interesting way to relate these: adapters! Hence, in `AdapTT₂`, there is a natural and interesting way to relate substitutions, which we call *transformations*, after Licata and Harper [47]. Transformations are typed by a judgment $\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau$, where $\Gamma \vdash \sigma, \tau : \Delta$, and collect adapters between their endpoints. That is, to create a transformation relating substitutions $\sigma, \tau$ respectively extended by types `A` and `B`, we must provide a transformation

<footnote n="7">⁷For the category theorist, this is a manifestation, on objects, of the (2-categorical) Yoneda lemma, which says that $\text{Ty}(\Gamma)$ is isomorphic to the category of natural transformations $\text{Sub}(\cdot, \Gamma) \to \text{Ty}$.</footnote>
$\mu : \sigma \Rightarrow \tau$ and an adapter $f : A \Rightarrow B$.

$$ \frac{\Gamma \vdash \sigma, \tau : \Delta \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \quad \tau \quad \Gamma \vdash A, B \quad \Gamma \vdash f : A \Rightarrow B}{\Gamma \vdash \mu \blacktriangleright f : \sigma \blacktriangleright A \Rightarrow \Delta \blacktriangleright (X:Ty) \quad \tau \blacktriangleright B} $$

In categorical terms, Ctx in AdapTT₂ is a 2-category, whose objects are contexts, 1-morphisms substitutions, and 2-morphisms the transformations just introduced.

Ty also interacts with this structure: transformations act on types. Indeed, the core idea of AdapTT₂ is that a transformation $\mu$ acting on a type A induces an adapter:

$$ \text{TRANS}\text{TY} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \quad \tau \quad \Delta \vdash A}{\Gamma \vdash A[\mu] : A[\sigma] \Rightarrow A[\tau]} $$

AdapTT₂ internalizes the functoriality of types: any type A in $\Delta$, given a context $\Gamma$, gives rise to a functor from the category of substitutions from $\Gamma$ to $\Delta$ to that of types in $\Gamma$, and Rule TRANS TY corresponds to the action on morphisms (transformations). This gives us a way to compute the source category of A as a functor, by analyzing the structure of its context $\Delta$. Thus, the more expressive the contexts, the more interesting functorial type formers we can capture.

For instance, for lists, we derive Rule TRANS LIST below. Specializing it as we did above, we obtain Rule AD LIST, corresponding to the usual subtyping rule for lists, or to a kind of map operation.

$$ \text{TRANS}\text{LIST} \frac{\Delta \vdash \sigma, \tau : \Gamma_{\text{List}} \quad \Delta \vdash \mu : \sigma \Rightarrow \Gamma_{\text{List}} \quad \tau}{\Delta \vdash \text{List}[\mu] : \text{List}[\sigma] \Rightarrow \text{List}[\tau]} \qquad \text{AD}\text{LIST} \frac{\Delta \vdash A, B \quad \Delta \vdash f : A \Rightarrow B}{\Delta \vdash \text{List}(f) : \text{List}(A) \Rightarrow \text{List}(B)} $$

As a more involved example, combining the formation rule for lists above and that for sums below, by a single application of Rule TRANS TY, we can derive functoriality for a combination of them.

$$ \frac{\overline{(X : Ty) \blacktriangleright (Y : Ty) \vdash X + Y}}{\Delta \vdash A, A', B, B' \quad \Delta \vdash a : A \Rightarrow A' \quad \Delta \vdash b : B \Rightarrow B' \atop \Delta \vdash (\text{List}(X + \text{List}(Y))[a \blacktriangleright b] : \text{List}(A + \text{List}(B)) \Rightarrow \text{List}(A' + \text{List}(B'))} $$

The behavior of this complex adapter is obtained by following the type's structure, i.e. by combining the functoriality of the List and + types. In general, in AdapTT₂, the functoriality of complex types is derived compositionally from that of each type former.

### 3.1.2 Identity: transformations and terms.
So far, we omitted to consider terms. However, just like types, terms should be acted upon by transformations, and conversely we should have a way to extend transformations to account for term variables. Here, the insight is that since we have only a set of terms, the only way to relate them is by a definitional equality constraint, as follows:

$$ \text{TRANS}\text{TM} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \quad \tau \quad \Delta \vdash A \quad \Gamma \vdash t : A[\sigma] \quad \Gamma \vdash u : A[\tau] \quad \Gamma \vdash t \langle A[\mu] \rangle \equiv u : A[\tau]}{\Gamma \vdash \mu \blacktriangleright t : (\sigma \blacktriangleright t) \Rightarrow \Delta \blacktriangleright (x:A) (\tau \blacktriangleright u)} $$

$$ \text{TRANS}\text{TY}\text{AD}\text{TM} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \quad \tau \quad \Delta \vdash A \quad \Gamma \vdash t : A}{\Gamma \vdash t[\sigma] \langle A[\mu] \rangle \equiv t[\tau] : A[\tau]} $$

In particular, the equality constraint required in Rule TRANS TM can be exactly recovered by specializing Rule TRANS TYAD TM to $t \equiv \emptyset^{\text{tm}}$, so the rules are in harmony.

An interesting example that uses term variables is the identity type, given by

$$ \Gamma_{\text{Id}} := (X : Ty) \blacktriangleright (x : X) \blacktriangleright (y : X) $$
We can compute that a substitution $\Delta \vdash \sigma : \Gamma_{\text{ld}}$ consists of a type $\Delta \vdash X[\sigma]$ and two of its inhabitants, while transformations between these correspond to an adapter between the types preserving the terms. In other words, we obtain the following rule:

$$ \frac{\Gamma \vdash A, B \quad \Gamma \vdash a, a' : A \quad \Gamma \vdash f : A \Rightarrow B}{\Gamma \vdash \text{Id}[[f \triangleright a \triangleright a')] : \text{Id}[A \triangleright a \triangleright a'] \Rightarrow \text{Id}[B \triangleright a \langle f \rangle \triangleright a' \langle f \rangle]} $$

We recover the complex-looking typing rule of MLTT$_{map}$ [45], completely mechanically, simply from the description $\Gamma_{\text{ld}}$. Furthermore, the computation rule we derive for it in Section 4.2 is

$$ (\text{refl } a)\langle\text{Id}[[f \triangleright a \triangleright a]]\rangle \equiv \text{refl}(a\langle f \rangle) $$

which also agrees with the one of MLTT$_{map}$.

### 3.1.3 Functions and trees: contravariance.
Type variables as just introduced are not quite enough to adequately capture all interesting examples. First, as seen in the case of $\Pi$, we need a form of contravariance: adapters for the domain need to go in the direction opposite to that of the codomain. To describe this, we annotate type variables in contexts with a direction $\text{Dir} := + | -$.

$$ \frac{\vdash \Gamma}{\vdash \Gamma \blacktriangleright (X : \text{Ty}_d)} \quad (d : \text{Dir}) $$

$$ \frac{\vdash \Gamma}{\Gamma \blacktriangleright (X : \text{Ty}_+) \vdash X} $$

Type variables from Section 3.1.1 correspond to the + direction. Crucially, we still only allow access to covariant variables: since a type $\Gamma \vdash A$ is implicitly always covariant with respect to its context, it does not make sense to directly access contravariant variables.

To nonetheless be able to use contravariant variables, and more generally describe contravariant types, we introduce an operation on contexts called *dualization*, written $\Gamma^-$. It reverses variables' direction, e.g. $((X : \text{Ty}_-) \blacktriangleright (Y : \text{Ty}_+))^-$ $\equiv$ $(X : \text{Ty}_+) \blacktriangleright (Y : \text{Ty}_-)$. Combined with the rule for (covariant) variable, this lets us e.g. derive $((X : \text{Ty}_-) \blacktriangleright (Y : \text{Ty}_+))^-$ $\vdash$ X. A contravariant type in $\Gamma$ is then simply a type in $\Gamma^-$. Equipped with dualization, we extend the rules for substitutions and transformations: we can substitute a contravariant type for a contravariant type variable but, more interestingly, the direction of adapters for a contravariant type variable is *reversed*. That is, to construct a transformation $\mu : \sigma \blacktriangleright A \Rightarrow \Delta \blacktriangleright (X : \text{Ty}_-) \tau \blacktriangleright B$, we must provide an adapter $f : B \Rightarrow A$.

$$ \frac{\Delta \vdash \sigma : \Gamma \quad \Delta^- \vdash A}{\Delta \vdash \sigma \blacktriangleright A : \Gamma \blacktriangleright (X : \text{Ty}_-)} $$

$$ \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma^- \vdash A, B \quad \Gamma^- \vdash f : B \Rightarrow A}{\Gamma \vdash \mu \blacktriangleright f : \sigma \blacktriangleright A \Rightarrow \Delta \blacktriangleright (X : \text{Ty}_-) \tau \blacktriangleright B} $$

We also allow term variables of contravariant type, although as for type variables we only allow access to those of covariant type, the other must be accessed via dualization.

$$ \frac{\Gamma^- \vdash A}{\vdash \Gamma \blacktriangleright_-(x : A)} $$

This lets us construct the context $\Gamma \to := (X : \text{Ty}_-) \blacktriangleright (Y : \text{Ty}_+)$ of the non-dependent function type, and derive the corresponding adapter typing rule.

$$ \frac{\Gamma^- \vdash A, A' \quad \Gamma \vdash B, B' \quad \Gamma^- \vdash a : A' \Rightarrow A \quad \Gamma \vdash b : B \Rightarrow B'}{\Gamma \vdash \to [[a \blacktriangleright b]] : A \to B \Rightarrow A' \to B'} $$

We can give it the computation rule $(f\langle\to[[a \blacktriangleright b]]\rangle) u \equiv (f u(a))\langle b \rangle$, a simpler variant of Example 2.1.
Another example is the type Tree of Y-branching trees with X-storing nodes, with context of parameters $\Gamma_{\text{Tree}} := (X : \text{Ty}_+) \bullet (Y : \text{Ty}_-)$ and constructors and equations as follows (where $f : X \Rightarrow X'$ and $g : Y \Rightarrow Y'$)

$$ (X: \text{Ty}_+) \bullet (Y: \text{Ty}_-) \vdash \text{leaf} : \text{Tree} \qquad (X: \text{Ty}_+) \bullet (Y: \text{Ty}_-) \triangleright (x: X) \triangleright (r: Y \to \text{Tree}) \vdash \text{node} : \text{Tree}[X \triangleright Y] $$

$$ \text{leaf}[X \triangleright Y] \langle \text{Tree}[f \triangleright g] \rangle \equiv \text{leaf}[X' \triangleright Y'] $$

$$ \text{node}[X \triangleright Y \triangleright x \triangleright r] \langle \text{Tree}[f \triangleright g] \rangle \equiv \text{node}[X' \triangleright Y' \triangleright x \langle f \rangle \triangleright r \langle Y \to \text{Tree}[f \triangleright g] \rangle] $$

By $\eta$-expansion, we can further compute that $r(Y \to \text{Tree}[f \triangleright g]) \equiv \lambda x. r[x(g)]\langle \text{Tree}[f \triangleright g] \rangle$. Again this is an inductive type whose computation rules we can automatically derive. As for functions, we see the need for the contravariant adapter $g$ which acts by “pre-composition” for node.

### 3.1.4 $\Sigma$: dependency.
So far, all our examples have been non-dependent. But if we want to capture dependent function or pair types, the type variables as introduced for now are not sufficient. To gain the ability to represent dependency, we further generalize them to bind a term-level variable. For simplicity, we allow only a single binding for now, but generalize to telescopes of types in Section 3.2. Our new rules for context extension and variables are now

$$ \frac{\Gamma \vdash A \qquad \Gamma \vdash A \qquad \Gamma \vdash \sigma : \Delta \quad \Delta \vdash A \quad \Gamma \triangleright A[\sigma] \vdash B}{\vdash \Gamma \triangleright (X: A.Ty)} $$

$$ \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Delta \vdash A \quad \Gamma \triangleright (x: A[\sigma]) \vdash f : B \Rightarrow B' [\text{id} \triangleright x \langle A[\mu] \rangle]}{\Gamma \vdash \mu \triangleright f : \sigma \triangleright B \Rightarrow_{\Delta \triangleright (X:A.Ty)} \tau \triangleright B'} $$

Accessing the type variables gives a type with access to an extra binder, and accordingly in a substitution that type variable must be replaced by one allowed to use this extra binder. Finally, transformations must be extended by an adapter between the dependent types, suitably lying over the base transformation. For instance, the context for the dependent pair type is $\Gamma_{\Sigma} := (X: \text{Ty}_+) \bullet (Y: X. \text{Ty}_+)$ where $Y$ depends on a term of type $X$. Once Rule TRANS TY is unfolded, its adapter is typed as follows

$$ \text{ADPAIREx} \frac{\Delta \vdash A, A' \quad \Delta \vdash a : A \Rightarrow A' \qquad \Delta \triangleright (x: A) \vdash B \quad \Delta \triangleright (x: A') \vdash B' \quad \Delta \triangleright (x: A) \vdash b : B \Rightarrow B' [\text{id} \triangleright x \langle a \rangle]}{\Delta \vdash \Sigma[a \triangleright b] : \Sigma(x: A).B \Rightarrow \Sigma(x: A').B'} $$

### W and $\Pi$: putting it all together.
As examples which combine both contravariance and dependency, we can look at the type W of well-founded trees, given by $\Gamma_W := (X: \text{Ty}_+) \bullet (Y: X. \text{Ty}_-)$, and the one of dependent functions $\Gamma_{\Pi} := (X: \text{Ty}_-) \bullet (Y: X. \text{Ty}_+)$, for which we also need to allow the type of variables bound by a type variable to be contravariant. We defer the general rules for variables for a moment, but the derived typing rules for adapters in these examples are as follows:

$$ \text{ADWEx} \frac{(\Delta \triangleright (x: A))^{-} \vdash B \quad (\Delta \triangleright (x: A'))^{-} \vdash B' \quad (\Delta \triangleright (x: A))^{-} \vdash b : B' [\text{id} \triangleright x \langle a \rangle] \Rightarrow B}{\Delta \vdash W[a \triangleright b] : W(x: A).B \Rightarrow W(x: A').B'} $$

$$ \text{ADFUNEx} \frac{\Delta^{-} \vdash A, A' \quad \Delta^{-} \vdash a : A' \Rightarrow A \qquad \Delta \triangleright (x: A) \vdash B \quad \Delta \triangleright (x: A') \vdash B' \quad \Delta \triangleright (x: A') \vdash b : B[\text{id} \triangleright x \langle a \rangle] \Rightarrow B'}{\Delta \vdash \Pi[a \triangleright b] : \Pi(x: A).B \Rightarrow \Pi(x: A').B'} $$
<figure><img src="image_19.png" /></figure>

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

<figure><img src="image_21.png" /><figcaption>Fig. 3. Basic structure of AdapTT₂ (excerpt)</figcaption></figure>

As we can see, there are subtle but important discrepancies in the types of the “dependent adapter” between Σ, W and Π, and the judgmental structure offered by AdapTT₂ is leveraged in correctly handling these discrepancies.

## 3.2 A 2-Dimensional Type Theory with Adapters

We are now finally in the position to give the official rules of AdapTT₂. The main judgments are collected in Fig. 3. Formally, we understand these as describing a generalized algebraic theory (GAT) [15, 14], whose sorts we also collect in Fig. 3. We use both interchangeably, i.e. write either $\sigma : \text{Sub}(\Gamma, \Delta)$ or $\Gamma \vdash \sigma : \Delta$. In premises, we often omit variables appearing in later objects, and whose sort can be inferred. The full rules are collected in Appendix D, and have been mostly type checked in AGDA as postulated symbols and equations, using rewrite rules to emulate an extensional type theory as meta-theory.

**Basic judgmental structure.** The core judgments of AdapTT₂, given on top of Fig. 3, extend those of AdapTT with transformations, which relates two substitutions. We also use the group of directions Dir with elements + and -, isomorphic to $Z/2Z$.

The base operations of AdapTT₂ are collected in the rest of Fig. 3. We omit the empty context $\diamond$ and unique substitution $\Gamma \vdash \diamond_{\Gamma} : \diamond$, similar to AdapTT. We can compose transformations, and left and right whisker a transformation by a substitution, which respectively generalize the composition of transformations, action of transformations on terms/types, and of substitution on adapters. And indeed, the former compute like componentwise versions of the latter. Categorically, these operations and their equations amount to saying that Ctx is a 2-category with Sub and Trans respectively as 1- and 2-morphisms.

As in AdapTT, Ty(Γ) also forms a category (with Ad as morphisms), but the novelty is that these categories assemble in a 2-functor Ty. That is, given $\sigma : \text{Sub}(\Gamma, \Delta)$, substitution $\cdot[\sigma]$ is a functor between Ty(Δ) and Ty(Γ) (as in AdapTT), but moreover $\cdot[[\mu]]$ is a natural transformation between
<figure><img src="image_22.png" /><figcaption>Fig. 4. Term variables in $AdapTT_2$ (equations for $\sigma \triangleright t$ and $\sigma \triangleright t^{-}$ omitted)</figcaption></figure>

the functors corresponding to its endpoints. Similarly, Tm is a “dependent 2-functor”, albeit a degenerate one: the action of a transformation on a term is a definitional equality $TRANSm$.

Finally, we have the dualization operation $\cdot^-$, which lets us represent objects that depend con-
travariantly on the context. Dualization also acts on substitutions and transformations, essentially
as the identity, although it formally reverses the direction of the latter. The empty context and
substitutions are mapped to themselves: $\diamond^{-} \equiv \diamond$ and $(\diamond \Gamma^{-})^{-} \equiv \diamond \Gamma$. Given a direction $d$: Dir,
we write $(\cdot)^d$ with the convention that $(\cdot)^{-}$ is the one of Fig. 3 and $(\cdot)^{+}$ is the identity. As $(\cdot)^{dd'}$
coincides with $((\cdot)^d)^{d'}$, this defines a group action of directions on contexts. Since directions are
a meta-level set, a rule involving direction variables should be formally understood as a family of
rules, one for each possible concrete combination of directions.

**Term variables.** Term variables (Fig. 4) behave broadly similarly to those of AdapTT, with two
differences. The first is the ability to bind variables of contravariant type, a flexibility used to
represent e.g. Π-types, as explained in Section 3.1.4. Note, however, that we only allow accessing
covariant variables in Rule VARZTM, contravariant variables have to be accessed indirectly, as we
can derive $(\Gamma \triangleright_ A)^{-} \oto \Theta_A^{\mathrm{tm}} : A[\uparrow]$ from Rule VARZTM and the equation $(\Gamma \triangleright_ A)^{-} \equiv \Gamma^{-} \triangleright_+ A$.

The second is the extension of transformations, which we touched upon in Section 3.1.2. Here we
have two rules, one for each direction, which need a different adjustment of the endpoints. Rules
TRANSm+ and TRANSm- are more economical albeit less symmetric versions of Rule TRANSm,
where we substitute $u$ by $t\langle A\llbracket\mu\rrbracket\rangle$ to which it must be equal.

Dualization acts on the primitives of Fig. 4, adjusting variance. For instance, we have

$$
\Gamma^{-} \vdash (\sigma \triangleright d t)^{-} \equiv \sigma^{-} \triangleright_{-d} t : (\Delta \triangleright d A)^{-}
$$

which is well-typed as $(\Delta \triangleright_d A)^{-} \equiv \Delta^{-} \triangleright_{-d} A$ and $A[(\sigma^{-})^{-}] \equiv A[\sigma]$.

**Functoriality of context extension.** From the primitives of Fig. 4, we can derive an operation $\bowtie$,
which categorically corresponds to the functoriality of context extension, and its equations

$$
\begin{gather*}
\underset{\text{SUBAD}}{\frac{\Gamma \vdash \sigma : \Delta \quad \Gamma^d \vdash A \quad \Delta^d \vdash B \quad \Gamma^d \vdash a : A \Rightarrow B[\sigma^d]}{\Gamma \triangleright_d A \vdash \sigma \bowtie_d a : \equiv ((\sigma^d \circ \uparrow) \triangleright \Theta^{\mathrm{tm}} \langle a[\uparrow] \rangle)^d : \Delta \triangleright_d B}} \\
(\mathrm{id}_\Gamma \bowtie_d \mathrm{id}_A) \equiv \mathrm{id}_{\Gamma \triangleright A} \quad (\tau \bowtie_d b) \circ (\sigma \bowtie_d a) \equiv (\tau \circ \sigma) \bowtie_d (b[\sigma] \circ a) \quad (\tau \bowtie_d a) \circ (\sigma \triangleright_d t) \equiv (\tau \circ \sigma) \triangleright_d t \langle a[\sigma] \rangle
\end{gather*}
$$
<figure><img src="image_23.png" /><figcaption>Fig. 5. Rules for telescopes (excerpt) – Note that telescopes only contain term variables</figcaption></figure>

*Telescopes.* In Section 3.1, we saw the need for dependent type variables. Our basic examples only need 0 or 1 binder, but to allow for a uniform treatment of these and more complex examples with more binders, we introduce telescopes, whose main rules are collected in Fig. 5. Telescopes represent context extensions, although limited to term variables only. Hence, they are lists of types (in a pre-existing context), and informally behave as iterated Σ-types. Telescopes in context Γ are built out of the empty telescope ♦ by successive telescope extension Θ ▷ A, which extends Θ with a new term variable of type A. A context Γ can be extended by a telescope Θ defined over it:

$$ \vdash \Gamma \triangleright_d \Diamond \equiv \Gamma \qquad \vdash \Gamma \triangleright_d (\Theta \triangleright A) \equiv (\Gamma \triangleright_d \Theta) \triangleright_d A $$

All types in a telescope have the same (covariant) direction. Just like for types, we can represent a contravariant telescope Θ in Γ (where all types are contravariant) as an element of Tel(Γ⁻).

Telescopes come with their own sort of adapters TelAd, which are lists of componentwise adapters between two telescopes, and instantiations Inst, which are lists of terms inhabiting the respective types of a telescope. The behavior of telescopes, instantiations and telescope adapters mirrors that of respectively types, terms and adapters, so we reuse the notations for the judgments of the latter. They come with a somewhat tedious although unsurprising calculus, where all operations are componentwise. We record only the most interesting ones: the telescope weakening ↑Θ, obtained by composing the individual weakenings for the types in Θ, i.e.

$$ \Gamma \triangleright_d (\Theta \triangleright A) \vdash \uparrow_{\Theta \triangleright A} \equiv \uparrow_{\Theta} \circ \uparrow_A : \Gamma $$

and the variable instantiation vinst, which consists of a list of variables, in that

$$ \Gamma \triangleright \Theta \triangleright A \vdash \text{vinst}_{\Theta \triangleright A} \equiv \text{vinst}_{\Theta}[\uparrow_A] \triangleright \theta^{\text{tm}} : (\Theta \triangleright A)[\uparrow] $$

This instantiation plays a role very similar to that of θ^tm. Finally, just as for terms we can define the functorial action ≀≀ of context extension by a telescope: σ ≀≀ α := (σ ◦ ↑) ≀≀ vinst(α[↑]).

*Type variables.* Using telescopes and instantiations, we can turn to type variables (Fig. 6), which combine contravariance (Section 3.1.3), and dependency (Section 3.1.4). The context Γ ▷ₜ (Θ.Tyₜ) represents the extension of Γ with a new type variable, dependent of the telescope Θ defined over Γ^d', and assumed to have direction d. Rule SUBTY gives the corresponding substitution extension: a type variable (Θ.Tyₜ) must be replaced by a type with direction d in a context extended by Θ. Rules
$$ \mathrm{CTXTY} \quad \frac{\vdash \Gamma \quad \Gamma^{d'} \vdash \Theta}{\vdash \Gamma \triangleright_{d'} (\Theta.Ty_d)} (d, d' : \mathrm{Dir}) \qquad \mathrm{SUBTY} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^{d'} \vdash \Theta \quad (\Gamma \triangleright_{d'} \Theta[\sigma^{d'}])^d \vdash A}{\Gamma \vdash \sigma \triangleright_d A : \Delta \triangleright_{d'} (\Theta.Ty_d)} (d, d' : \mathrm{Dir}) $$

$$ \mathrm{TRANSAD++} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_A \tau \quad \Delta \vdash \Theta \quad \Gamma \triangleright_+ \Theta[\sigma] \vdash A \quad \Gamma \triangleright_+ \Theta[\tau] \vdash B \quad \Gamma \triangleright_+ \Theta[\sigma] \vdash f : A \Rightarrow B[\mathrm{id}_\Gamma \triangleright_+ \Theta[[\mu]]]}{\Gamma \vdash \mu \triangleright_+ f : \sigma \triangleright_+ A \Rightarrow_{\Delta \triangleright_+ (\Theta.Ty_d)} \tau \triangleright_+ B} $$

$$ \mathrm{TRANSAD+-} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_A \tau \quad \Delta \vdash \Theta \quad (\Gamma \triangleright_+ \Theta[\sigma])^- \vdash A \quad (\Gamma \triangleright_+ \Theta[\tau])^- \vdash B \quad (\Gamma \triangleright_+ \Theta[\sigma])^- \vdash f : B[\mathrm{id}_\Gamma \triangleright_+ \Theta[[\mu]]] \Rightarrow A}{\Gamma \vdash \mu \triangleright_- f : \sigma \triangleright_- A \Rightarrow_{\Delta \triangleright_+ (\Theta.Ty_d)} \tau \triangleright_- B} $$

$$ \mathrm{WKTY} \quad \frac{\vdash \Gamma \quad \Gamma^{d'} \vdash \Theta}{\Gamma \triangleright_{d'} (\Theta.Ty_d) \vdash \uparrow : \Gamma} (d, d' : \mathrm{Dir}) \qquad \mathrm{VARZTY} \quad \frac{\vdash \Gamma \quad \Gamma^d \vdash \Theta}{\Gamma \triangleright_d (\Theta.Ty_+) \triangleright_d \Theta[\uparrow^d] \vdash \emptyset^{ty}} (d : \mathrm{Dir}) $$

<caption>Fig. 6. Type variables</caption>

TRANSAD++ and TRANSAD+- give transformations' extension for covariant telescopes. The biggest difference is the variance of the adapter: in the latter rule, the direction of the adapter is reversed compared to the former. Similar rules applying to telescopes with a contravariant dependency over the context are provided in Appendix D.6.

It might not be evident why in these rules the direction of the adapter coincides with that of the types substituted for the variable: we could imagine contravariant adapters between covariant types or vice-versa. However, this constraint arises from whiskering. Indeed, consider the data in the diagram below, from which we construct (◇ A) ◦ μ : Trans(Γ, ◇ A[σ], ◇ A[τ]).

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

The obvious computation rule is to simplify it to ◇ A[μ], which is only valid if A is covariant.

Moreover, Rules SUBTY, TRANSAD++ and TRANSAD+- are in line with the action of dualization, as directions are just right for the following equations to be type-correct:

$$ \Gamma \vdash (\sigma \triangleright_d A)^- \equiv \sigma^- \triangleright_{-d} A : \Delta \triangleright_{d'} (\Theta.Ty_d) \quad \Gamma \vdash (\mu \triangleright_d f)^- \equiv \mu^- \triangleright_{-d} f : \tau \triangleright_{-d} B \Rightarrow \sigma \triangleright_{-d} A $$

Finally, as for term variables, we have a weakening operation, and a variable zero θ^ty. This variable lives in an extended context, corresponding to the extra binders it has access to. These would typically be instantiated by providing an instantiation, and indeed we can derive

$$ \frac{\vdash \Gamma \quad \Gamma^d \vdash \Theta \quad \Gamma \triangleright_d (\Theta.Ty_+) \vdash \Theta' \quad \Gamma \triangleright_d (\Theta.Ty_+) \triangleright \Theta' \vdash \iota : \Theta}{\Gamma \triangleright_d (\Theta.Ty_+) \triangleright \Theta' \vdash \emptyset^{ty}[\uparrow \Theta' \triangleright \iota]} (d : \mathrm{Dir}) $$

That is, if we access a type variable and provide an instantiation of its binders, then we obtain a type in the current context, i.e. without extra extension.

### 3.3 Back to AdapTT and natural models

A type former Γ ⊢ F in AdapTT₂ is automatically equipped with a functorial structure with respect to its category of parameters represented by the context Γ. This structure can be transferred to any NatMod<sub>DO</sub>, i.e. model of AdapTT, which interprets the underlying type former F. To establish this
correspondence, we first explain what it means for a NatMod<sub>DO</sub> C to support a given type former in terms of presheaves over C, and how the existence of a structural type cast derives from an internal category structure on these presheaves. Such an internal category in presheaves over C can equivalently be seen as a Cat-valued presheaf over C. The main theorem of this section shows that, for any NatMod<sub>DO</sub> C, these Cat-valued presheaves Pst(C) := C<sup>op</sup> → Cat on C support a model of AdapTT<sub>2</sub>. Applying this interpretation to Γ ⊢ F in Pst(C) thus yields a structural type cast on the interpretation of the underlying type former in C.

**Definition 3.1 (Type former in a natural model).** A type former in a natural model C is a pair (D: Psh(C), F: D → Ty) of a presheaf D and a natural transformation F to the presheaf of types.

For a context Γ : C, the object D Γ represents the input parameters of the type former (D, F), while F turn such data d : D Γ into a type F<sub>Γ</sub> d : Ty(Γ).

**Example 3.2 (Π type former).** In a natural model, the Π type is given [12, Prop. 2.4] by

$$D^{\Pi} \Gamma := (A : Ty(\Gamma)) \times (B : Ty(\Gamma \triangleright A))$$

$$F_{\Gamma}^{\Pi} (A, B) := \Pi A.B : Ty \Gamma$$

**Definition 3.3 (Functorial structure on a type former).** A type former (D, F: D → Ty) in the natural model underlying a NatMod<sub>DO</sub> C has a functorial structure when D is equipped with an internal category structure and F is an internal functor from D to Ty, equipped with its internal category structure of adapters.

Given a functorial structure on a type former (D, F) and a context Γ : C, the morphisms between inputs d, d' : D Γ represents the data needed to build an adapter between F<sub>Γ</sub> d and F<sub>Γ</sub> d', while the functorial action of F<sub>Γ</sub> builds this adapter. Going back to the example of Π-types, we could equip (D<sup>Π</sup>, F<sup>Π</sup>) with the functorial structure of Example 2.1. But instead we can *derive* this structure from an interpretation, via Theorem 3.4, of the judgment Ty_▶(θ<sup>ty</sup>. Ty_+) ⊢ Π : Ty in AdapTT<sub>2</sub>, corresponding to an intrinsically functorial presentation of Π-types.

To properly establish the correspondence between NatMod<sub>DO</sub> models of AdapTT and AdapTT<sub>2</sub>, we need conditions on the size of the models. Given a universe *U*, a category C is *U*-small if its types of objects and homsets are in *U*. A NatMod<sub>DO</sub> C is *U*-small if its underlying category is and the Ty and Tm presheaves land into *U*-small categories.

**THEOREM 3.4.** *Given a *U*-small NatMod<sub>DO</sub> C, the 2-category Pst(C) of Cat-valued presheaf is a model of 2-dimensional AdapTT<sub>2</sub>.*

**PROOF SKETCH.** The construction follows ideas from 2-level type theory [10] where the outer layer is interpreted as presheaves over a model of the inner layer. Here, the inner layer is an instance of AdapTT while the outer layer is one of AdapTT<sub>2</sub>. We leverage an alternative description of Pst(C) as the 2-category Cat(Psh(C)) of categories, functors and natural transformations internal to presheaves over C [37, Ch. 7]. To manipulate these structures internally to a presheaf category, we use extensional MLTT<sup>8</sup> following Hofmann [34, Ch. 4]. Working within Psh(C), we construct the 2-category *U*-small categories equipping it with all the components to interpret AdapTT<sub>2</sub>, akin to Licata and Harper's [47] model of directed 2-dimensional type theory in Cat.

Categories, functor and natural transformation can be defined in a standard fashion in extensional MLTT. Relativizing these constructions to *U*, seen as an internal universe using Hofmann-Streicher lifting [13], we use *U*-Cat, the 2-category of *U*-small categories, as the interpretation of Ctx. *U*-Cat has a terminal object ◇, the category with a single object and morphism. A type A in a context Γ : *U*-Cat is interpreted as a functor A : Γ → *U*-Cat, substitutions acts by precomposition

<footnote n="8"><sup>8</sup>Or intensional MLTT extended with the principles of uniqueness of identity proof and function extensionality [33, 83].</footnote>
and transformations by whiskering. A term $t$ of type $A$ in $\Gamma$ is interpreted as a lax natural transformation $\diamond \to A$ [38, definition 4.2.1], where $\diamond : \Gamma \to \mathcal{L}\text{-Cat}$ is the constant functor to $\diamond$. An adapter $f$ between types $A$ and $B$ in $\Gamma$ is interpreted as a lax natural transformation $f : A \to B$, and acts on a term $t : \diamond \to A$ by vertical composition $f \circ t : \diamond_{\Gamma} \to B$. In these two cases, substitutions interpreted as functors act by whiskering and transformations interpreted as natural transformations by horizontal composition which preserve lax natural transformations. All these operations are functorial on the nose since they are interpreted by composition in a strict 2-category.

Context extensions are interpreted by variants on the Grothendieck construction: positive context extension $\Gamma \triangleright_+ A$ is interpreted by $\int_{\Gamma} A$ while the negative context extension $\Gamma \triangleright_- B$ is interpreted by $(\int_{\Gamma^{\text{op}}} B)^{\text{op}}$. The interpretation of telescopes and instantiations reuses that of types and terms. The empty telescope on $\Gamma$ is interpreted as $\diamond_{\Gamma} : \Gamma \to \mathcal{L}\text{-Cat}$. For a telescope $\Theta : \Gamma \to \mathcal{L}\text{-Cat}$ over $\Gamma$ and a type $A : \int_{\Gamma} \Theta \to \mathcal{L}\text{-Cat}$, the extension $\Theta \triangleright A$ is interpreted as the functor $\gamma : \Gamma \mapsto \int_{\Theta(\gamma)} A(\gamma, \cdot)$. The final missing piece is the interpretation of type variables. Observe that $\mathcal{L}\text{-Cat}$ is cartesian closed as a 1-category and take $\Rightarrow: \mathcal{L}\text{-Cat}^{\text{op}} \times \mathcal{L}\text{-Cat} \to \mathcal{L}\text{-Cat}$ the bifunctor sending categories $A, B$ to their functor category. The assumption that the Cat-valued presheaf $\text{Ty}$ is externally $\mathcal{L}$-small implies that $\text{Ty} : \mathcal{L}\text{-Cat}$, as well as its opposite category $\text{Ty}^{\text{op}} : \mathcal{L}\text{-Cat}$ where the direction of adapters is flipped. Interpreting direction $+$ as the identity functor $\mathcal{L}\text{-Cat} \to \mathcal{L}\text{-Cat}$ and $-$ as the opposite category functor, for any context $\Gamma$ and telescope $\Theta : \Gamma^d \to \mathcal{L}\text{-Cat}$, the interpretation of $\Gamma \triangleright_d (\Theta. \text{Ty}_{d'})$ proceeds by first composing the pair of $\Theta^{\text{op}} : \Gamma^{-d} \to \mathcal{L}\text{-Cat}^{\text{op}}$ and the constant functor with value $\text{Ty}_{d'}$ with the bifunctor $\Rightarrow$ which yield $\Theta^{\text{op}} \Rightarrow \text{Ty}_{d'} : \Gamma^{-d} \to \mathcal{L}\text{-Cat}$, and then taking its Grothendieck construction $(\int_{\Gamma^{-d}} \Theta^{\text{op}} \Rightarrow \text{Ty}_{d'})^{-d}$. $\square$

*Expressivity of $\text{AdapTT}_2$'s type variables.* $\text{AdapTT}_2$ does not offer many constructions on type variables: there are no $\Sigma$ or $\Pi$ formers that apply to type variables, even though the model sketched above would support such constructions. This design is chosen to express the functoriality rules required for type formers in $\text{AdapTT}$, only tracking the functorial dependencies between families of parameters. The restriction of telescopes in family variables to term variables is compatible with a simple model where every type is discrete and enough to express many type formers we are interested in. Extending these quantifications to family variables, which stand for non-discrete categories, would extend the expressivity of the framework but also require more intricate tracking on the directed aspect, as can be found in [47] with restrictions on the combination of polarities.

# 4 Fundamental types

With the underlying judgmental structure sorted out, we can turn back to adding interesting type formers to $\text{AdapTT}_2$. Normally, to specify a type former one gives rules for type formation, introduction, elimination, computation (β) and, possibly, uniqueness (η) [79, Rem. 1.5.1]. We worked hard to make sure that the type formation rule amounts to giving a context, as showcased in Section 3.1. This automatically implies a typing rule for the adapter —by Rule TRANSAD++—, as well as the functoriality equations. Thus, to extend a usual type former to integrate adapters, the main remaining task is to specify the interaction of the adapter with introduction and elimination forms.

## 4.1 Negative types: functions and pairs

For negative types ($\Pi$ and $\Sigma$), we can essentially follow Laurent et al. [45]. Their contexts, as given in Section 3.1 translate to the following

$$ \Gamma_{\Pi} := \diamond \triangleright_{+} (\diamond \cdot \text{Ty}_{-}) \triangleright_{-} ((\diamond \triangleright \theta^{\text{ty}}) \cdot \text{Ty}_{+}) $$

$$ \Gamma_{\Sigma} := \diamond \triangleright_{+} (\diamond \cdot \text{Ty}_{+}) \triangleright_{+} ((\diamond \triangleright \theta^{\text{ty}}) \cdot \text{Ty}_{+}) $$
$$
\begin{align*}
\text{ADFUN} &\quad \frac{\Delta \vdash \sigma, \tau : \Gamma_{\Pi} \quad \Delta \vdash \mu : \sigma \Rightarrow \tau}{\Delta \vdash \Pi[\mu] : \Pi[\sigma] \Rightarrow \Pi[\tau]} &
\text{ADPAIR} &\quad \frac{\Delta \vdash \sigma, \tau : \Gamma_{\Sigma} \quad \Delta \vdash \mu : \sigma \Rightarrow \tau}{\Delta \vdash \Sigma[\mu] : \Sigma[\sigma] \Rightarrow \Sigma[\tau]} \\
\text{ADFUNEQ} &\quad \frac{\Delta \vdash a : A' \Rightarrow A \quad \Delta \triangleright A' \vdash b : B[\text{id} \gg a] \Rightarrow B' \quad \Delta \vdash f : \Pi[A \triangleright B] \quad \Delta \vdash u : A'}{\Delta \vdash f[\Pi[a \triangleright b]] u \equiv (f u(a))(b[\text{id} \triangleright u(a)]) : B'[\text{id} \triangleright u]} &
\text{ADPAIREQ1} &\quad \frac{\Delta \vdash a : A \Rightarrow A' \quad \Delta \triangleright A \vdash b : B \Rightarrow B'[\text{id} \gg a] \quad \Delta \vdash p : \Sigma[A \triangleright B]}{\Delta \vdash \pi_1 (p(\Sigma[a \triangleright b])) \equiv (\pi_1 p)(a) : A' \\
&\qquad \Delta \vdash \pi_2 (p(\Sigma[a \triangleright b])) \equiv (\pi_2 p)(b[\text{id} \triangleright \pi_1 p]) : B'[\text{id} \triangleright (\pi_1 p)(a)]}
\end{align*}
$$

<caption>Fig. 7. Adapters for Π and Σ types</caption>

The typing rules and equations for adapters are in Fig. 7. If we compute concretely what a sub-
stitution/transformation targeting ΓΠ and ΓΣ consists of, we exactly recover rules ADFUNEx and
ADPAIREx from Section 3.1.4. We can derive a contravariant version of the rules for free by instan-
tiating them in a dualized context, for instance Π A.B is contravariant if B is and A is covariant.

Adapters compute according to the types' eliminator, following the idea that negative types
are characterized by their eliminators. Extending AdapTT₂ with λ-abstraction and application, we
recover equations on constructors, e.g. (λt)⟨Π[[a ▷ b]]⟩ ≡ λ(t[θ<sup>tm</sup>(a)])(b) via η expansion.

Moreover, the functoriality laws up to casts are derivable from the computation equations only.
Indeed, we can obtain f⟨Π[[a<sub>2</sub> ◦ a<sub>1</sub>]] ▷ (b<sub>2</sub> ◦ b<sub>1</sub>)]⟩ ≡ f⟨Π[[a<sub>1</sub> ▷ b<sub>1</sub>]] ◦ Π[[a<sub>2</sub> ▷ b<sub>2</sub>]]⟩, by first η-expanding both
sides, then triggering ADFUNEQ to compute the Π adapters away, and conclude by functoriality of
coercion, i.e. the fact that t⟨a' ◦ a⟩ ≡ t⟨a⟩⟨a'⟩. The situation for Π[[id ▷ id]] and Σ is similar.

4.2 Inductive types

To represent inductive types, we cannot rely on encodings through e.g. W types, as these necessar-
ily rely on term-level manipulations —for instance A+B is encoded as Σ(b: Bool). if b then A else B,
by using the large eliminator for booleans. As we do not internalize adapters as a type, such an
encoding would yield a degenerate notion of adapters for the + type, which is unsatisfactory.

Instead, we provide a general scheme for parametrized and indexed inductive types, capturing a
class corresponding to that originally described by Coquand and Paulin [21] and Paulin-Mohring
[61], and still used as the backbone of most proof assistants. We describe this class using a theory
of signatures, inspired by multiple existing ones [43, 40, 26]. Compared to the former two [43, 40],
we focus more closely on parameters, as it is with respect to them that (inductive) type formers
are functorial, and use the machinery of type variables and telescopes from Section 3.2 in the sig-
natures, rather than relying on an external product type and universe. Our descriptions are closer
to the latter [26], although we frame them using GATs rather than of a universe of description.

Extended GAT. To lighten the rules, we rely on two extensions to the standard setting of gener-
alized algebraic theories. The first is the list type—at the meta-level of the GAT—, which we denote
with a vector notation. We still use ◇ and ▷ for nil and cons, [x; y; ... ] for an explicit list, and c ∈ cs
for witnesses that c appears in a list cs, which are essentially de Bruijn indices. Second, we allow
ourselves a form of record types, expressed as follows:

$$
\frac{
  \vdash \Gamma_{par} \quad \Gamma_{par} \vdash \Theta_{ind} \quad \Gamma_{par} \vdash \Theta_{nr} \quad r : \overline{\text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})} \quad \Gamma_{par} \triangleright \Theta_{nr} \vdash \iota : \Theta_{ind}[\uparrow]
}{
  \{\text{nrec} := \Theta_{nr}; \text{rec} := r; \text{ind} := \iota\} : \text{ConDesc}(\Gamma_{par}, \Theta_{ind})
}
$$
$$
\begin{align*}
\text{DATADESC} &\frac{\vdash \Gamma_{par} \qquad \Gamma_{par} \vdash \Theta_{ind}}{\text{DataDesc}(\Gamma_{par}, \Theta_{ind}) \coloneqq \overline{\text{ConDesc}(\Gamma_{par}, \Theta_{ind})}} \\
\text{CONDESC} &\frac{\vdash \Gamma_{par} \qquad \Gamma_{par} \vdash \Theta_{ind} \qquad \Gamma_{par} \vdash \Theta_{nr} \qquad r : \overline{\text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})} \qquad \Gamma_{par} \triangleright \Theta_{nr} \vdash \iota : \Theta_{ind}[\uparrow] \\
&\phantom{\vdash \Gamma_{par} \qquad \Gamma_{par} \vdash \Theta_{ind} \qquad \Gamma_{par} \vdash \Theta_{nr} \qquad r : \overline{\text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})} \qquad} \{\text{nrec} := \Theta_{nr}; \text{rec} := r; \text{ind} := \iota\} : \text{ConDesc}(\Gamma_{par}, \Theta_{ind})} \\
\text{RECDESC} &\frac{\vdash \Gamma_{par} \qquad \Gamma_{par} \vdash \Theta_{ind} \qquad \Gamma_{par} \vdash \Theta_{nr} \qquad (\Gamma_{par} \triangleright \Theta_{nr})^{-} \vdash \Theta_{ar} \qquad (\Gamma_{\triangleright+} \Theta_{nr}) \triangleright_{-} \Theta_{ar} \vdash \iota : \Theta_{ind}[\uparrow] \\
&\phantom{\vdash \Gamma_{par} \qquad \Gamma_{par} \vdash \Theta_{ind} \qquad \Gamma_{par} \vdash \Theta_{nr} \qquad (\Gamma_{par} \triangleright \Theta_{nr})^{-} \vdash \Theta_{ar} \qquad (\Gamma_{\triangleright+} \Theta_{nr}) \triangleright_{-} \Theta_{ar} \vdash \iota : \Theta_{ind}[\uparrow] \\
&\phantom{\vdash \Gamma_{par} \qquad \Gamma_{par} \vdash \Theta_{ind} \qquad \Gamma_{par} \vdash \Theta_{nr} \qquad (\Gamma_{par} \triangleright \Theta_{nr})^{-} \vdash \Theta_{ar} \qquad (\Gamma_{\triangleright+} \Theta_{nr}) \triangleright_{-} \Theta_{ar} \vdash \iota : \Theta_{ind}[\uparrow]} \{\text{arit} := \Theta_{ar}; \text{rind} := \iota\} : \text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})
\end{align*}
$$

<caption>Fig. 8. Signatures for inductive types, constructors and recursive arguments</caption>

This rule adds a new “record sort” `ConDesc`, indexed by a context and a telescope, with three fields `nrec`, `rec` and `ind`, accessed by `c.nrec`. These extensions can be encoded in standard GATs at the cost of introducing new sorts, operations and equations, which would only add distraction.

**Signatures.** Signatures, presented in Fig. 8, are built out of three additional sorts: inductive descriptions `DataDesc`, constructors descriptions `ConDesc` and recursive argument descriptions `RecDesc`. The description of an inductive type `I`: `DataDesc` is indexed by a context `Γpar` of parameters and a telescope `Θind` of indices, and consists of a list of constructor descriptions. A constructor description `c`: `ConDesc` consists of a telescope `nrec` of non-recursive arguments, a list `rec` of recursive argument description, and a final instantiation `ind` of indices, which can depend on the non-recursive arguments<fnref n="9" />. Finally, the description of a recursive argument `r`: `RecDesc` is given by a telescope of arities `arit` binding additional parameters for a recursive argument, corresponding to a “branching” argument, and an instantiation `rind` of the indices for the recursive occurrence. Note that, crucially, the arity is a *contravariant* telescope, as an adapter acts on recursive arguments’ parameters by pre-composition, generalizing the examples of trees in Sections 3.1.3 and 3.1.4.

**Example 4.1 (List).** List has one covariant type parameter and no indices, i.e. $\Gamma_{List} := \diamond \triangleright_+ (\diamond \cdot \Gamma_{Ty_+})$ is the context of parameters and $\diamond$ the telescope of indices. The description is given by

$$
\begin{align*}
c_{nil} &\coloneqq \{\text{nrec} := \diamond; \text{rec} := \diamond; \text{ind} := \diamond\} : \text{ConDesc}(\Gamma_{List}, \diamond) \\
c_{cons} &\coloneqq \{\text{nrec} := \diamond \triangleright \theta^{ty}; \text{rec} := [\{\text{arit} := \diamond; \text{rind} := \diamond\}]; \text{ind} := \diamond\} : \text{ConDesc}(\Gamma_{List}, \diamond) \\
listDesc &\coloneqq [c_{nil}; c_{cons}] : \text{DataDesc}(\Gamma_{List}, \diamond)
\end{align*}
$$

The constructor `nil` has no arguments, and `cons` has two arguments, a non-recursive one typed by the unique type parameter, and a recursive one with empty arity, i.e. no branching.

We omit the type `Nat`, which is similar. We use `0` and `S` for its two constructors.

**Example 4.2 (Vectors).** The type of vectors is similar to lists, except that there is now an index of type `Nat`, i.e. we take $\Theta_{Vec} := \diamond \triangleright Nat : \text{Tel}(\Gamma_{List})$. Constructors are given by

$$
\begin{align*}
c_{nil} &\coloneqq \{\text{nrec} := \diamond; \text{rec} := \diamond; \text{ind} := \diamond \triangleright 0\} : \text{ConDesc}(\Gamma_{List}, \Theta_{Vec}) \\
c_{cons} &\coloneqq \{\text{nrec} := \diamond \triangleright \theta^{ty} \triangleright Nat; \text{rec} := [\{\text{arit} := \diamond; \text{rind} := \diamond \triangleright \theta^{tm}\}]; \text{ind} := S[\theta^{tm}]\} \\
&\qquad : \text{ConDesc}(\Gamma_{List}, \Theta_{Vec}) \\
\text{vecDesc} &\coloneqq [c_{nil}; c_{cons}] : \text{DataDesc}(\Gamma_{List}, \Theta_{Vec})
\end{align*}
$$

<footnote n="9">⁹Allowing indices to depend on recursive arguments would yield descriptors for inductive-inductive type former. This is also what allows separating non-recursive arguments and recursive ones without losing generality.</footnote>
The index is instantiated in both constructors, and in the recursive argument of $c_{cons}$.

**Example 4.3 (Sum).** The sum type has two non-dependent, covariant parameters, thus we take $\Gamma_+ := \diamond \triangleright_+ (\diamond.Ty_+) \triangleright_+ (\diamond.Ty_+)$, and no index. It is given by

$$ c_{inl} := \{nrec := \diamond \triangleright \theta^{\text{ty}}[\uparrow]; rec := \diamond; ind := \diamond\} : \text{ConDesc}(\Gamma_+, \diamond) $$

$$ c_{inr} := \{nrec := \diamond \triangleright \theta^{\text{ty}}; rec := \diamond; ind := \diamond\} : \text{ConDesc}(\Gamma_+, \diamond) $$

$$ \text{sumDesc} := [c_{inl}; c_{inr}] : \text{DataDesc}(\Gamma_+, \diamond) $$

We have two constructors with one non-recursive argument, of either the first or second parameter.

**Example 4.4 (Trees).** The type W of well-founded trees is given by the following:

$$ \Gamma_W := \diamond \triangleright_+ (\diamond.Ty_+) \triangleright_+ (\diamond \triangleright \theta^{\text{ty}}.Ty_-) : \text{Ctx} $$

$$ c_{sup} := \{nrec := \diamond \triangleright \theta^{\text{ty}}[\uparrow]; rec := \diamond \triangleright \{arit := \theta^{\text{ty}}; rind := \diamond\}; ind := \diamond\} : \text{ConDesc}(\Gamma_W, \diamond) $$

$$ WDesc := [c_{sup}] : \text{DataDesc}(\Gamma_W, \diamond) $$

This time we see a non-empty arity for its unique constructor, whose recursive argument is branching. Note also that because the second variable of $\Gamma_W$ appears in contravariant position (as “width” of the branching), it is declared with direction $-$.

**Example 4.5 (Identity).** The identity type has two parameters, a type and a term of that type, and one index, again a term of that type.<fnref n="10" /> The single constructor for reflexivity has no arguments, and its index is the second parameter, thus

$$ \Gamma_{\text{ld}} := \diamond \triangleright_+ (\diamond.Ty_+) \triangleright \theta^{\text{ty}} \qquad \Theta_{\text{ld}} := \diamond \triangleright \theta^{\text{ty}}[\uparrow] $$

$$ c_{refl} := \{nrec := \diamond; rec := \diamond; ind := \theta^{\text{tm}}\} : \text{ConDesc}(\Gamma_{\text{ld}}, \Theta_{\text{ld}}) $$

$$ \text{idDesc} := [c_{refl}] : \text{DataDesc}(\Gamma_{\text{ld}}, \Theta_{\text{ld}}) $$

**Constructors.** Given a signature, we first construct the corresponding type and term constructors, in Fig. 9. The inductive type, INDTy, is easy: we simply read off the parameters and indices from the description, and declare the well-formedness of a type in the former extended by the latter. As explained in Section 3.1.1, this suffices to recover the type in an arbitrary context by substitution.

For constructors, Rule INDCSSTR is a bit more complicated, and relies on an auxiliary telescope conData, whose instantiations correspond to the arguments of the constructor. This telescope is computed with respect to an extra variable depending on the telescope of indices, and the loop is tied by instantiating this variable with the inductive itself. In turn, conData is computed by concatenating the telescope of non-recursive arguments and that of recursive arguments. The latter are computed from their description by recData, which, for each recursive argument, builds a $\Pi$ with domain the arity and codomain the extra type variable, properly instantiated.

**Adapters.** From the data of Fig. 9, we can already derive an adapter ind($I$) $[\tilde{\mu}]$ given any $\Delta \vdash$ $\tilde{\mu} : pi \Rightarrow \Gamma_{par} \vdash \Theta_{ind} pi'$. The missing piece is to give equality rules for the action of this adapter on constr. First, by extensionality for substitutions, such a $\tilde{\mu}$ must be of the form

$$ \Delta \vdash \mu \triangleright \iota : p \triangleright \iota \Rightarrow_{\Gamma_{par} \vdash \Theta_{ind}} p' \triangleright \iota \langle \Theta_{ind} [\mu] \rangle $$

for $\Delta \vdash \mu : p \Rightarrow_{\Gamma_{par}} p'$ and $\Delta \vdash \iota : \Theta_{ind}[p]$. That is, any “inductive adapter” consists of a transformation between two parameter substitutions, and a constraint between indices of the source and

<footnote n="10">¹⁰This is the “based” identity type. Alternatively, we could consider both terms to be indices.</footnote>
<figure><img src="image_25.png" /><figcaption>Fig. 9. Inductive type and term constructors</figcaption></figure>

<figure><img src="image_26.png" /><figcaption>Fig. 10. Inductive adapter equation, without and with indices</figcaption></figure>

target types. Following this decomposition, we aim to characterize a term of the form

$$ \mathrm{constr}(ic)[p \triangleright argn \triangleright argr] \langle \mathrm{ind}(I) \llbracket \mu \triangleright c_{\mathrm{ind}}[p \triangleright argn] \rrbracket \rangle $$

Indeed, as the term constructor is given in its universal context in Fig. 9, we must also account for a substitution $p \triangleright argn \triangleright argr$.

In the end, we obtain Rule INDADEQ of Fig. 10. The core idea is more readable without indices, in the simplified Rule INDADEQPAR: we rely on the fact that conData is a telescope to derive an action of the transformation $\mu$ on it, which provides an adapter by which we can adapt the arguments of
$\overline{(X: Ty_+) \vdash List}$

$\overline{(X: Ty_+) \vdash \text{nil} : \text{List}[X]}$

$\overline{(X: Ty_+) \triangleright (x: X) \triangleright (y: \text{List}[X])} \vdash \text{cons} : \text{List}[X]$

$\Delta \vdash f : A \Rightarrow A' \quad \Delta \vdash a : A \quad \Delta \vdash l : \text{List}[A]$

$\Delta \vdash \text{nil}[A] \langle \text{List}[[f]] \rangle \equiv \text{nil}[A'] : \text{List}[A']$

$\Delta \vdash \text{cons}[A \triangleright a \triangleright l] \langle \text{List}[[f]] \rangle \equiv \text{cons}[A' \triangleright a(f) \triangleright l \langle \text{List}[[f]] \rangle] : \text{List}[A']$

$\overline{(X: Ty_+) \triangleright (n: \text{Nat}) \vdash \text{Vec}}$

$\overline{(A: Ty_+) \vdash \text{nil} : \text{Vec}[A \triangleright 0]}$

$\overline{(A: Ty_+) \triangleright (x: A)(y: \text{Nat}) \triangleright (z: \text{Vec}[A \triangleright y])} \vdash \text{cons} : \text{Vec}[A \triangleright S[y]]$

$\Delta \vdash f : A \Rightarrow A' \quad \Delta \vdash a : A \quad \Delta \vdash n : \text{Nat} \quad \Delta \vdash v : \text{Vec}[A \triangleright n]$

$\Delta \vdash \text{nil}[A] \langle \text{Vec}[[f \triangleright 0]] \rangle \equiv \text{nil}[A'] : \text{Vec}[A \triangleright 0]$

$\Delta \vdash \text{cons}[A \triangleright a \triangleright n \triangleright v] \langle \text{Vec}[[f \triangleright S[n]]] \rangle \equiv \text{cons}[A' \triangleright a(f) \triangleright n \triangleright v \langle \text{Vec}[[f \triangleright n]] \rangle] : \text{Vec}[A' \triangleright S[n]]$

$\overline{(X: Ty_+) \triangleright (Y: Ty_+) \vdash +}$

$\overline{(X: Ty_+) \triangleright (Y: Ty_+) \triangleright (x: X) \vdash \text{inl} : +[X \triangleright Y]}$

$\overline{(X: Ty_+) \triangleright (Y: Ty_+) \triangleright (y: Y) \vdash \text{inr} : +[X \triangleright Y]}$

$\Delta \vdash f : A \Rightarrow A' \quad \Delta \vdash g : B \Rightarrow B' \quad \Delta \vdash a : A \quad \Delta \vdash b : B$

$\Delta \vdash \text{inl}[A \triangleright B \triangleright a] \langle +[[f \triangleright g]] \rangle \equiv \text{inl}[A' \triangleright B' \triangleright a(f)] : +[A' \triangleright B']$

$\Delta \vdash \text{inr}[A \triangleright B \triangleright b] \langle +[[f \triangleright g]] \rangle \equiv \text{inr}[A' \triangleright B' \triangleright b(g)] : +[A' \triangleright B']$

$\overline{(X: Ty_+) \triangleright (Y: X. Ty_-)} \vdash W$

$\overline{(X: Ty_-) \triangleright (Y: X. Ty_+) \triangleright (x: X) \triangleright (z: Y[\text{id} \triangleright x] \rightarrow W[X \triangleright Y])} \vdash \text{sup} : W[X \triangleright Y]$

$\Delta \vdash f : A \Rightarrow A' \quad \Delta \triangleright (x: A) \vdash g : B' \langle \text{id} \triangleright x(f) \rangle \Rightarrow B \quad \Delta \vdash a : A \quad \Delta \vdash s : B[\text{id} \triangleright a] \rightarrow W[A \triangleright B]$

$\Delta \vdash \text{sup}[A \triangleright B \triangleright a \triangleright s] \langle W[[f \triangleright g]] \rangle \equiv \text{sup}[A' \triangleright B' \triangleright a(f) \triangleright s \rightarrow [[g[\text{id} \triangleright a] \rightarrow W[[f \triangleright g]]]]] : W[A' \triangleright B']$

$\overline{(X: Ty_+) \triangleright (x: X) \triangleright (y: X) \vdash \text{id}}$

$\overline{(X: Ty_+) \triangleright (x: X) \vdash \text{refl} : \text{id}[X \triangleright x \triangleright x]}$

$\Delta \vdash f : A \Rightarrow A' \quad \Delta \vdash a : A$

$\Delta \vdash \text{refl}[A \triangleright a] \langle \text{id}[[f \triangleright a \triangleright a]] \rangle \equiv \text{refl}[A' \triangleright a(f)] : \text{id}[A' \triangleright a(f) \triangleright a(f)]$

<caption>Fig. 11. Example computation of adapters for inductive types</caption>

the constructor. The adapter we use, $(\text{conData}(c)[\text{id} \triangleright \text{ind}(I)])[[\mu]]$, is obtained directly from the type of *arg*. However, we can compute it with the equation for the whiskering, and derive it is equal to $\text{conData}(c)[[\mu] \triangleright \text{ind}(I)][[\mu]]$. This intuitively corresponds to the fact that the transformation acts on the *conData* by using $\mu$ for the parameters, and recursively relies on $\text{ind}(I)][[\mu]]$ for recursive positions. The final rule is more noisy, as it has to account for indices, but as these are essentially constrained by a definitional equality, there is not much more happening on their end.

**Example 4.6 (Computation of adapters).** We can now revisit Examples 4.1 to 4.5 in Fig. 11. We switch back to named syntax, and use named constants for term and type constructors, in the obvious way: $\text{nil} \equiv \text{constr}(ic)$ where $ic: c_{\text{nil}} \in \text{listDesc}$, and $\text{List} \equiv \text{ind}(\text{listDesc})$. We also conflate adapter $f: A \Rightarrow A'$ and transformations $\diamond \triangleright f: \diamond \triangleright A \Rightarrow \diamond \triangleright A$, and similarly for substitutions.
*Non-Example 4.7 (Mixed variance).* Types in AdapTT₂ being fully covariant (or contravariant) slightly limits our expressivity. Consider the (simplified version of the) type of indexed trees, IW, given by parameters $\Gamma_{IW} := (I: Ty_+) (X: Ty_+) (Y: Ty_-) (d: X \to Y \to I)$, indices $\Theta_{IW} := I$, and constructor sup : $\Pi(i: I) (x: X) (\Pi(y: Y). \text{IWIXY}(d \times y))$. IWXYi. However, as $Y \to I: Ty_+$ but $X: Ty_+$, the type $X \to Y \to I$ of d is actually ill-formed. Making X contravariant instead is not a solution, as it would break the quantification over $x: X$ —and be inconsistent with plain W.

This is not an oversight. Indeed, if one tries to describe an ad-hoc adapter between IW IXY d and IW I' X' Y' d', one certainly needs adapters $a_I : \text{Ad}(I, I')$, $a_A : \text{Ad}(A, A')$ and $a_B : \text{Ad}(B', B)$. But when trying to write the constraint between d and d', one ends up needing

$$ (x: X) \triangleright (y: Y) \vdash (d \times (a_A \rangle) y) (a_I \rangle) \equiv d' \times y (a_B \rangle) : I' $$

The adapters $a_I$, $a_A$ and $a_B$ act simultaneously on both sides, which goes beyond Rules TRANS TM and TRANS TY AD TM. Describing such mixed actions seems possible using spans, but this would be considerably more involved than our current setup, so for now we refrain from exploring it. This issue also explains why our telescopes have a uniform variance.

*Recursors and fusion law.* As it is mainly orthogonal to our functoriality concerns and very tedious, we do not describe the derivation of a cursor for our datatype descriptions here.

There is, however, one interaction worth investigating, that was dubbed fusion law [45]. In Section 4.1, we described the action of adapters only on destructors, but, thanks to $\eta$ laws, this entailed a derivable equality for adapters on constructors. For inductive types, we only have an equation for adapters on constructors, which entails no equation for the cursor in the absence of an $\eta$ law. The fusion law is such an equation, saying that applying a cursor on a term $t \langle \text{indAd}(I, \mu) \rangle$ amounts to applying to $t$ a cursor where $\mu$ is pushed in the branches. Categorically, this says that the family (over $\Gamma_{par}$) of initial algebras ind($I$) is natural, in that computing the section of a displayed algebra after the action of $\mu$ coincides with the section of a different displayed algebra, directly pre-composed with $\mu$.

*Functorial type formers from descriptions.* To wrap up this section, we revisit Theorem 3.4 with inductive type descriptions at hand. Unfolding the construction of the model of AdapTT over a NatMod<sub>DO</sub>, the constant introduced by a description $I: \text{DataDesc}(\Gamma_{par}, \Theta_{ind})$ in AdapTT₂ lets us compute the rules C must satisfy to support the functorial inductive type former presented by $I$.

To illustrate this, consider the description of W-types from Example 4.4. The interpretation of $\Gamma_W := (X: \diamond.Ty_+) \triangleright_+ (Y: \diamond \triangleright \Theta^{\text{ty}}.Ty_-)$ via Theorem 3.4 yields a Cat-valued presheaf that can be evaluated at an object $\Gamma$ of C: its objects are pairs $(\Gamma \vdash A, \Gamma \triangleright (x: A) \vdash B)$ of a type in $\Gamma$ and a family over it, while its morphisms are pairs of adapters $(\Gamma \vdash f: A \Rightarrow A', \Gamma \triangleright (x: A) \vdash g: B'[\text{id} \triangleright x \langle f \rangle] \Rightarrow B)$. Requiring functorial W types to exist then corresponds to the admissibility of the two following rules, whose premises have been computed from $\Gamma_W$.

$$ \frac{\Gamma \vdash A \quad \Gamma, x: A \vdash B}{W \ A \ B} $$

$$ \frac{\Gamma \vdash f: A \Rightarrow A' \quad \Gamma \triangleright (x: A) \vdash g: B'[\text{id} \triangleright x \langle f \rangle] \Rightarrow B}{\Gamma \vdash W[[f \triangleright g]] : W \ A \Rightarrow B} $$

We can also compute the action of this adapter on the constructor.

$$ \frac{\Delta \vdash f: A \Rightarrow A' \quad \Delta \triangleright (x: A) \vdash g: B'[\text{id} \triangleright x \langle f \rangle] \Rightarrow B \quad \Delta \vdash a: A \quad \Gamma \triangleright (b: B[\text{id} \triangleright a]) \vdash k: W \ A \ B}{\Delta \vdash \sup a (\lambda b.k) \langle W[[f \triangleright g]] \rangle \equiv \sup (a \langle f \rangle) (\lambda b'.(k (b' \langle g \rangle)) \langle W[[f \triangleright g]] \rangle) : W \ A' \ B'} $$

In general, considering descriptions in AdapTT₂ which are more constrained and informative thanks to variance information, we can derive everything needed for a functorial type former in
the sense of Definitions 3.1 and 3.3: the source category of the type former as functor, the way to construct a type and adapter from this information, and the equations satisfied by said adapter.

# 5 Related work

**Type casting.** Type casting is ubiquitous in dependent type theory, and has been studied in many forms. The most pervasive one is provided by propositional equality, which itself comes in many flavours: inductive [52], univalent [79], cubical [18], observational [9, 67]... Observational equality is the most directly structural, and it is hence the most natural to relate to AdapTT. However, since we do not force adapters to be unique, other forms of equality could a priori work with AdapTT, similarly to Example 2.9. It might be particularly interesting to explore how AdapTT could interact with the ongoing work of higher observational type theory [7].

Another common approach to type casting is subtyping. Here the main divide is between subsumptive subtyping, where the same underlying term is given multiple types, and coercive subtyping, with an explicit operation.<fnref n="11" /> Subsumptive subtyping is closer to what users expect —not having to insert coercions—but has a non-algebraic character which makes it impossible to capture with GATs, and causes theoretical issues [48], although it can be described with a more refinedibrational view [54]. However, Laurent et al. [45] show that focusing on coercive subtyping, which is the one AdapTT allows (see Example 2.8), is not really an issue, as a flexible enough coercive system can emulate a subsumptive one. For this, though, functoriality equations are paramount.

**Comprehension categories.** Coraglia and Emmenegger [22, 23] analyze comprehension categories [36] as models of type theory in terms of natural models and remark they carry structure akin to (proof-relevant) subtyping. Najmaei et al. [56] further this comparison, chiefly motivated by semantics, and explore models generated by weak algebraic factorization system with a natural induced notion of morphism between types. We arrive at a similar understanding from the opposite perspective: even though our initial motivation lie in the syntax for casts/subtyping, we also converge to the notion of comprehension categories. This coincidence of two different research lines with rather different motivations is remarkable, and shows how natural NatMod<sub>DOS</sub> are.

The emphasis on models in these works comes with an important difference regarding strictness: Najmaei et al. [56] focus on a syntax faithfully representing comprehension categories, where fibrations are not necessarily split. Hence, many correspondences are only up to isomorphism, e.g. A[id] and A are isomorphic rather than convertible. As we aim primarily for a usable syntax, we were happy to strictify these equations – as done in Najmaei et al.’s CCTT<sub>split</sub> –, trading splitness for a lighter syntax. Coraglia and Emmenegger similarly mention “[they] have written the action of reindexing as if the fibrations involved were split [which] allows [them] to simplify notation in the rules”.

The treatment of functorial types presents a second difference. Najmaei et al. focus on a handful of types (Π,Σ and Id), for which they give dedicated rules in their equivalent CCTT of our AdapTT. This presentation does not provide a general framework to capture the functoriality of types, as granted by AdapTT<sub>2</sub>. On the other hand, they are careful to separate the structure for a given type former on a model from the extra subtyping structure for that type former. We take the different view, embodied by AdapTT<sub>2</sub>, that every type (former) should be functorial — possibly with respect to a discrete source category.

**Representing inductive types.** Chapman et al. [17] pioneered the description of inductive types through a type of descriptions. Escot and Cockx [26] leveraged similar descriptions for metaprogramming in AGDA, introducing telescopes as we do. Our notion of inductive descriptions remain

<footnote n="11">¹¹The subsumptive/coercive terminology is due to Luo [50].</footnote>
external as a judgment, heavily inspired by the theories of signatures of Kovács [43] and Kaposi and von Raumer [40]. The very structured descriptions provided by these approaches are crucial for us, and we could not use encodings via (indexed) containers [1, 8], which fundamentally rely on a detour via universes and large elimination.

*Functoriality and parametricity.* Beyond the works already mentioned featuring structural co-
ercions [45, 46, 9, 67, 65], another line with strong connections to ours is that on univalent para-
metricity [77]. Although relying on (binary) parametricity rather than functoriality, the end result
is a form of transport that follows the structure of type formers. The subsequent work on TROCQ
[19] extends this approach to a rich hierarchy of possible relations between types along which
one can (partially) transport, from the basic existence of a function to full-blown equivalence, the
only one covered by univalent parametricity. This careful study could inform the extension of
AdapTT₂ with subtler forms of variance, while our work could inform how to extend TROCQ to
handle inductive types. Arkor [11] also models type variables in System F using 2-categories.

*Directed and Multimodal Type Theories.* Theorem 3.4 is directly inspired by the work of Licata and Harper [47] on a 2-dimensional directed type theory corresponding to Cat. Further work on 2-dimensional directed type theory have focused on the internalization of morphisms as a type [58, 57] and on bicategorical models [5]. Garner [30] presents a 2-dimensional variant of MLTT with *undirected* 2-cells as a step toward higher-models of identity types, recently extended to all type formers of MLTT with weak computational rules by Spadetto [73]. In the setting of homotopy type theory, Riehl and Shulman [68] propose a framework for synthetic $(\infty, 1)$-categories where every function between types behaving as categories (Segal types) are automatically functorial, with a cubical and constructive variant investigated by Weaver and Licata [81]. Gratzer et al. [32] design another variant based on simplicial type theory relying on multi-modal dependent type theory [31] which we could take inspiration from for extending AdapTT$_2$.

*Presheaf Models of Dependent Type Theory.* Using Hofmann’s [34, Ch. 4] model of MLTT in presheaves is a recurrent theme in our work. Uemura [80] proposes to use presheaf categories as a semantics for Second-Order Generalized Algebraic Theories (SOGAT), that we employ (Fig. 12) to give a concise description of AdapTT. The articulation of AdapTT and AdapTT₂ is reminiscent of 2-level type theory [10] and the internal construction of the 2-category of categories mirrors the axiomatic construction of cubical models in Orton and Pitts [59]. Weber [82] introduces the notion of (elementary) 2-topos to abstract over the typical case of a 2-category of internal categories, suitable for a general semantics of AdapTT₂.

# 6 Perspectives

We have provided a foundational framework to understand type casting operations in dependent type theory. This framework has close kinship to existing classes of models, particularly comprehension categories [36, 23, 56], although it is closer to established syntaxes and type systems, making it appealing for potential implementations. Our main contribution is the systematic study of functorial type formers in this framework, providing a general explanation of the structural aspects of type casting. This relies on the introduction of variable for dependent types, giving rise to an elegant 2-categorical structure which let us easily derive functoriality for complex composite types. The work culminates in the derivation of functoriality for a general class of indexed inductive types, from their description in a suitable theory of signatures.

We hope our work will inform the design of novel coercion systems in proof assistants and de-
pendently typed programming languages, and pave the way for further study of topics which are
both critical for practical usability and theoretically rather poorly understood, despite longstanding interest. Many avenues are still open for further theoretical and practical investigations.

*Variations on variance.* AdapTT₂ only features co- and contravariant types and type variables, leaving the field open to extensions that we sketch here. First, allowing mixed variance in types and telescopes would support Non-Example 4.7. From the analysis there, handling mixed variance, that is, types whose action on a transformation generates some more complex data than a single adapter in one or the other direction, seem to require working with spans.

Second, an equivariant direction characterizing types with only trivial adapters would be useful to describe types from AdapTT which cannot be directly typed in AdapTT₂. For instance, the identity function's type $A \to A$ needs $A$ to be both co- and contravariant, which could be obtained for an equivariant $A$. We conjecture this to be the sole obstruction to embed AdapTT into AdapTT₂.

Third, strict positivity of inductive types can itself be expressed using variance [27]. Doing so with the infrastructure of AdapTT₂ would simplify the description of inductive types, and enable nested types, i.e. inductive types where a recursive occurrence appears as parameter of another inductive type. Moreover, Escot et al. report that their AGDA implementation suffers from interactions of variance with structural subtyping, which would could alleviated using AdapTT₂.

*Generating adapters.* Beyond the examples of TT<sup>obs</sup>, MLTT<sub>coe</sub> and CastCIC, many more instances of ground adapters would make sense as extensions AdapTT: user-defined coercions à la Rocq or LEAN, cumulativity as an adapter $Ad(\mathcal{U}_i, \mathcal{U}_j)$ between universes whenever $i \le j$, record coercions as a building block for algebraic hierarchies [63], refinement between subset types as employed in PVS [71], F* [76] and liquid type systems [69]. AdapTT gives a good lens to (re)analyze these instances of type casts, and the framework provided by AdapTT₂ could greatly help in obtaining enhanced, structural versions, well-behaved thanks to definitional functoriality.

*Metatheory & Implementation.* We did not attempt to prove normalization or decidability of type-checking for our languages, though we conjecture these properties should hold. Indeed, very few such proofs cover a general class of inductive types, limiting the interest of the challenge. However, despite its rich equational theory, conversion in AdapTT₂ is intentional enough to be decidable. At a high level, apart from the unproblematic $\beta$ and $\eta$ rules, deciding the additional functor laws should follow the strategy of MLTT<sub>map</sub> [45] and reduce to functoriality of adapters at inductive types that can be dealt by using ideas from Allais et al.'s [6] v-equations.

An important insight by McBride and Nordvall Forsberg [53], which does not appear in our algebraic approach to typing, is the close relationship between adapters and bidirectional typing: adapters naturally mediate the phase change between inference and checking We expect that these aspects would surface in a future implementation of AdapTT and AdapTT₂.

## Data Availability Statement

The AGDA formalisation used to guide the rules' design by type-checking them is freely available on Zenodo [3].

## Acknowledgments

We would like to acknowledge and thank Théo Laurent who shared his insights from preliminary investigations on this topic. We thank Conor McBride and Fredrik Nordvall Forsberg for hosting a research visit that fueled our interest in adapters, Rafael Bocquet, Thiago Felicissimo, Josselin Poiret, András Kovács, Benedikt Ahrens, Niyousha Najmaei, Paige North and Niels van der Weide for very valuable discussions, and the anonymous reviewers for their insightful comments.
This work was supported in part by a European Research Council (ERC) Consolidator Grant for the project "TypeFoundry", funded under the European Union's Horizon 2020 Framework Programme (grant agreement no. 101002277).

## References

[1] Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. 2005. Containers: constructing strictly positive types. *Theor. Comput. Sci.*, 342, 1, 3–27. doi:10.1016/J.TCS.2005.06.002.

[2] Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, and Kenji Maillard. 2026. AdapTT: functoriality for dependent type casts. *Proc. ACM Program. Lang.*, 9, POPL, (Jan. 2026). doi:10.1145/3776664.

[3] [SW] Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, and Kenji Maillard, Formalisation of the rules presented in the article "AdapTT: Factoriality for Dependent Type Casts" 2025. doi:10.5281/zenodo.17348641.

[4] [n. d.] Agda's documentation on cumulativity. (). https://agda.readthedocs.io/en/latest/language/cumulativity.html.

[5] Benedikt Ahrens, Paige Randall North, and Niels van der Weide. 2023. Bicategorical type theory: semantics and syntax. *Math. Struct. Comput. Sci.*, 33, 10, 868–912. doi:10.1017/S0960129523000312.

[6] Guillaume Allais, Conor McBride, and Pierre Boutillier. 2013. New equations for neutral terms: a sound and complete decision procedure, formalized. In *Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-Typed Programming* (DTP '13). Association for Computing Machinery, Boston, Massachusetts, USA, 13–24. ISBN: 9781450323840. doi:10.1145/2502409.2502411.

[7] Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman. 2024. Internal parametricity, without an interval. *Proc. ACM Program. Lang.*, 8, POPL, Article 78, (Jan. 2024), 30 pages. doi:10.1145/3632920.

[8] Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. 2015. Indexed containers. *Journal of Functional Programming*, 25, e5.

[9] Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. 2007. Observational equality, now! In *Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification* (PLPV '07). Association for Computing Machinery, Freiburg, Germany, 57–68. ISBN: 9781595936776. doi:10.1145/1292597.1292608.

[10] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. 2023. Two-level type theory and applications. *Math. Struct. Comput. Sci.*, 33, 8, 688–743. doi:10.1017/S0960129523000130.

[11] Nathanael Arkor. A 2-dimensional perspective on polymorphism. Talk at the ICE-TCS seminar, (2022).

[12] Steve Awodey. 2018. Natural models of homotopy type theory. *Mathematical Structures in Computer Science*, 28, 2, 241–286. doi:10.1017/S0960129516000268.

[13] Steve Awodey. 2024. On hofmann-streicher universes. *Math. Struct. Comput. Sci.*, 34, 9, 894–910. doi:10.1017/S0960129524000203.

[14] Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. 2021. On generalized algebraic theories and categories with families. *Mathematical Structures in Computer Science*, 31, 9, 1006–1023. doi:10.1017/S0960129521000268.

[15] John Cartmell. 1986. Generalised algebraic theories and contextual categories. *Annals of Pure and Applied Logic*, 32, 209–243. doi:10.1016/0168-0072(86)90053-9.

[16] Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2017. Undecidability of equality in the free locally cartesian closed category (extended version). *Logical Methods in Computer Science*, 13.

[17] James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. 2010. The gentle art of levitation. In *Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming* (ICFP '10). ACM, Baltimore, Maryland, USA, 3–14. ISBN: 978-1-60558-794-3. doi:10.1145/1863543.1863547.

[18] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2015. Cubical Type Theory: a constructive interpretation of the univalence axiom. In *21st International Conference on Types for Proofs and Programs* (21st International Conference on Types for Proofs and Programs) number 69. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Tallinn, Estonia, (May 2015), 262. doi:10.4230/LIPIcs.TYPES.2015.5.

[19] Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2024. Trocq: proof transfer for free, with or without univalence. In *Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferencand Practice of Software, ETAPS 2024, Proceedings, Part I* (Lecture Notes in Computer Science). Stephanie Weirich, (Ed.) Vol. 14576. Springer, 239–268. doi:10.1007/978-3-031-57262-3_10.

[20] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. 2020. Hierarchy builder: algebraic hierarchies made easy in coq with elpi (system description). In *5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)* (LIPIcs). Zena M. Ariola, (Ed.) Vol. 167. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 34:1–34:21. ISBN: 978-3-95977-155-9. doi:10.4230/LIPICS.FSCD.2020.34.

[21] 1990. *Inductively defined types*. COLOG-88. Springer Berlin Heidelberg, 50–66. ISBN: 9783540469636. doi:10.1007/3-540-52335-9_47.
[22] Greta Coraglia and Jacopo Emmenegger. 2024. A 2-categorical analysis of context comprehension. *Theory and Applications of Categories*, 42, 41.

[23] Greta Coraglia and Jacopo Emmenegger. 2024. Categorical Models of Subtyping. In *29th International Conference on Types for Proofs and Programs (TYPES 2023)* (Leibniz International Proceedings in Informatics (LIPIcs)). Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg, (Eds.) Vol. 303. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 3:1–3:19. ISBN: 978-3-95977-332-4. doi:10.4230/LIPIcs.TYPES.2023.3.

[24] Greta Coraglia and Ivan Di Liberti. 2024. Context, judgement, deduction. (2024). arXiv: 2111.09438 [math.LO]. doi:10.48550/arXiv.2111.09438.

[25] Nicolaas Govert de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. *Indagationes Mathematicae (Proceedings)*, 75, 5, 381–392. doi:10.1016/1385-7258(72)90034-0.

[26] Lucas Escot and Jesper Cockx. 2022. Practical generic programming over a universe of native datatypes. *Proc. ACM Program. Lang.*, 6, ICFP, Article 113, (Aug. 2022), 25 pages. doi:10.1145/3547644.

[27] Lucas Escot, Josselin Poiret, Joris Ceulemans, Andreas Nuyts, and Malin Altenmüller. 2023. Read the mode and stay positive. In *29th International Conference on Types for Proofs and Programs*.

[28] Marcelo Fiore. Discrete generalised polynomial functors. Talk at ICALP 2012, (2012).

[29] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009. Packaging mathematical structures. In *Theorem Proving in Higher Order Logics*. Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, (Eds.) Springer Berlin Heidelberg, Berlin, Heidelberg, 327–342.

[30] Richard Garner. 2009. Two-dimensional models of type theory. *Math. Struct. Comput. Sci.*, 19, 4, 687–736. doi:10.1017/S0960129509007646.

[31] Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2021. Multimodal dependent type theory. *Log. Methods Comput. Sci.*, 17, 3. doi:10.46298/LMCS-17(3:11)2021.

[32] Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. 2025. The yoneda embedding in simplicial type theory. *CoRR*, abs/2501.13229. arXiv: 2501.13229. doi:10.48550/ARXIV.2501.13229.

[33] Martin Hofmann. 1997. *Extensional constructs in intensional type theory*. *CPHC/BCS distinguished dissertations*. Springer. ISBN: 978-3-540-76121-1.

[34] 1997. *Syntax and semantics of dependent types*. *Extensional Constructs in Intensional Type Theory*. Springer London, London, 13–54. ISBN: 978-1-4471-0963-1. doi:10.1007/978-1-4471-0963-1_2.

[35] Cătălin Hrițcu. 2014. Polarities: subtyping for datatypes. https://github.com/FStarLang/FStar/issues/65. Accessed: 2023-07-04. (2014).

[36] Bart Jacobs. 1993. Comprehension categories and the semantics of type dependency. *Theoretical Computer Science*, 107, 2, 169–207. doi:10.1016/0304-3975(93)090169-T.

[37] Bart P. F. Jacobs. 2001. *Categorical Logic and Type Theory*. *Studies in logic and the foundations of mathematics*. Vol. 141. North-Holland. ISBN: 978-0-444-50853-9. http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.

[38] Niles Johnson and Donald Yau. 2021. Categories. In *2-Dimensional Categories*. Oxford University Press, (Jan. 2021). ISBN: 9780198871378. eprint: https://academic.oup.com/book/0/chapter/367000442/chapter-pdf/45085865/oso-9780198871378-chapter-1.pdf. doi:10.1093/oso/9780198871378.003.0001.

[39] Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. 2019. Constructing quotient inductive-inductive types. *Proceeding of the ACM on Programming Languages*, 3, POPL, Article 2, (Jan. 2019), 24 pages. doi:10.1145/3290315.

[40] Ambrus Kaposi and Jakob von Raumer. 2020. A Syntax for Mutual Inductive Families. In *5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)* (Leibniz International Proceedings in Informatics (LIPIcs)). Zena M. Ariola, (Ed.) Vol. 167. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. ISBN: 978-3-95977-155-9. doi:10.4230/LIPIcs.FSCD.2020.23.

[41] Ambrus Kaposi and Szumi Xie. 2024. Second-order generalised algebraic theories: signatures and first-order semantics. In *9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia* (LIPIcs). Jakob Rehof, (Ed.) Vol. 299. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 10:1–10:24. ISBN: 978-3-95977-323-2. doi:10.4230/LIPICS.FSCD.2024.10.

[42] Gregory Maxwell Kelly. 1982. *Basic concepts of enriched category theory*. Vol. 64. CUP Archive.

[43] András Kovács. 2022. *Type-Theoretic Signatures for Algebraic Theories and Inductive Types*. Ph.D. Dissertation. Eötvös Loránd University. doi:10.15476/ELTE.2022.070.

[44] Théo Laurent. 2025. *Structural Subtyping in MLTT*. Theses. Université de montpellier, (Apr. 2025). https://theses.hal.sciences-tel-05144931.

[45] Théo Laurent, Meven Lennon-Bertrand, and Kenji Maillard. 2024. Definitional functoriality for dependent (sub)types. In *33rd European Symposium on Programming, ESOP 2024* (Lecture Notes in Computer Science). Stephanie Weirich, (Ed.) Vol. 14576. Springer, 302–331. doi:10.1007/978-3-031-57262-3_13.
[46] Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. 2022. Gradualizing the calculus of inductive constructions. *ACM Transactions on Programming Languages and Systems*, 44, 2, Article 7, (Apr. 2022), 82 pages. doi:10.1145/3495528.

[47] Daniel R. Licata and Robert Harper. 2011. 2-dimensional directed type theory. In *Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011* (Electronic Notes in Theoretical Computer Science). Michael W. Mislove and Joël Ouaknine, (Eds.) Vol. 276. Elsevier, 263–289. doi:10.1016/J.ENTCS.2011.09.026.

[48] Georgiana Elena Lungu and Zhaohui Luo. 2018. On Subtyping in Type Theories with Canonical Objects. In *22nd International Conference on Types for Proofs and Programs (TYPES 2016)* (Leibniz International Proceedings in Informatics (LIPIcs)). Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić, (Eds.) Vol. 97. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. ISBN: 978-3-95977-065-1. doi:10.4230/LIPIcs.TYPES.2016.13.

[49] Z. Luo. 1989. Ecc, an extended calculus of constructions. In *Fourth Annual Symposium on Logic in Computer Science*, 386–395. doi:10.1109/LICS.1989.39193.

[50] Zhaohui Luo. 1999. Coercive subtyping. *Journal of Logic and Computation*, 9, 1, (Feb. 1999), 105–130. eprint: https://academic.oup.com/logcom/article-pdf/9/1/105/2760838/090105.pdf. doi:10.1093/logcom/9.1.105.

[51] Zhaohui Luo and Robin Adams. 2008. Structural subtyping for inductive types with functorial equality rules. *Mathematical Structures in Computer Science*, 18, 5, 931–972. doi:10.1017/S0960129508006956.

[52] Per Martin-Löf and Giovanni Sambin. 1984. *Intuitionistic Type Theory*. Number 1 in *Studies in Proof Theory*. Napoli: Bibliopolis.

[53] Conor McBride and Frederik Nordvall Forsberg. 2021. Functorial adapters. In *27th International Conference on Types for Proofs and Programs*.

[54] Paul-André Melliès and Noam Zeilberger. 2015. Functors are type refinement systems. In *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages* (POPL '15). Association for Computing Machinery, Mumbai, India, 3–16. ISBN: 9781450333009. doi:10.1145/2676726.2676970.

[55] Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In *Automated Deduction – CADE 28*. André Platzer and Geoff Sutcliffe, (Eds.) Springer International Publishing, Cham, 625–635. ISBN: 978-3-030-79876-5. https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37.

[56] Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, and Paige Randall North. 2026. A type theory for comprehension categories with applications to subtyping. *Proc. ACM Program. Lang.*, 9, POPL, (Jan. 2026). doi:10.1145/3776725.

[57] Jacob Neumann and Thorsten Altenkirch. 2024. Synthetic 1-categories in directed type theory. In *30th International Conference on Types for Proofs and Programs, TYPES 2024, June 10-14, 2024, Copenhagen, Denmark* (LIPIcs). Rasmus Ejlers Møgelberg and Benno van den Berg, (Eds.) Vol. 336. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 7:1–7:23. ISBN: 978-3-95977-376-8. doi:10.4230/LIPICS.TYPES.2024.7.

[58] Paige Randall North. 2019. Towards a directed homotopy type theory. In *Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2019, London, UK, June 4-7, 2019* (Electronic Notes in Theoretical Computer Science). Barbara König, (Ed.) Vol. 347. Elsevier, 223–239. doi:10.1016/J.ENTCS.2019.09.012.

[59] Ian Orton and Andrew M. Pitts. 2018. Axioms for modelling cubical type theory in a topos. *Log. Methods Comput. Sci.*, 14, 4. doi:10.23638/LMCS-14(4:23)2018.

[60] Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: a prototype verification system. In *Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction (CADE-11)*. Springer-Verlag, Berlin, Heidelberg, 748–752. ISBN: 3540556028.

[61] C. Paulin-Mohring. 1993. Inductive Definitions in the System Coq - Rules and Properties. In *Proceedings of the conference Typed Lambda Calculi and Applications* (Lecture Notes in Computer Science) number 664. M. Bezem and J.-F. Groote, (Eds.) LIP research report 92-49.

[62] Pierre-Marie Pédrot and Nicolas Tabareau. 2018. Failure is not an option an exceptional type theory. In *ESOP 2018 - 27th European Symposium on Programming* (LNCS). Vol. 10801. Springer, Thessaloniki, Greece, 245–271. doi:10.1007/978-3-319-89884-1_9.

[63] Robert Pollack. 2000. Dependently typed records for representing mathematical structure. In *Theorem Proving in Higher Order Logics*. Mark Aagaard and John Harrison, (Eds.) Springer Berlin Heidelberg, Berlin, Heidelberg, 462–479.

[64] Loïc Pujet. 2022. *Computing with Extensionality Principles in Type Theory*. Ph.D. Dissertation. Nantes Université.

[65] Loïc Pujet, Yann Leray, and Nicolas Tabareau. 2025. Observational equality meets cic. *ACM Transactions on Programming Languages and Systems*, 47, 2, Article 6, (Apr. 2025), 35 pages. doi:10.1145/3719342.

[66] Loïc Pujet and Nicolas Tabareau. 2023. Impredicative observational equality. *Proc. ACM Program. Lang.*, 7, POPL, Article 74. (Jan. 2023), 26 pages. doi:10.1145/3571739.

[67] Loïc Pujet and Nicolas Tabareau. 2022. Observational equality: now for good. *Proc. ACM Program. Lang.*, 6, POPL, Article 32, 27 pages. doi:10.1145/3498693.
[68] Emily Riehl and Michael Shulman. 2017. A type theory for synthetic $\infty$-categories. *Higher Structures*, 1, 1, 147–224.

[69] Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid types. In *Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation* (PLDI '08). Association for Computing Machinery, Tucson, AZ, USA, 159–169. ISBN: 9781595938602. doi:10.1145/1375581.1375602.

[70] Amokrane Saïbi. 1997. Typing algorithm in type theory with inheritance. *Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '97*. doi:10.1145/263699.263742. doi:10.1145/263699.263742.

[71] Natarajan Shankar and Sam Owre. 2000. Principles and pragmatics of subtyping in PVS. In *Recent Trends in Algebraic Development Techniques*. Didier Bert, Christine Choppy, and Peter D. Mosses, (Eds.) Springer Berlin Heidelberg, Berlin, Heidelberg, 37–52. ISBN: 978-3-540-74464-1.

[72] Matthieu Sozeau. 2007. Subset coercions in coq. In *Types for Proofs and Programs*. Thorsten Altenkirch and Conor McBride, (Eds.) Springer Berlin Heidelberg, Berlin, Heidelberg, 237–252. ISBN: 978-3-540-74464-1.

[73] Matteo Spadetto. 2025. Higher dimensional semantics of axiomatic dependent type theory. Private communication, in preparation. (2025).

[74] Ross Street. 1974. Fibrations and yoneda's lemma in a 2-category. In *Category Seminar*. Gregory M. Kelly, (Ed.) Springer Berlin Heidelberg, Berlin, Heidelberg, 104–133. ISBN: 978-3-540-37270-7.

[75] Nikhil Swamy et al. 2016. Dependent types and multi-monadic effects in F. In *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016*, St. Petersburg, FL, USA, January 20 - 22, 2016. Rastislav Bodík and Rupak Majumdar, (Eds.) ACM, 256–270. ISBN: 978-1-4503-3549-2. doi:10.1145/2837614.2837655.

[76] Nikhil Swamy et al. 2016. Dependent types and multi-monadic effects in F*. In *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016*, St. Petersburg, FL, USA, January 20 - 22, 2016, 256–270. doi:10.1145/2837614.2837655.

[77] Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. 2018. Equivalences for Free: Univalent Parametricity for Effective Transport. *Proceedings of the ACM on Programming Languages*. ICFP'18 2, ICFP, (Sept. 2018), 1–29. doi:10.1145/3234615.

[78] [SW] The Rocq Development Team, The Rocq Prover version 9.0, Apr. 2025. doi:10.5281/zenodo.15149629, URL: https://doi.org/10.5281/zenodo.15149629.

[79] The Univalent Foundations Program. 2013. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study. https://homotopytypetheory.org/book.

[80] Taichi Uemura. 2021. *Abstract and Concrete Type Theories*. Ph.D. Dissertation. Institute for Logic, Language and Computation, University of Amsterdam. https://hdl.handle.net/11245.1/41ff0b60-64d4-4003-8182-c244a9afab3b.

[81] Matthew Z. Weaver and Daniel R. Licata. 2020. A constructive model of directed univalence in bicubical sets. In *LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020*. Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, (Eds.) ACM, 915–928. ISBN: 978-1-4503-7104-9. doi:10.1145/3373718.3394794.

[82] Mark Weber. 2007. Yoneda structures from 2-toposes. *Applied Categorical Structures*, 15, 3, 259–323. doi:10.1007/s10485-007-9079-2.

[83] Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. 2019. Eliminating reflection from type theory. In *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*. Assia Mahboubi and Magnus O. Myreen, (Eds.) ACM, 91–103. ISBN: 978-1-4503-6222-1. doi:10.1145/3293880.3294095.
<figure><img src="image_27.png" /><figcaption>Fig. 12. SOGAT definition of AdapTT</figcaption></figure>

## A Second order presentation of AdapTT

Figure 12 presents a definition of AdapTT using a second-order generalized algebraic theory (SOGAT) [80]. In this presentation, only the part of the context that is required to specify a judgment is implicitly given, all the sorts, operations and equations can be understood as parametrized by an implicit additional context. The presentation of Fig. 2 is derived from this presentation by the translation of a SOGAT into a generalized algebraic theory (GAT) [41].

The presentation of a bare category with families, which we extend, features a sort `Ty` classifying well-formed types, and a dependent sort `Tm A` classifying well-formed terms of type `A`: `Ty`. The sort `Tm A` of terms is flagged as a representable sort: the construction of the corresponding (first-order) generalized algebraic theory uses this information to construct explicit contexts populated with variables for representable sorts, here only `Tm`. This is enough to derive all structural rules of a `CwF`, including Rules `VARZERO`, `WK`, `SUBEXT` and their equations.

To this basic structure, we add `Ad AB`, the sort of adapters between the types `A` and `B`. The operation `id` provides the identity adapter, while `◦` composes two adapters with compatible target and source. Together with the equations `idl`, `idr` and `assoc`, these operations equip `Ty` with the structure of a category. Again, because this is a SOGAT, all these sorts operations are automatically stable under substitution in the derived GAT, i.e. Rules `SUBAD`, `SUBADID`, and `SUBADCOMP`.

Adapters `a`: `Ad AB` act on terms `t`: `Tm A` to obtain another term `t(a)`: `Tm B`. This action must respect identity adapters (`adapt/id`) and composition of adapters (`adapt/◦`), hence satisfying functional laws that make `Ty` a (Set-valued) functor on the category of types and adapters, thus an internal category to presheaves on `_Ctx` after the translation.

## B Correspondence between gCwFs and NatMod<sub>DOs</sub>

In this section, we show the correspondence between split gCwFs and NatMod<sub>DOs</sub>, corresponding to Section 2.3 and in particular Theorem 2.13.

### B.1 Categorical refresher

*2-categorical Yoneda.* We start by recalling the categorical material we need. First, recall the (2-categorical) Yoneda lemma [42]: given `A` in `Pst(C)`, for every object `c` of `C`, there is an isomorphism of categories `A(c)` ≅ `yc` → `A` between `A(c)` and the category of functors `yc` → `A`.

*Discrete opfibrations.* To assess the task at hand, we expand on Definition 2.2, in particular regarding the condition that `p` is a discrete opfibration. We recall that a functor `F`: `C` → `D` is a discrete opfibration if for every object `a` in `C` and any morphism `f'`: `F(a)` → `b'` in `D`, there exists a unique morphism `f`: `a` → `b` in `C` such that `F(f) = f'`, called the lift of `f'` at `a`. Given any
**LEMMA B.1.** With the same notations as above, the following equation holds

$$ \epsilon_B \circ \Sigma(\bar{\tau}_{t,a}) = \mathrm{id}_B $$

**PROOF.** First note that using the naturality of $\epsilon$, the triangle equation for adjunctions and the verticality of $a$ we have:

$$
\begin{align*}
u(\epsilon_B \circ \Sigma(\bar{\tau}_{t,a})) &= u(\epsilon_B) \circ \tau_{t,a} \\
&= u(\epsilon_B) \circ u(\Sigma(\Delta(a) \circ \eta_t)) \\
&= u(\epsilon_B \circ \Sigma\Delta(a) \circ \Sigma\eta_t) \\
&= u(a \circ \epsilon_{\Sigma(t)} \circ \Sigma\eta_t) \\
&= u(a) \\
&= \mathrm{id}_{u(B)}
\end{align*}
$$

Moreover, we note that the maps $\epsilon_B$ and $\bar{\tau}_{t,a}$ are cartesian, and $\Sigma$ preserves cartesian maps, hence $\epsilon_B \circ \Sigma(\bar{\tau}_{t,a})$ is cartesian. Being a cartesian map whose image is the identity, it is itself an identity by splitness of the fibration $u$. $\square$

We now prove a more precise version of Proposition 2.12.

**PROPOSITION B.2.** in a split gCwF, the functor $\Sigma$ induces a discrete opfibration of Cat-valued presheaves from $\dot{u}^{-1}$ to $u^{-1}$. Explicitly, considering an object $t$ of $\dot{U}$ and a vertical morphism $a: \Sigma(t) \to B$ in $\mathcal{U}$, there exists a unique object $t\langle a \rangle$ in $\dot{U}$ equipped with a vertical morphism $\tilde{a}: t \to t\langle a \rangle$ such that

$$ \Sigma(t\langle a \rangle) = B $$

$$ \Sigma(\tilde{a}) = a $$

This operation moreover satisfies the equation $t\langle a \rangle[\sigma] = t[\sigma]\langle a[\sigma] \rangle$.

**PROOF OF PROPOSITION B.2.** Considering an object $t$ of $\dot{U}$ and a vertical morphism $a: \Sigma(t) \to B$ in $\mathcal{U}$, we define $t\langle a \rangle = \Delta(B)[\tau_{t,a}]$ with the vertical morphism $\tilde{a}: t \to t\langle a \rangle$ given by the lifting property justified by the equation $\dot{u}(t\langle a \rangle) = \dot{u}(t)$, depicted below in the category $\dot{U}$:

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

It suffices to show that these satisfy the required equations. For the first equation, we note that since $\epsilon_B$ is cartesian, we have $\Sigma\Delta(B) = B[u(\epsilon_B)]$. Thus, using Lemma B.1, we have

$$ \Sigma(t\langle a \rangle) = \Sigma\Delta(B)[\Sigma\bar{\tau}_{t,a}] = B[\epsilon_B \circ \Sigma\bar{\tau}_{t,a}] = B $$

The second equation is given by the following commutative diagram, where the left square commutes by definition of $\tilde{a}$, the right square commutes by naturality, the top region commutes by the triangle equation, and the lower region commutes by Lemma B.1:

<figure><img src="image_29.png" /></figure>
We next prove uniqueness. Consider an object $t'$ and a vertical morphism $b : t \to t'$ such that $\Sigma t' = B$ and $\Sigma b = a$, we show that necessarily $b = \tilde{a}$. For this we consider the following naturality square

$$ \begin{array}{ccc} t & \xrightarrow{\eta_t} & \Delta\Sigma t \\ \multicolumn{1}{c}{b} & \searrow & \searrow \\ t' & \xrightarrow{\eta_{t'}} & \Delta\Sigma t' \end{array} $$

Taking the image by $\dot{u}$ of this naturality square yields by verticality of the morphism $b$,

$$ \dot{u}(\eta_{t'}) = \dot{u}(\tau_a) $$

Since $\eta_{t'}$ is cartesian it is its own chosen lift by assumption, we conclude that $\eta_{t'} = \overline{\tau_{t,a}}$, which proves that $t' = t\langle a \rangle$. Moreover, the morphism $b$ is a vertical morphism making the following diagram commute

$$ \begin{array}{ccc} t\langle a \rangle & \xrightarrow{\overline{\tau_{t,a}}} & \Delta(B) \\ \multicolumn{1}{c}{b} & \searrow & \searrow \\ t & \xrightarrow{\tau_{t,a}} & \end{array} $$

By uniqueness of such a morphism, we conclude that $b = \tilde{a}$.

Finally, we consider a morphism $\sigma: \Gamma' \to \Gamma$ and show the equation $t\langle a \rangle[\sigma] = t[\sigma]\langle a[\sigma] \rangle$. This is given by the following computation, where the second line is obtained by the fact that $\Delta$ preserves chosen lifts, the third line is given by definition of $a[\sigma]$, and the fourth line is given by naturality of $\eta$ and by the fact that $\Sigma$ preserves chosen lifts:

$$ \begin{align*} t[\sigma]\langle a[\sigma] \rangle &= \Delta(B[\sigma])[\tau_{t[\sigma],a[\sigma]}] \\ &= \Delta B[\Delta\sigma][\Delta(a[\sigma]) \circ \eta_{t[\sigma]}] \\ &= \Delta B[\Delta(a) \circ \Delta(\sigma) \circ \eta_{t[\sigma]}] \\ &= \Delta B[\tau_{t,a}][\sigma] \\ &= t\langle a \rangle[\sigma] \end{align*} $$

□

**THEOREM B.3.** *The category of split gCwFs and the category of NatMod<sub>DO</sub>s are equivalent.*

**PROOF.** Starting with a split gCwF, we define a NatMod<sub>DO</sub> by considering the presheaves of Ty and Tm to be given respectively by $u^{-1}$ and $\dot{u}^{-1}$. The morphism of fibrations $\Sigma$ then induces a natural transformation $p: Tm \to Ty$. By Proposition B.2, $p$ is a discrete opfibration. Moreover, the existence of $\Delta$ implies that $p$ is representable. Indeed, given an object $A$ in Ty(Γ), we define $\Gamma \triangleright A = \dot{u}(\Delta A)$, together with $\uparrow = \dot{u}(\epsilon_A)$ and $\theta^{\text{tm}}$ to be the element of $\dot{U}$ corresponding to $\Delta(A)$. Since $\epsilon_A$ is its own lift, $\Sigma(\theta^{\text{tm}}) = A[\uparrow]$ and so $\theta^{\text{tm}}$ is an object of Tm(Γ$\triangleright$A, A[\uparrow])$. Given a morphism $\sigma: \Gamma \to \Gamma'$ in $\mathcal{B}$, and objects $A: \text{Ty}(\Gamma')$ and $t: Tm(\Gamma, A[\sigma])$, we define the morphism $\sigma \triangleright t = \dot{u}(\Delta(\sigma) \circ \eta_t)$ where $\sigma: A[\sigma] \to A$ is the cartesian lift of $\sigma$ at $A$ through $u$. In order to check that these satisfy the adequate universal property, we verify the three following conditions:

(1) Given $\sigma: \Gamma \to \Gamma'$ with $A: \text{Ty}(\Gamma')$ and $t: Tm(\Gamma, A[\sigma])$, we have $\uparrow \circ (\sigma \triangleright t) = \sigma$. This is proven by the following computation using the naturality of $\epsilon$ and one triangle identity for
adjunctions

$$
\begin{align*}
\uparrow \circ (\sigma \triangleright t) &= u(\epsilon_{\Sigma\Delta\Sigma t}) \circ \dot{u}(\Delta(\bar{\sigma}) \circ \eta_t) \\
&= u(\epsilon_{\Sigma\Delta\Sigma t} \circ \Sigma\Delta(\bar{\sigma}) \circ \Sigma\eta_t) \\
&= u(\bar{\sigma} \circ \epsilon_{\Sigma t} \circ \Sigma\eta_t) \\
&= u(\bar{\sigma}) \\
&= \sigma
\end{align*}
$$

(2) Given $\sigma : \Gamma \to \Gamma'$ with $A : \mathrm{Ty}(\Gamma')$ and $t : \mathrm{Tm}(\Gamma, A[\sigma])$, we have $\theta^{\mathrm{tm}}[\sigma \triangleright t] = t$. This is given by the fact that since $\Delta$ preserves chosen lifts and $\eta_t$ is the chosen lift of its projection, by splitness of $\dot{u}$, the following morphism is the chosen lift of its projection

$$
\Delta(\bar{\sigma}) \circ \eta_t : t \to \theta^{\mathrm{tm}}
$$

(3) For $\sigma : \Gamma \to \Gamma' \triangleright A$, we have $\sigma = (\uparrow \circ \sigma) \triangleright \theta^{\text{tm}}[\sigma]$. To show this, we denote $\bar{\sigma} : \Delta(A)[\sigma] \to \Delta(A)$ the cartesian lift of $\sigma$ at $\Delta(A)$. Using the fact that $\epsilon_A$ is the chosen lift of its projection, as well as the naturality of $\eta$ and the other triangle identity for adjunction, we obtained the desired identity by the following computation:

$$
\begin{align*}
(\uparrow \circ \sigma) \triangleright \theta^{\text{tm}}[\sigma] &= \dot{u}(\Delta(\epsilon_A \circ \Sigma \bar{\sigma}) \circ \eta_{\Delta(A)}[\sigma]) \\
&= \dot{u}(\Delta \epsilon_A \circ \eta_{\Delta(A)} \circ \bar{\sigma}) \\
&= \dot{u}(\bar{\sigma}) \\
&= \bar{\sigma}
\end{align*}
$$

Conversely, starting with a NatMod<sub>DO</sub> Ctx, we define a split gCwF by letting *B* be Ctx, the split
fibration *u* : *u* → *B* to be the Grothendieck construction of the functor *Ty* : Ctx → **Cat** and the
split fibration *ú* : *ú* → **Cat** to be the Grothendieck construction of the functor *Tm* : Ctx → **Cat**.
The natural transformation *p* : **Tm** → *Ty* then induces a morphism of split fibrations Σ, which fits
into the following picture:

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

where both *u* and *ú* are split opfibrations and *Σ* is a morphism of fibration that preserves chosen lifts.
To complete the gCwF structure, it suffices to check that ∫<sub>Γ</sub> ty<sub>Γ</sub> has a right adjoint that preserves
chosen lifts, with unit and counit being componentwise the chosen lift of their projection. We
explicitly define the right adjoint

<figure><img src="image_31.png" /></figure>
Note that $\Delta$ sends $(\sigma, \mathrm{id})$ onto a pair whose second component is an identity, and hence it preserves chosen lifts. Moreover, we have natural transformations

$$ \eta_{\Gamma,t} : (\Gamma, t) \to (\Gamma \triangleright p_{\Gamma}(t), \theta^{\mathrm{tm}}) $$

$$ \eta_{\Gamma,t} = (\mathrm{id} \triangleright t, \mathrm{id}) $$

$$ \epsilon_{\Gamma,A} : (\Gamma \triangleright A, A[\uparrow]) \to (\Gamma, A) $$

$$ \epsilon_{\Gamma,A} = (\uparrow, \mathrm{id}) $$

Since the second component is always the identity, both these natural transformations are componentwise the chosen lift of their projection. In order to check the triangle identities it thus suffices to check their that they hold on the first components. The first triangle identity is given, for $t: \mathrm{Tm}(\Gamma)$ by the equation

$$ \uparrow_{\Gamma, p_{\Gamma}(t)} \circ (\mathrm{id}_{\Gamma} \triangleright t) = \mathrm{id}_{\Gamma} $$

The second equation is given, for $A: \mathrm{Ty}(\Gamma)$, by the following computation:

$$ \begin{align*} & ((\uparrow_{\Gamma,A} \circ \uparrow_{\Gamma \triangleright A,A[\uparrow]}) \triangleright \theta^{\mathrm{tm}}_{\Gamma \triangleright A,A[\uparrow]}) \circ (\mathrm{id}_{\Gamma,A} \triangleright \theta^{\mathrm{tm}}_{\Gamma,A}) \\ &= (\uparrow_{\Gamma,A} \circ \uparrow_{\Gamma \triangleright A,A[\uparrow]} \circ (\mathrm{id}_{\Gamma,A} \triangleright \theta^{\mathrm{tm}}_{\Gamma,A})) \triangleright \theta^{\mathrm{tm}}_{\Gamma \triangleright A,A[\uparrow]} [\mathrm{id}_{\Gamma,A} \triangleright \theta^{\mathrm{tm}}_{\Gamma,A}] \\ &= \uparrow_{\Gamma,A} \triangleright \theta^{\mathrm{tm}}_{\Gamma,A} \\ &= \mathrm{id}_{\Gamma \triangleright A} \end{align*} $$

These two functors define an equivalence of 2-categories, induced by the equivalence between split fibrations over Ctx and functors Ctx$^{\mathrm{op}} \to \mathrm{Cat}$ defined by the Grothendieck construction and the fiber. $\square$

## C Alternative presentation of AdapTT

In this section, we present an alternate description of the theory AdapTT, that was suggested by an anonymous reviewer. This version is a bit more verbose but gives insight regarding the required equality on term constructors. We present here the rules together with a description of their intended semantics, keeping in mind that it should have the same models as AdapTT, namely, NatMod$_{\mathrm{DO}}$. This presentation is obtained by removing all the equations that we impose on terms, and instead introducing an additional judgment:

$$ \frac{\Gamma \vdash a : A \quad \Gamma \vdash b : B \quad \Gamma \vdash f : A \Rightarrow B}{\Gamma \vdash e : a \equiv_f b} $$

The reader may think of this judgment as denoting $\Gamma \vdash a \langle f \rangle \equiv b : B$, as this is what we will force it to be. We write this judgment with explicit witnesses, even thought the discreteness condition we impose for the opfibration enforces that there is (definitionally) at most one inhabitant. Semantically, in the NatMod$_{\mathrm{DO}}$ structure, $\Gamma \vdash e : a \equiv_f b$ describes morphisms $e$ in $\mathrm{Tm}(\Gamma)$ whose image by $p$ is the morphism $f$ in the category $\mathrm{Ty}(\Gamma)$.

### C.1 Category structure

The following rules axiomatise the category structure of $\mathrm{Tm}(\Gamma)$, together with the functoriality of the map $p_{\Gamma}: \mathrm{Tm}(\Gamma) \to \mathrm{Ty}(\Gamma)$.

$$ \frac{\Gamma \vdash a : A}{\Gamma \vdash \mathrm{id} : A \equiv_{\mathrm{id}} A} $$

$$ \frac{\Gamma \vdash e : a \equiv_f b \quad \Gamma \vdash e' : b \equiv_g c}{\Gamma \vdash e' \circ e : a \equiv_{g \circ f} c} $$

$$ \frac{\Gamma \vdash e : a \equiv_f b}{\Gamma \vdash e \circ \mathrm{id} \equiv e : a \equiv_f b} $$

$$ \frac{\Gamma \vdash e : a \equiv_f b}{\Gamma \vdash \mathrm{id} \circ e \equiv e : a \equiv_f b} $$

$$ \frac{\Gamma \vdash e : a \equiv_f b \quad \Gamma \vdash e' : b \equiv_g c \quad \Gamma \vdash e'' : d \equiv_h c}{\Gamma \vdash e'' \circ (e' \circ e) \equiv (e'' \circ e') \circ e : a \equiv_{h \circ g \circ f} d} $$
## C.2 Action of substitutions

The following rules make the assignment $\Gamma \mapsto \mathrm{Tm}(\Gamma)$ functorial in $\Gamma$, at the level on morphisms, and ensure that the map $p$ is natural.

$$ \frac{\Gamma \vdash e : a \equiv_f b \quad \Delta \vdash \sigma : \Gamma}{\Gamma \vdash e[\sigma] : a[\sigma] \equiv_{f[\sigma]} b[\sigma]} \qquad \frac{\Gamma \vdash e : a \equiv_f b}{\Gamma \vdash e[id] \equiv e : a \equiv_f b} \\ \frac{\Gamma \vdash e : a \equiv_f b \quad \Delta \vdash \sigma : \Gamma \quad \Xi \vdash \tau : \Delta}{\Gamma \vdash e[\sigma \circ \tau] \equiv e[\sigma][\tau] : a[\sigma][\tau] \equiv_{f[\sigma][\tau]} b[\sigma][\tau]} $$

## C.3 Discrete opfibration structure

Finally, we add rules to axiomatize the discrete opfibration structure of the morphism $p$ as follows:

$$ \frac{\Gamma \vdash a : A \quad \Gamma \vdash f : A \Rightarrow B}{\Gamma \vdash e_f(a) : a \equiv_f a \langle f \rangle} \qquad \frac{\Gamma \vdash e : a \equiv_f b}{\Gamma \vdash a \langle f \rangle \equiv b} \qquad \frac{\Gamma \vdash e : a \equiv_f b}{\Gamma \vdash e \equiv e_f(a) : a \equiv_f b} $$

From these rules, it follows that there is at most one witness for the judgment $a \equiv_f b$ up to conversion: if $\Gamma \vdash e : a \equiv_f b$ and $\Gamma \vdash e' : a \equiv_f b$ then $\Gamma \vdash e \equiv e' : a \equiv_f b$. In particular, all the categorical equations introduced before are derivable.

This completes the alternate presentation of AdapTT. One can check that Rule ADAPTID and Rule ADAPTCOMP are derivable in this presentation. Conversely, the alternate presentation of AdapTT given here is derivable from the one given in the main text.

## C.4 Factoriality of term constructors

This presentation allows us to rewrite the equality that we require on term constructors in a different, perhaps more natural or systematic way. We illustrate this with the example of lists, for which we have required that adapters behave like generalized map functions as follows

$$ (h :: t) \langle \mathrm{List}(f) \rangle \equiv (h \langle f \rangle) :: (t \langle \mathrm{List}(f) \rangle) $$

The above constraint can be rephrased in the new formulation as a requirement for the term constructor to act on morphisms in $\mathrm{Tm}(\Gamma)$, as follows

$$ \frac{\Gamma \vdash e^h : h \equiv_f h' \quad \Gamma \vdash e^t : t \equiv_{\mathrm{List}(f)} t'}{\Gamma \vdash e^h :: e^t : h :: t \equiv_{\mathrm{List}(f)} h' :: t'} $$

We did not explore it further, but we believe there should be an alternate presentation of $\mathrm{AdapTT}_2$ that follows this style.

# D Full rules for $\mathrm{AdapTT}_2$

## D.1 All sorts and corresponding judgment forms

$$ \begin{array}{ccccccc} & & \Gamma, \Delta : \mathrm{Ctx} & & \Gamma : \mathrm{Ctx} & & \Gamma : \mathrm{Ctx} \\ \mathrm{Ctx} & \rightarrow & \mathrm{Sub}(\Gamma, \Delta) & \rightarrow & \sigma, \tau : \mathrm{Sub}(\Gamma, \Delta) & \rightarrow & \mathrm{A}, \mathrm{B} : \mathrm{Ty}(\Gamma) \\ & & \vdash & & \mathrm{Trans}(\Gamma, \Delta, \sigma, \tau) & \rightarrow & \mathrm{Ad}(\Gamma, \mathrm{A}, \mathrm{B}) \\ & & \vdash & & \Box & \rightarrow & \mathrm{Tm}(\Gamma, \mathrm{A}) \\ & & \vdash & & \Gamma \vdash \Box : \Delta & \rightarrow & \Gamma \vdash \Box : A \Rightarrow B \\ & & \vdash & & \Gamma \vdash \Box : \sigma \Rightarrow \Delta \tau & \rightarrow & \Gamma \vdash \Box : A \\ & & \vdash & & \Gamma : \mathrm{Ctx} & \rightarrow & \Gamma : \mathrm{Ctx} \\ & & \mathrm{Tel}(\Gamma) & & \mathrm{TelAd}(\Gamma, \Theta, \Theta') & \rightarrow & \mathrm{Inst}(\Gamma, \Theta) \end{array} $$
$$\Gamma \vdash \Box$$

$$\Gamma \vdash \Box : \Theta \Rightarrow \Theta'$$

$$\Gamma \vdash \Box : \Theta$$

## D.2 Basic structure of AdapTT₂

$$\text{SUBID} \quad \frac{\Gamma \vdash \Gamma}{\Gamma \vdash \text{id}_{\Gamma} : \Gamma}$$

$$\text{SUBCOMP} \quad \frac{\Delta \vdash \tau : \Xi \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash \tau \circ \sigma : \Xi}$$

$$\text{SUBRIGHTUNITALITY} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \sigma \circ \text{id}_{\Gamma} \equiv \sigma : \Delta}$$

$$\text{SUBLEFTUNITALITY} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \text{id}_{\Delta} \circ \sigma \equiv \sigma : \Delta}$$

$$\text{SUBASSOC} \quad \frac{\Phi \vdash \sigma : \Delta \quad \Xi \vdash \delta : \Phi \quad \Gamma \vdash \tau : \Xi}{\Gamma \vdash \sigma \circ (\delta \circ \tau) \equiv (\sigma \circ \delta) \circ \tau : \Delta}$$

$$\text{ADID} \quad \frac{\Gamma \vdash A}{\Gamma \vdash \text{id}_{A} : A \Rightarrow A}$$

$$\text{ADCOMP} \quad \frac{\Gamma \vdash g : B \Rightarrow C \quad \Gamma \vdash f : A \Rightarrow B}{\Gamma \vdash g \circ f : A \Rightarrow C}$$

$$\text{TRANSID} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \text{id}_{\sigma} : \sigma \Rightarrow \Delta \sigma}$$

$$\text{TRANSCOMP} \quad \frac{\Gamma \vdash \mu : \rho \Rightarrow \Delta \sigma \quad \Gamma \vdash \nu : \sigma \Rightarrow \Delta \tau}{\Gamma \vdash \nu \circ \mu : \rho \Rightarrow \Delta \tau}$$

$$\text{TRANSWHISKERLEFT} \quad \frac{\Delta \vdash \tau : \Xi \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \sigma'}{\Gamma \vdash \tau \circ \mu : (\tau \circ \sigma) \Rightarrow \Xi (\tau \circ \sigma')}$$

$$\text{TRANSWHISKERRIGHT} \quad \frac{\Delta \vdash \nu : \tau \Rightarrow \Xi \tau' \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash \nu \circ \sigma : (\tau \circ \sigma) \Rightarrow \Xi (\tau' \circ \sigma)}$$

$$\text{TRANSLEFTUNITALITY} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \sigma'}{\Gamma \vdash \mu \circ \text{id}_{\sigma} \equiv \mu : \sigma \Rightarrow \Delta \sigma'}$$

$$\text{TRANSRIGHTUNITALITY} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \sigma'}{\Gamma \vdash \text{id}_{\sigma'} \circ \mu \equiv \mu : \sigma \Rightarrow \Delta \sigma'}$$

$$\text{TRANSASSOC} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma \vdash \nu : \tau \Rightarrow \Delta \rho \quad \Gamma \vdash \xi : \rho \Rightarrow \Delta \psi}{\Gamma \vdash \xi \circ (\nu \circ \mu) \equiv (\xi \circ \nu) \circ \mu : \sigma \Rightarrow \Delta \psi}$$

$$\text{TRANSWHISKERLEFTRIGHTUNITALITY} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \tau : \Xi}{\Gamma \vdash \tau \circ \text{id}_{\sigma} \equiv \text{id}_{\tau \circ \sigma} : \tau \circ \sigma \Rightarrow \Xi \tau \circ \sigma}$$

$$\text{TRANSWHISKERRIGHTLEFTUNITALITY} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \tau : \Xi}{\Gamma \vdash \text{id}_{\tau} \circ \sigma \equiv \text{id}_{\tau \circ \sigma} : \tau \circ \sigma \Rightarrow \Xi \tau \circ \sigma}$$

$$\text{TRANSWHISKERLEFTLEFTUNITALITY} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \sigma'}{\Gamma \vdash \text{id}_{\Delta} \circ \mu \equiv \mu : \sigma \Rightarrow \Delta \sigma'}$$

$$\text{TRANSWHISKERRIGHTRIGHTUNITALITY} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \sigma'}{\Gamma \vdash \mu \circ \text{id}_{\Gamma} \equiv \mu : \sigma \Rightarrow \Delta \sigma}$$
$$ \text{TRANSWHISKERLEFTASSOC} \xrightarrow{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \sigma' \quad \Delta \vdash \tau : \Xi \quad \Xi \vdash \tau' : \Psi} \frac{\Gamma \vdash (\tau' \circ \tau) \circ \mu \equiv \tau' \circ (\tau \circ \mu) : (\tau' \circ \tau \circ \sigma) \Rightarrow \psi (\tau' \circ \tau \circ \sigma')}{\Gamma \vdash \mu \circ (\sigma' \circ \sigma) \equiv (\mu \circ \sigma') \circ \sigma : (\tau \circ \sigma' \circ \sigma) \Rightarrow \psi (\tau' \circ \sigma' \circ \sigma')} $$

$$ \text{TRANSWHISKERRIGHTASSOC} \xrightarrow{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \sigma' : \Xi \quad \Xi \vdash \mu : \tau \Rightarrow \psi \tau'} \frac{\Gamma \vdash \mu \circ (\sigma' \circ \sigma) \equiv (\mu \circ \sigma') \circ \sigma : (\tau \circ \sigma' \circ \sigma) \Rightarrow \psi (\tau' \circ \sigma' \circ \sigma')}{\Gamma \vdash \mu \circ (\sigma' \circ \sigma) \equiv (\mu \circ \sigma') \circ \sigma : (\tau \circ \sigma' \circ \sigma) \Rightarrow \psi (\tau' \circ \sigma' \circ \sigma')} $$

$$ \text{TRANSWHISKERLEFTDISTR} \xrightarrow{\Delta \vdash \sigma : \Xi \quad \Gamma \vdash \mu : \tau \Rightarrow_{\Delta} \tau' \quad \Gamma \vdash \nu : \tau' \Rightarrow_{\Delta} \tau''} \frac{\Gamma \vdash \sigma \circ (\mu \circ \nu) \equiv (\sigma \circ \mu) \circ (\sigma \circ \nu) : (\delta \circ \tau) \Rightarrow_{\Xi} (\delta \circ \tau'')}{\Gamma \vdash \mu \circ (\sigma' \circ \sigma) \equiv (\mu \circ \sigma') \circ \sigma : (\tau \circ \sigma' \circ \sigma) \Rightarrow \psi (\delta \circ \tau'')} $$

$$ \text{TRANSWHISKERRIGHTDISTR} \xrightarrow{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \mu : \tau \Rightarrow_{\Xi} \tau' \quad \Delta \vdash \nu : \tau' \Rightarrow_{\Xi} \tau''} \frac{\Gamma \vdash (\mu \circ \nu) \circ \sigma \equiv (\mu \circ \sigma) \circ (\nu \circ \sigma) : (\delta \circ \tau) \Rightarrow_{\Xi} (\delta \circ \tau'')}{\Gamma \vdash (\mu \circ \nu) \circ \sigma \equiv (\mu \circ \sigma) \circ (\nu \circ \sigma) : (\delta \circ \tau) \Rightarrow \psi (\delta \circ \tau'')} $$

$$ \text{ADRIGHTUNITALITY} \xrightarrow{\Gamma \vdash a : A \Rightarrow B} \frac{\Gamma \vdash a \circ \text{id}_A \equiv a : A \Rightarrow B}{\Gamma \vdash a \circ \text{id}_A \equiv a : A \Rightarrow B} $$

$$ \text{ADLEFTUNITALITY} \xrightarrow{\Gamma \vdash a : A \Rightarrow B} \frac{\Gamma \vdash \text{id}_B \circ a \equiv a : A \Rightarrow B}{\Gamma \vdash \text{id}_B \circ a \equiv a : A \Rightarrow B} $$

$$ \text{ADASSOC} \xrightarrow{\Gamma \vdash a : A \Rightarrow B \quad \Gamma \vdash b : B \Rightarrow C \quad \Gamma \vdash c : C \Rightarrow D} \frac{\Gamma \vdash c \circ (b \circ a) \equiv (c \circ b) \circ a : A \Rightarrow D}{\Gamma \vdash c \circ (b \circ a) \equiv (c \circ b) \circ a : A \Rightarrow D} $$

$$ \text{ADTM} \xrightarrow{\Gamma \vdash f : A \Rightarrow B \quad \Gamma \vdash t : A} \frac{\Gamma \vdash t \langle f \rangle : B}{\Gamma \vdash t \langle f \rangle : B} $$

$$ \text{SUBTY} \xrightarrow{\Delta \vdash A \quad \Gamma \vdash \sigma : \Delta} \frac{\Gamma \vdash A[\sigma]}{\Gamma \vdash A[\sigma]} $$

$$ \text{SUBTYID} \xrightarrow{\Gamma \vdash A} \frac{\Gamma \vdash A[\text{id}_\Gamma] \equiv A}{\Gamma \vdash A[\text{id}_\Gamma] \equiv A} \quad \text{SUBTYCOMP} \xrightarrow{\Gamma \vdash A \quad \Xi \vdash \sigma : \Gamma \quad \Delta \vdash \tau : \Xi} \frac{\Delta \vdash A[\sigma \circ \tau] \equiv A[\sigma][\tau]}{\Delta \vdash A[\sigma \circ \tau] \equiv A[\sigma][\tau]} $$

$$ \text{SUBAD} \xrightarrow{\Delta \vdash f : A \Rightarrow B \quad \Gamma \vdash \sigma : \Delta} \frac{\Gamma \vdash f[\sigma] : A[\sigma] \Rightarrow B[\sigma]}{\Gamma \vdash f[\sigma] : A[\sigma] \Rightarrow B[\sigma]} $$

$$ \text{SUBADID} \xrightarrow{\Gamma \vdash a : A \Rightarrow B} \frac{\Gamma \vdash a[\text{id}_\Gamma] \equiv a : A \Rightarrow B}{\Gamma \vdash a[\text{id}_\Gamma] \equiv a : A \Rightarrow B} $$

$$ \text{SUBADCOMP} \xrightarrow{\Gamma \vdash a : A \Rightarrow B \quad \Xi \vdash \sigma : \Gamma \quad \Delta \vdash \tau : \Xi} \frac{\Delta \vdash a[\sigma \circ \tau] \equiv a[\sigma][\tau] : A[\sigma \circ \tau] \Rightarrow B[\sigma \circ \tau]}{\Delta \vdash a[\sigma \circ \tau] \equiv a[\sigma][\tau] : A[\sigma \circ \tau] \Rightarrow B[\sigma \circ \tau]} $$

$$ \text{SUBADONID} \xrightarrow{\Delta \vdash A \quad \Gamma \vdash \sigma : \Delta} \frac{\Gamma \vdash \text{id}_A[\sigma] \equiv \text{id}_A[\sigma] : A[\sigma] \Rightarrow A[\sigma]}{\Gamma \vdash \text{id}_A[\sigma] \equiv \text{id}_A[\sigma] : A[\sigma] \Rightarrow A[\sigma]} $$

$$ \text{SUBADONCOMP} \xrightarrow{\Delta \vdash a : A \Rightarrow B \quad \Delta \vdash b : B \Rightarrow C \quad \Gamma \vdash \sigma : \Delta} \frac{\Gamma \vdash (b \circ a)[\sigma] \equiv (b[\sigma]) \circ (a[\sigma]) : A[\sigma] \Rightarrow C[\sigma]}{\Gamma \vdash (b \circ a)[\sigma] \equiv (b[\sigma]) \circ (a[\sigma]) : A[\sigma] \Rightarrow C[\sigma]} $$

$$ \text{SUBTM} \xrightarrow{\Delta \vdash t : A \quad \Gamma \vdash \sigma : \Delta} \frac{\Gamma \vdash t[\sigma] : A[\sigma]}{\Gamma \vdash t[\sigma] : A[\sigma]} $$

$$ \text{SUBTMID} \xrightarrow{\Gamma \vdash t : A} \frac{\Gamma \vdash t[\text{id}_\Gamma] \equiv t : A}{\Gamma \vdash t[\text{id}_\Gamma] \equiv t : A} \quad \text{SUBTMCOMP} \xrightarrow{\Delta \vdash t : A \quad \Xi \vdash \sigma : \Gamma \quad \Delta \vdash \tau : \Xi} \frac{\Delta \vdash t[\sigma \circ \tau] \equiv t[\sigma][\tau] : A[\sigma \circ \tau]}{\Delta \vdash t[\sigma \circ \tau] \equiv t[\sigma][\tau] : A[\sigma \circ \tau]} $$

$$ \text{ADTMID} \xrightarrow{\Gamma \vdash t : A} \frac{\Gamma \vdash t[\text{id}_A] \equiv t : A}{\Gamma \vdash t[\text{id}_A] \equiv t : A} $$
$$ \begin{array}{l} \text{ADTMCOMP} \\ \frac{\Gamma \vdash t : A \quad \Gamma \vdash a : B \Rightarrow C \quad \Gamma \vdash b : A \Rightarrow B}{\Gamma \vdash t \langle a \circ b \rangle \equiv t \langle b \rangle \langle a \rangle : C} \end{array} $$

$$ \text{SUBTMONADTM} \quad \frac{\Delta \vdash t : A \quad \Delta \vdash a : A \Rightarrow B \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash t \langle a \rangle [\sigma] \equiv t [\sigma] \langle a [\sigma] \rangle : B [\sigma]} $$

$$ \text{TRANS\textsc{ty}} \quad \frac{\Delta \vdash A \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash A[\mu] : A[\sigma] \Rightarrow A[\tau]} \qquad \text{TRANS\textsc{tyid}} \quad \frac{\Delta \vdash A \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash A[\mathrm{id}_{\sigma}] \equiv \mathrm{id}_{A[\sigma]} : A[\sigma] \Rightarrow A[\sigma]} $$

$$ \text{TRANS\textsc{tycomp}} \quad \frac{\Delta \vdash A \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Gamma \vdash \nu : \tau \Rightarrow_{\Delta} \xi}{\Gamma \vdash A[\nu \circ \mu] \equiv A[\nu] \circ A[\mu] : A[\sigma] \Rightarrow A[\xi]} $$

$$ \text{SUB\textsc{tyon}\textsc{trans\textsc{ty}}} \quad \frac{\Xi \vdash A \quad \Delta \vdash \mu : \sigma \Rightarrow_{\Xi} \tau \quad \Gamma \vdash \delta : \Delta}{\Gamma \vdash A[\mu][\delta] \equiv A[\mu \circ \delta] : A[\sigma \circ \delta] \Rightarrow A[\tau \circ \delta]} $$

$$ \text{TRANS\textsc{tyon}\textsc{sub\textsc{ty}}} \quad \frac{\Xi \vdash A \quad \Delta \vdash \xi : \Xi \quad \Gamma \vdash \nu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash A[\xi][\nu] \equiv A[\xi \circ \nu] : A[\xi \circ \sigma] \Rightarrow A[\xi \circ \tau]} $$

$$ \text{TRANS\textsc{ty}\textsc{natura}} \quad \frac{\Delta \vdash f : A \Rightarrow B \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash B[\mu] \circ f[\sigma] \equiv f[\tau] \circ A[\mu] : A[\sigma] \Rightarrow B[\tau]} $$

$$ \text{TRANS\textsc{ty}\textsc{ad\textsc{tm}}} \quad \frac{\Delta \vdash t : A \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash t[\sigma] \langle A[\mu] \rangle \equiv t[\tau] : A[\tau]} $$

### D.3 Empty context and context dualisation

$$ \text{CTXEMP} \quad \frac{\vdash}{\vdash \diamond} \qquad \text{SUBEMP} \quad \frac{\vdash \Gamma}{\Gamma \vdash \diamond \Gamma : \diamond} \qquad \text{SUBEMPEXT} \quad \frac{\Gamma \vdash \sigma : \diamond}{\Gamma \vdash \sigma \equiv \diamond \Gamma : \diamond} \qquad \text{CTXDUAL} \quad \frac{\vdash \Gamma}{\vdash \Gamma^{-}} $$

$$ \text{SUBDUAL} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma^{-} \vdash \sigma^{-} : \Delta^{-}} \qquad \text{TRANSDUAL} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma^{-} \vdash \mu^{-} : \tau^{-} \Rightarrow_{\Delta^{-}} \sigma^{-}} \qquad \text{CTXEMPDUAL} \quad \frac{\vdash \diamond^{-} \equiv \diamond}{\vdash \Gamma^{-}} $$

$$ \text{SUBIDDUAL} \quad \frac{\vdash \Gamma}{\Gamma^{-} \vdash \mathrm{id}_{\Gamma}^{-} \equiv \mathrm{id}_{\Gamma^{-}} : \Gamma^{-}} \qquad \text{SUBCOMPDUAL} \quad \frac{\Delta \vdash \tau : \Xi \quad \Gamma \vdash \sigma : \Delta}{\Gamma^{-} \vdash (\tau \circ \sigma)^{-} \equiv \tau^{-} \circ \sigma^{-} : \Xi^{-}} $$

$$ \text{TRANS\textsc{id\textsc{dual}}} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma^{-} \vdash \mathrm{id}_{\sigma}^{-} \equiv \mathrm{id}_{\sigma^{-}} : \sigma^{-} \Rightarrow_{\Delta^{-}} \sigma^{-}} $$

$$ \text{TRANS\textsc{comp\textsc{dual}}} \quad \frac{\Gamma \vdash \mu : \rho \Rightarrow_{\Delta} \sigma \quad \Gamma \vdash \nu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma^{-} \vdash (\mu \circ \nu)^{-} \equiv \nu^{-} \circ \mu^{-} : \tau^{-} \Rightarrow_{\Delta^{-}} \rho^{-}} \qquad \text{CTXPLUS} \quad \frac{\vdash \Gamma}{\vdash \Gamma^{+} \equiv \Gamma} $$

$$ \text{SUBPLUS} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \sigma^{+} \equiv \sigma : \Delta} \qquad \text{TRANSPLUS} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash \mu^{+} \equiv \mu : \sigma \Rightarrow_{\Delta} \tau} \qquad \text{CTXDOUBLEDUAL} \quad \frac{\vdash \Gamma}{\vdash \Gamma^{-} \equiv \Gamma} $$
$$ \text{SUBDOUBLEDUAL} \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \sigma^{--} \equiv \sigma : \Delta} $$

$$ \text{TRANSDOUBLEDUAL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash \mu^{--} \equiv \mu : \sigma \Rightarrow_{\Delta} \tau} $$

$$ \text{TRANSWHISKERLEFTDUAL} \frac{\Delta \vdash \tau : \Xi \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \sigma'}{\Gamma \vdash (\tau \circ \mu)^{-} \equiv \tau^{-} \circ \mu^{-} : \tau \circ \sigma \Rightarrow \Xi \tau \circ \sigma'} $$

$$ \text{TRANSWHISKERRIGHTDUAL} \frac{\Delta \vdash \nu : \tau \Rightarrow \Xi \tau' \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash (\nu \circ \sigma)^{-} \equiv \nu^{-} \circ \sigma^{-} : \tau \circ \sigma \Rightarrow \Xi \tau' \circ \sigma} $$

### D.4 Term variables in AdapTT₂

$$ \text{CTXEXTTM} \frac{\Gamma \vdash \Gamma \quad \Gamma^d \vdash A}{\Gamma \vdash \Gamma_{\triangleright d} A} \quad (\text{d: Dir}) $$

$$ \text{SUBEXTTM} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^d \vdash A \quad \Gamma^d \vdash t : A[\sigma^d]}{\Gamma \vdash \sigma \triangleright_d t : \Delta \triangleright_d A} \quad (\text{d: Dir}) $$

$$ \text{WKTM} \frac{\Gamma^d \vdash A}{\Gamma \triangleright_d A \quad A \vdash \uparrow_A : \Gamma} \quad (\text{d: Dir}) $$

$$ \text{VARZTM} \frac{\Gamma \vdash A}{\Gamma \triangleright_+ A \quad \Gamma \vdash \theta_A^{\text{tm}} : A[\uparrow]} $$

$$ \text{SUBTL} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^d \vdash A \quad \Gamma \vdash t : A[\sigma^d]}{\Gamma \vdash \uparrow \circ (\sigma \triangleright_d t) \equiv \sigma : \Delta} \quad (\text{d: Dir}) $$

$$ \text{SUBETA} \frac{\Delta \vdash A \quad \Gamma \vdash \sigma : \Delta \triangleright A}{\Gamma \vdash (\uparrow \circ \sigma) \triangleright_d \theta_A^{\text{tm}}[\sigma] \equiv \sigma : \Delta} $$

$$ \text{ADTMVARZ} \frac{\Delta \vdash A \quad \Gamma \vdash \sigma : \Delta \triangleright A \quad \Gamma \vdash \tau : \Delta \triangleright A \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta \triangleright_+ A} \tau}{\Gamma \vdash \theta_A^{\text{tm}}[\sigma] \langle A[\uparrow \circ \mu] \rangle \equiv \theta_A^{\text{tm}}[\tau] : A[\tau]} $$

$$ \text{SUBTMEXTVARZ} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash A \quad \Gamma \vdash t : A[\sigma]}{\Gamma \vdash \theta_A^{\text{tm}}[\sigma \triangleright t] \equiv t : A[\sigma]} $$

$$ \text{TRANSSTM+} \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Gamma \vdash t : A[\sigma]}{\Gamma \vdash \mu \triangleright_+ t : \sigma \triangleright_+ t \Rightarrow \tau \triangleright_+ t \langle A[\mu] \rangle} $$

$$ \text{TRANSSTM-} \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Gamma \vdash t : A[\tau^{-}]}{\Gamma \vdash \mu \triangleright_{-} t : \sigma \triangleright_{-} t \langle A[\mu^{-}] \rangle \Rightarrow \tau \triangleright_{-} t} $$

$$ \text{TRANSTL+} \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Gamma \vdash t : A[\sigma]}{\Gamma \vdash \uparrow \circ (\mu \triangleright_+ t) \equiv \mu : \sigma \Rightarrow_{\Delta} \tau} $$

$$ \text{TRANSTL-} \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Gamma \vdash t : A[\tau^{-}]}{\Gamma \vdash \uparrow \circ (\mu \triangleright_{-} t) \equiv \mu : \sigma \Rightarrow_{\Delta} \tau} $$

$$ \text{TRANSETA} \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta \triangleright_+ A} \tau}{\Gamma \vdash \mu \equiv (\uparrow \circ \mu) \triangleright_+ \theta^{\text{tm}}[\sigma] : \sigma \Rightarrow_{\Delta \triangleright_+ A} \tau} $$

$$ \text{CTXEXTTMDUAL} \frac{\Gamma \vdash \Gamma \quad \Gamma^d \vdash A}{\Gamma \vdash (\Gamma \triangleright_d A)^{-} \equiv \Gamma^{-} \triangleright_{-d} A} \quad (\text{d: Dir}) $$

$$ \text{WKTMDUAL} \frac{\Gamma \vdash \Gamma^d \vdash A}{(\Gamma \triangleright_d A)^{-} \vdash \uparrow^{-} \equiv \uparrow : \Gamma^{-}} \quad (\text{d: Dir}) $$

$$ \text{SUBEXTTMDUAL} \frac{\Gamma \vdash \sigma : \Delta \quad \Gamma^d \vdash A \quad \Gamma \vdash t : A[\sigma^d]}{\Gamma^{-} \vdash (\sigma \triangleright_d t)^{-} \equiv \sigma^{-} \triangleright_{-d} t : (\Delta \triangleright_d A)^{-}} \quad (\text{d: Dir}) $$
$$ \text{TRANSM+DUAL} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Delta \vdash A \quad \Gamma \vdash t : A[\sigma]}{\Gamma \vdash (\mu \triangleright_+ t)^- \equiv \mu^- \triangleright_- t : \tau^- \triangleright t \langle A[\mu^-] \rangle \Rightarrow_{\Delta \triangleright A} \sigma^- \triangleright t} $$

$$ \text{TRANSM-DUAL} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Delta^- \vdash A \quad \Gamma^- \vdash t : A[\tau^-]}{\Gamma^- \vdash (\mu \triangleright_- t)^- \equiv \mu^- \triangleright_+ t : \tau^- \triangleright_- t \Rightarrow_{\Delta \triangleright_- A} \sigma^- \triangleright_- t \langle A[\mu^-] \rangle} $$

$$ \text{TYTRANSSUB} \quad \frac{\Delta \vdash A \quad \Gamma \vdash \mu : \tau \Rightarrow_{\Delta} \xi \quad \Xi \vdash \sigma : \Gamma}{\Xi \vdash A[\mu^-][\sigma] \equiv A[\mu^- \circ \sigma] : A[\tau \circ \sigma] \Rightarrow A[\xi \circ \sigma]} $$

$$ \text{TYSUBTRANS} \quad \frac{\Delta \vdash A \quad \Gamma \vdash \sigma : \Delta \quad \Xi \vdash \mu : \tau \Rightarrow_{\Gamma} \xi}{\Xi \vdash A[\sigma][\mu^-] \equiv A[\sigma^- \circ \mu^-] : A[\sigma^- \circ \tau] \Rightarrow A[\sigma^- \circ \xi]} $$

## D.5 Telescopes

$$ \text{CTXEXTTEL} \quad \frac{\Gamma \vdash \Gamma^d \vdash \Theta}{\Gamma \vdash \Gamma \triangleright_d \Theta} \quad (\text{d: Dir}) \quad \text{TELEMP} \quad \frac{\Gamma \vdash \Gamma}{\Gamma \vdash \diamond} \quad \text{TELEXTTY} \quad \frac{\Gamma \vdash \Gamma \vdash \Theta \quad \Gamma \triangleright_+ \Theta \vdash A}{\Gamma \vdash \Theta \triangleright A} $$

$$ \text{WKTEL} \quad \frac{\Gamma \vdash \Gamma \quad \Gamma^d \vdash \Theta}{\Gamma \triangleright_d \Theta \vdash \uparrow_{\Theta} : \Gamma} \quad (\text{d: Dir}) $$

$$ \text{SUBTEL} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \Theta}{\Gamma \vdash \Theta[\sigma]} $$

$$ \text{TRANSTEL} \quad \frac{\Delta \vdash \Theta \quad \Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau}{\Gamma \vdash \Theta[\mu^-] : \Theta[\sigma] \Rightarrow \Theta[\tau]} $$

$$ \text{ADINST} \quad \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta_2 \quad \Gamma \vdash l : \Theta_1}{\Gamma \vdash l(a) : \Theta_2} $$

$$ \text{VARINST} \quad \frac{\Gamma \vdash \Gamma \quad \Gamma \vdash \Theta}{\Gamma \triangleright_+ \Theta \vdash \text{vinst} : \Theta[\uparrow_{\Theta}]} \quad \text{SUBEXTINST} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^d \vdash \Theta \quad \Gamma^d \vdash l : \Theta[\sigma^d]}{\Gamma \vdash \sigma \triangleright_d l : \Delta \triangleright_d \Theta} \quad (\text{d: Dir}) $$

$$ \text{TRANSEXT+INST} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Delta \vdash \Theta \quad \Gamma \vdash l : \Theta[\sigma]}{\Gamma \vdash \mu \triangleright_+ l : \sigma \triangleright l \Rightarrow \tau \triangleright l \langle \Theta[\mu^-] \rangle} $$

$$ \text{TRANSEXT-INST} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow_{\Delta} \tau \quad \Delta^- \vdash \Theta \quad \Gamma^- \vdash l : \Theta[\tau^-]}{\Gamma \vdash \mu \triangleright_- l : \sigma \triangleright_- l \langle \Theta[\mu^-] \rangle \Rightarrow \tau \triangleright l} $$

$$ \text{SUBTELID} \quad \frac{\Gamma \vdash \Theta}{\Gamma \vdash \Theta[\text{id}_\Gamma] \equiv A} $$

$$ \text{SUBTELCOMP} \quad \frac{\Gamma \vdash \Theta \quad \Xi \vdash \sigma : \Gamma \quad \Delta \vdash \tau : \Xi}{\Delta \vdash \Theta[\sigma \circ \tau] \equiv \Theta[\sigma][\tau]} $$

$$ \text{SUBTELONEMP} \quad \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \diamond[\sigma] \equiv \diamond} $$

$$ \text{SUBTELONEXT} \quad \frac{\Delta \vdash \Theta \quad \Delta \triangleright \Theta \vdash A \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash (\Theta \triangleright A)[\sigma] \equiv \Theta[\sigma] \triangleright A[(\sigma \circ \uparrow) \triangleright \text{vinst}_\Theta]} \quad \text{SUBINST} \quad \frac{\Delta \vdash l : \Theta \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash l[\sigma] : \Theta[\sigma]} $$
$$ \text{SUBINSTID} \frac{\Gamma \vdash \iota : \Theta}{\Gamma \vdash \iota [\text{id}_\Gamma] \equiv \iota : \Theta} \qquad \text{SUBINSTCOMP} \frac{\Gamma \vdash \iota : \Theta \quad \Xi \vdash \sigma : \Gamma \quad \Delta \vdash \tau : \Xi}{\Delta \vdash \iota [\sigma \circ \tau] \equiv \iota [\sigma][\tau] : \Theta[\sigma \circ \tau]} $$

$$ \text{TELADID} \frac{\Gamma \vdash \Theta}{\Gamma \vdash \text{id}_\Theta : \Theta \Rightarrow \Theta} \qquad \text{TELADCOMP} \frac{\Gamma \vdash g : \Theta_2 \Rightarrow \Theta_3 \quad \Gamma \vdash f : \Theta_1 \Rightarrow \Theta_2}{\Gamma \vdash g \circ f : \Theta_1 \Rightarrow \Theta_3} $$

$$ \text{SUBTELAD} \frac{\Delta \vdash f : \Theta_1 \Rightarrow \Theta_2 \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash f[\sigma] : \Theta_1[\sigma] \Rightarrow \Theta_2[\sigma]} \qquad \text{TELADRIGHTUNITALITY} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta_2}{\Gamma \vdash a \circ \text{id}_{\Theta_1} \equiv a : \Theta_1 \Rightarrow \Theta_2} $$

$$ \text{TELADLEFTUNITALITY} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta_2}{\Gamma \vdash \text{id}_{\Theta_2} \circ a \equiv a : \Theta_1 \Rightarrow \Theta_2} $$

$$ \text{TELADASSOCIATIVITY} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta_2 \quad \Gamma \vdash b : \Theta_2 \Rightarrow \Theta_3 \quad \Gamma \vdash c : \Theta_3 \Rightarrow \Theta_4}{\Gamma \vdash c \circ (b \circ a) \equiv (c \circ b) \circ a : \Theta_1 \Rightarrow \Theta_4} $$

$$ \text{SUBTELADID} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta_2}{\Gamma \vdash a[\text{id}_\Gamma] \equiv a : \Theta_1 \Rightarrow \Theta_2} \qquad \text{SUBTELADCOMP} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta_2 \quad \Xi \vdash \sigma : \Gamma \quad \Delta \vdash \tau : \Xi}{\Delta \vdash a[\sigma \circ \tau] \equiv a[\sigma][\tau] : \Theta_1[\sigma \circ \tau] \Rightarrow \Theta_2[\sigma \circ \tau]} $$

$$ \text{SUBTELADONID} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash \text{id}_\Theta[\sigma] \equiv \text{id}_\Theta[\sigma] : \Theta[\sigma] \Rightarrow \Theta[\sigma]} $$

$$ \text{SUBTELADONCOMP} \frac{\Gamma \vdash a : \Theta_2 \Rightarrow \Theta_3 \quad \Gamma \vdash b : \Theta_1 \Rightarrow \Theta_2 \quad \Gamma \vdash \sigma : \Delta}{\Delta \vdash (a \circ b)[\sigma] \equiv (a[\sigma]) \circ (b[\sigma]) : \Theta_1[\sigma] \Rightarrow \Theta_3[\sigma]} $$

$$ \text{TRANSTELNATURALITY} \frac{\Delta \vdash a : \Theta_1 \Rightarrow \Theta_2 \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau}{\Gamma \vdash \Theta_2[[\mu]] \circ a[\sigma] \equiv a[\tau] \circ \Theta_1[[\mu]] : \Theta_1[\sigma] \Rightarrow \Theta_2[\tau]} $$

$$ \text{TRANSTELID} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash \Theta[[\text{id}_\sigma]] \equiv \text{id}_\Theta[\sigma] : A[\sigma] \Rightarrow A[\sigma]} $$

$$ \text{SUBTELADTRANSTEL} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Xi \vdash \xi : \Gamma}{\Gamma \vdash \Theta[[\mu]][[\xi]] \equiv \Theta[[\mu \circ \xi]] : \Theta[\sigma \circ \xi] \Rightarrow \Theta[\tau \circ \xi]} $$

$$ \text{TRANSTELCOMP} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma \vdash \nu : \tau \Rightarrow \Delta \xi}{\Gamma \vdash \Theta[[\nu \circ \mu]] \equiv \Theta[[\nu]] \circ \Theta[[\mu]] : \Theta[\sigma] \Rightarrow \Theta[\xi]} $$

$$ \text{TRANSTELSUBTEL} \frac{\Delta \vdash \Theta \quad \Xi \vdash \sigma : \Delta \quad \Gamma \vdash \nu : \tau \Rightarrow \Xi \xi}{\Gamma \vdash \Theta[\sigma][\nu] \equiv \Theta[[\sigma \circ \nu]] : \Theta[\sigma \circ \tau] \Rightarrow \Theta[\sigma \circ \xi]} $$

$$ \text{INSTTRANSTEL} \frac{\Delta \vdash \iota : \Theta_1 \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau}{\Gamma \vdash \iota[\sigma] \langle \Theta_1[[\mu]] \rangle \equiv \iota[\tau] : \Theta_1[\tau]} \qquad \text{ADINSTID} \frac{\Gamma \vdash \iota : \Theta}{\Gamma \vdash \iota[\text{id}_\Theta] \equiv \iota : \Theta} $$
$$ \text{ADINSTCOMP} \frac{\Gamma \vdash \iota : \Theta_1 \quad \Gamma \vdash a : \Theta_2 \Rightarrow \Theta_3 \quad \Gamma \vdash b : \Theta_1 \Rightarrow \Theta_2}{\Gamma \vdash \iota \langle a \circ b \rangle \equiv \iota \langle b \rangle \langle a \rangle : \Theta_3} $$

$$ \text{SUBINSTONADINST} \frac{\Delta \vdash \iota : \Theta_1 \quad \Delta \vdash a : \Theta_1 \Rightarrow \Theta_2 \quad \Gamma \vdash \sigma : \Delta}{\Gamma \vdash \iota \langle a \rangle [\sigma] \equiv \iota [\sigma] \langle a[\sigma] \rangle : \Theta_2[\sigma]} $$

$$ \text{CTXEXTTELDUAL} \frac{\Gamma^d \vdash \Theta}{\vdash (\Gamma \triangleright_d \Theta)^- \equiv \Gamma^- \triangleright_{-d} \Theta} $$

$$ \text{SUBEXTINSTDUAL} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^d \vdash \Gamma \quad \Gamma^d \vdash}{\Gamma^- \vdash (\sigma \triangleright_d \iota)^- \equiv \iota^- \triangleright_{-d} \iota : \Delta \triangleright_d \Theta^-} \quad \text{WKTELDUAL} \frac{\Gamma^d \vdash \Theta}{\Gamma \triangleright_d \Theta^- \vdash \uparrow^- \equiv \uparrow : \Gamma^-} $$

$$ \text{VARINSTADTRANS} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \sigma : \Delta \triangleright \Theta \quad \Gamma \vdash \tau : \Delta \triangleright \Theta \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \triangleright_+ \Theta \tau}{\Gamma \vdash \text{vinst}_{\Theta}[\sigma] \langle \Theta \llbracket \uparrow \circ \mu \rrbracket \rangle \equiv \text{vinst}_{\Theta}[\tau] : \Theta[\tau]} $$

$$ \text{INSTEMP} \frac{\Gamma \vdash \Gamma}{\Gamma \vdash \diamond : \diamond} \quad \text{INSTEXTTM} \frac{\Gamma \vdash \Theta \quad \Gamma \vdash \iota : \Theta \quad \Gamma \triangleright \Theta \vdash T \quad \Gamma \vdash t : T[\text{id} \triangleright \iota]}{\Gamma \vdash \iota \triangleright t : \Theta \triangleright T} $$

$$ \text{INSTTELEMP} \frac{\Gamma \vdash \iota : \diamond}{\Gamma \vdash \iota \equiv \diamond : \diamond} \qquad \text{SUBONINSTEMP} \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \diamond[\sigma] \equiv \diamond : \diamond} $$

$$ \text{SUBEXTINSTTL} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^d \vdash \Theta \quad \Gamma \vdash \iota : \Theta[\sigma^d]}{\Gamma \vdash \uparrow \circ (\sigma \triangleright_d \iota) \equiv \sigma : \Delta} \quad (d: \text{Dir}) $$

$$ \text{SUBEXTINSTETA} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \sigma : \Delta \triangleright \Theta}{\Gamma \vdash (\uparrow \circ \sigma) \triangleright_d \text{vinst}_{\Theta}[\sigma] \equiv \sigma : \Delta} $$

$$ \text{SUBINSTEXTVARINST} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \Theta \quad \Gamma \vdash \iota : \Theta[\sigma]}{\Gamma \vdash \text{vinst}_{\Theta}[\sigma \triangleright \iota] \equiv \iota : \Theta[\sigma]} \qquad \text{CTXEXTTELEMP} \frac{\Gamma \vdash \Gamma}{\Gamma \vdash \Gamma \triangleright_d \diamond \equiv \Gamma} $$

$$ \text{CTXEXTTELEXT} \frac{\Gamma^d \vdash \Theta \quad \Gamma^d \triangleright \Theta \vdash A}{\vdash \Gamma \triangleright_d (\Theta \triangleright A) \equiv (\Gamma \triangleright_d \Theta) \triangleright A} \quad \text{WKTELWKTY} \frac{\Gamma^d \vdash \Theta \quad \Gamma^d \triangleright_+ \Theta \vdash A}{\Gamma \triangleright_d \Theta \triangleright_+ A \vdash \uparrow \circ \uparrow_A \equiv \uparrow_{\Theta \triangleright A} : \Gamma} \quad (d: \text{Dir}) $$

$$ \text{VARINSTEXTVARZ} \frac{\Gamma^d \vdash \Theta \quad \Gamma^d \triangleright_+ \Theta \vdash A}{\Gamma \triangleright_d (\Theta \triangleright A) \vdash \text{vinst}_{\Theta \triangleright A} \equiv \text{vinst}_{\Theta}[\uparrow] \triangleright \theta^{\text{tm}} : \Theta \triangleright A} \quad (d: \text{Dir}) $$

$$ \text{SUBTELAD} \frac{\Gamma \vdash \sigma : \Delta \quad \Gamma^d \vdash \Theta \quad \Delta^d \vdash \Theta' \quad \Gamma^d \vdash \alpha : \Theta \Rightarrow \Theta'[\sigma^d]}{\Gamma \triangleright_d \Theta \vdash \sigma \triangleright_d \alpha \equiv ((\sigma^d \circ \uparrow) \triangleright \text{vinst}\langle \alpha[\uparrow] \rangle)^d : \Delta \triangleright_d \Theta'} \quad (d: \text{Dir}) $$

$$ \text{SUBEXTINSTEMP} \frac{\Gamma \vdash \sigma : \Delta}{\Gamma \vdash \sigma \triangleright_d \diamond \equiv \sigma : \Delta} \quad (d: \text{Dir}) $$
$$ \text{SUBEXTINSTEXT} \frac{\Gamma \vdash \sigma : \Delta \quad \Delta \vdash \Theta \quad \Gamma \vdash \iota : \Theta[\sigma] \quad \Delta \triangleright \Theta \vdash A \quad \Gamma \vdash t : A[\sigma \triangleright \iota]}{\Gamma \vdash \sigma \triangleright_d (\iota \triangleright t) \equiv (\sigma \triangleright \iota) \triangleright t : \Delta \triangleright \Theta \triangleright A} \quad (d: \text{Dir}) $$

$$ \text{TELADEXT} \frac{\Gamma \vdash \alpha : \Theta \Rightarrow \Theta' \quad \Gamma \triangleright \Theta \vdash f : A \Rightarrow A'[\text{id} \triangleright \alpha]}{\Gamma \vdash \alpha \triangleright f : \Theta \triangleright A \Rightarrow \Theta' \triangleright A'} $$

$$ \text{TELADEXTID} \frac{\Gamma \vdash \Theta \quad \Gamma \triangleright \Theta \vdash A}{\Gamma \vdash \text{id}_{\Theta} \triangleright \text{id}_{A} \equiv \text{id}_{\Theta \triangleright A} : \Theta \triangleright A \Rightarrow \Theta \triangleright A} $$

$$ \text{TELADEXTCOMP} \frac{\Gamma \vdash \alpha : \Theta \Rightarrow \Theta' \quad \Gamma \vdash \beta : \Theta' \Rightarrow \Theta'' \quad \Gamma \triangleright \Theta \vdash f : A \Rightarrow A'[\text{id} \triangleright \alpha] \quad \Gamma \triangleright \Theta' \vdash g : A' \Rightarrow A''[\text{id} \triangleright \beta]}{\Gamma \vdash (\beta \triangleright b) \circ (\alpha \triangleright a) \equiv (\beta \circ \alpha) \triangleright (b[\text{id} \triangleright \alpha] \circ A) : \Theta \triangleright A \Rightarrow \Theta'' \triangleright A''} $$

$$ \text{TRANSINST+} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma \vdash \iota : \Theta[\sigma]}{\Gamma \vdash \mu \triangleright \iota : \sigma \triangleright \iota \Rightarrow \tau \triangleright \iota \langle \Theta[\mu] \rangle} \qquad \text{TRANSINST-} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma^{-} \vdash \iota : \Theta[\tau^{-}]}{\Gamma \vdash \mu \triangleright_{-} \iota : \sigma \triangleright_{-} \iota \langle A[\mu^{-}] \rangle \Rightarrow \tau \triangleright_{-} t} $$

$$ \text{TRANSINST+TL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma \vdash \iota : \Theta[\sigma]}{\Gamma \vdash \uparrow \circ (\mu \triangleright_+ \iota) \equiv \mu : \sigma \Rightarrow \tau} \qquad \text{TRANSINST-TL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma^{-} \vdash \iota : A[\tau^{-}]}{\Gamma \vdash \uparrow \circ (\mu \triangleright_{-} \iota) \equiv \mu : \sigma \Rightarrow \tau} $$

$$ \text{TRANSINSTETA} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \triangleright_+ \Theta \tau}{\Gamma \vdash \mu \equiv (\uparrow \circ \mu) \triangleright_+ \text{vinst}[\sigma] : \sigma \Rightarrow \tau} $$

$$ \text{TRANSINST+DUAL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma \vdash \iota : \Theta[\sigma]}{\Gamma \vdash (\mu \triangleright_+ \iota)^{-} \equiv \mu^{-} \triangleright_{-} \iota : \tau^{-} \triangleright \iota \langle A[\mu] \rangle \Rightarrow \Delta \triangleright \Theta \sigma^{-} \triangleright \iota} $$

$$ \text{TRANSINST-DUAL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Gamma^{-} \vdash \iota : \Theta[\tau^{-}]}{\Gamma^{-} \vdash (\mu \triangleright_{-} \iota)^{-} \equiv \mu^{-} \triangleright_{+} \iota : \tau^{-} \triangleright_{-} \iota \Rightarrow \Delta \triangleright \Theta \sigma^{-} \triangleright_{-} \iota \langle \Theta[\mu^{-}] \rangle} $$

$$ \text{TELEXTTEL} \frac{\Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2}{\Gamma \vdash \Theta_1 \triangleright \Theta_2} $$

$$ \text{INSTEXTINST} \frac{\Gamma \vdash \iota_1 : \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2 \quad \Gamma \vdash \iota_2 : \Theta_2[\text{id}_{\Gamma \triangleright_+ \iota_1}]}{\Gamma \vdash \iota_1 \triangleright \iota_2 : \Theta_1 \triangleright \Theta_2} $$

$$ \text{CTXEXTTELEXTTEL} \frac{\Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2}{\vdash \Gamma \triangleright_+ (\Theta_1 \triangleright \Theta_2) \equiv (\Gamma \triangleright_+ \Theta_1) \triangleright \Theta_2} \qquad \text{TELEXTTELEMP} \frac{\Gamma \vdash \Theta}{\Gamma \vdash \Theta \triangleright \diamond \equiv \Theta} $$

$$ \text{TELEXTTELEXTTY} \frac{\Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2 \quad (\Gamma \triangleright_+ \Theta_1) \triangleright \Theta_2 \vdash A}{\Gamma \vdash \Theta_1 \triangleright (\Theta_2 \triangleright A) \equiv (\Theta_1 \triangleright \Theta_2) \triangleright A} $$

$$ \text{TELEXTTELEXTTEL} \frac{\Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2 \quad (\Gamma \triangleright_+ \Theta_1) \triangleright \Theta_2 \vdash \Theta_3}{\Gamma \vdash \Theta_1 \triangleright (\Theta_2 \triangleright \Theta_3) \equiv (\Theta_1 \triangleright \Theta_2) \triangleright \Theta_3} $$
$$ \text{SUBTELONEXTTEL} \frac{\Delta \vdash \sigma : \Gamma \quad \Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2}{\Delta \vdash (\Theta_1 \triangleright \Theta_2)[\sigma] \equiv \Theta_1[\sigma] \triangleright \Theta_2[\sigma \triangleq \text{id}_{\Theta_1[\sigma]}]} $$

$$ \text{WKTELWKTEL} \frac{\Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2}{(\Gamma \triangleright_+ \Theta_1) \triangleright_+ \Theta_2 \vdash \uparrow_{\Gamma, \Theta_1} \circ \uparrow_{\Gamma \triangleright_+ \Theta_1, \Theta_2} \equiv \uparrow_{\Gamma, \Theta_1 \triangleright \Theta_2} : \Gamma} $$

$$ \text{SUBEXTINSTEXTINST} \frac{\Delta \vdash \Theta_1 \quad \Gamma \vdash \iota_1 : \Theta_1[\sigma] \quad \Delta \triangleright_+ \Theta_1 \vdash \Theta_2 \quad \Gamma \vdash \iota_2 : \Theta_2[\Theta_1 \triangleright_+ \iota_1]}{\Gamma \vdash \sigma \triangleright_+ (\iota_1 \triangleright \iota_2) \equiv (\sigma \triangleright \iota_1) \triangleright \iota_2 : \Delta \triangleright_+ (\Theta_1 \triangleright \Theta_2)} $$

$$ \text{TELADEXTTELAD} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta'_1 \quad \Gamma \triangleright \Theta_1 \vdash \Theta_2 \quad \Gamma \triangleright \Theta'_1 \vdash \Theta'_2 \quad \Gamma \triangleright_+ \Theta_1 \vdash b : \Theta_2 \Rightarrow \Theta'_2[\text{id} \triangleq a]}{\Gamma \vdash a \triangleright b : \Theta_1 \triangleright \Theta_2 \Rightarrow \Theta'_1 \triangleright \Theta'_2} $$

$$ \text{TELADEXTTELADEMP} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta'_1}{\Gamma \vdash a \triangleright \diamond \equiv a : \Theta_1 \Rightarrow \Theta'_1} $$

$$ \text{SUBTELADONEXTAD} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta'_1 \quad \Gamma \triangleright \Theta_1 \vdash A \quad \Gamma \triangleright \Theta'_1 \vdash A' \quad \Gamma \triangleright_+ \Theta_1 \vdash b : A \Rightarrow A'[\text{id} \triangleq a] \quad \Delta \vdash \sigma : \Gamma}{\Gamma \vdash (a \triangleright b)[\sigma] \equiv a[\sigma] \triangleright b[(\sigma \circ \uparrow) \triangleright \text{vinst}] : \Theta_1[\sigma] \triangleright A[(\sigma \circ \uparrow) \triangleright \text{vinst}] \Rightarrow \Theta'_1[\sigma] \triangleright A'[[(\sigma \circ \uparrow) \triangleright \text{vinst}]} $$

$$ \text{SUBTELADONEXTAD} \frac{\Gamma \vdash a : \Theta_1 \Rightarrow \Theta'_1 \quad \Gamma \triangleright \Theta_1 \vdash \Theta_2 \quad \Gamma \triangleright \Theta'_1 \vdash \Theta'_2 \quad \Gamma \triangleright_+ \Theta_1 \vdash b : \Theta_2 \Rightarrow \Theta'_2[\text{id} \triangleq a] \quad \Delta \vdash \sigma : \Gamma}{\Gamma \vdash (a \triangleright b)[\sigma] \equiv a[\sigma] \triangleright b[(\sigma \circ \uparrow) \triangleright \text{vinst}] : \Theta_1[\sigma] \triangleright \Theta_2[(\sigma \circ \uparrow) \triangleright \text{vinst}] \Rightarrow \Theta'_1[\sigma] \triangleright \Theta'_2[(\sigma \circ \uparrow) \triangleright \text{vinst}]} $$

$$ \text{TELTRANSUB} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \mu : \tau \Rightarrow \Delta \xi \quad \Xi \vdash \sigma : \Gamma}{\Xi \vdash \Theta[\mu][\sigma] \equiv \Theta[\mu \circ \sigma] : \Theta[\tau \circ \sigma] \Rightarrow \Theta[\xi \circ \sigma]} $$

$$ \text{TELSUBTRANS} \frac{\Delta \vdash \Theta \quad \Gamma \vdash \sigma : \Delta \quad \Xi \vdash \mu : \tau \Rightarrow \Gamma \xi}{\Xi \vdash \Theta[\sigma][\mu] \equiv \Theta[\sigma \circ \mu] : \Theta[\sigma \circ \tau] \Rightarrow \Theta[\sigma \circ \xi]} $$

$$ \text{VARINSTTELEXTTY} \frac{\Gamma \vdash \Theta \quad \Gamma \triangleright_+ \Theta \vdash A}{\Gamma \triangleright_+ (\Theta \triangleright A) \vdash \text{vinst}_{\Theta \triangleright A} \equiv \text{vinst}_{\Theta}[\uparrow] \triangleright \theta^{\text{tm}} : (\Theta \triangleright A)[\uparrow]} $$

$$ \text{VARINSTTELEXTTEL} \frac{\Gamma \vdash \Theta_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2}{\Gamma \triangleright_+ (\Theta_1 \triangleright \Theta_2) \vdash \text{vinst}_{\Theta_1 \triangleright \Theta_2} \equiv \text{vinst}_{\Theta_1}[\uparrow] \triangleright \text{vinst}_{\Theta_2} : (\Theta_1 \triangleright \Theta_2)[\uparrow]} $$
$$ \Gamma \vdash a_1 : \Theta_1 \Rightarrow \Theta'_1 \quad \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2 \quad \Gamma \triangleright_+ \Theta'_1 \vdash \Theta'_2 \\ \Gamma \triangleright_+ \Theta_1 \vdash a_2 : \Theta_2 \Rightarrow \Theta'_2 [\text{id} \blacktriangleright a_1] \quad \Gamma \triangleright_+ (\Theta_1 \triangleright \Theta_2) \vdash A \\ \text{TELAD}\text{EXT}\text{TELAD}\text{EXT}\text{TELAD} \frac{\Gamma \triangleright_+ (\Theta'_1 \triangleright \Theta'_2) \vdash A' \quad \Gamma \triangleright_+ (\Theta_1 \triangleright \Theta_2) \vdash a : A \Rightarrow A' [\text{id} \blacktriangleright (a_1 \triangleright a_2)]}{\Gamma \vdash (a_1 \triangleright a_2) \triangleright a \equiv a_1 \triangleright (a_2 \triangleright a) : \Theta_1 \triangleright \Theta_2 \triangleright A \Rightarrow \Theta'_1 \triangleright \Theta'_2 \triangleright A'} $$

$$ \Gamma \vdash a_1 : \Theta_1 \Rightarrow \Theta'_1 \\ \Gamma \triangleright_+ \Theta_1 \vdash \Theta_2 \quad \Gamma \triangleright_+ \Theta'_1 \vdash \Theta'_2 \quad \Gamma \triangleright_+ \Theta_1 \vdash a_2 : \Theta_2 \Rightarrow \Theta'_2 [\text{id} \blacktriangleright a_1] \\ \Gamma \triangleright_+ (\Theta_1 \triangleright \Theta_2) \vdash \Theta_3 \quad \Gamma \triangleright_+ (\Theta'_1 \triangleright \Theta'_2) \vdash \Theta'_3 \\ \text{TELAD}\text{EXT}\text{TELAD}\text{EXT}\text{TELAD} \frac{\Gamma \triangleright_+ (\Theta_1 \triangleright \Theta_2) \vdash a_3 : \Theta_3 \Rightarrow \Theta'_3 [\text{id} \blacktriangleright (a_1 \triangleright a_2)]}{\Gamma \vdash (a_1 \triangleright a_2) \triangleright a_3 \equiv a_1 \triangleright (a_2 \triangleright a_3) : \Theta_1 \triangleright \Theta_2 \triangleright \Theta_3 \Rightarrow \Theta'_1 \triangleright \Theta'_2 \triangleright \Theta'_3} $$

## D.6 Type variables

$$ \text{CTXTY} \quad \frac{\vdash \Gamma \quad \Gamma^{d'} \vdash \Theta}{\vdash \Gamma \triangleright d' (\Theta.Ty_d)} \quad (d, d': \text{Dir}) \quad \text{SUBTY} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^{d'} \vdash \Theta \quad (\Gamma \triangleright d' \Theta[\sigma^{d'}])^d \vdash A}{\Gamma \vdash \sigma \triangleright_d A : \Delta \triangleright d' (\Theta.Ty_d)} \quad (d, d': \text{Dir}) $$

$$ \text{TRANSAD}^{++} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau}{\Gamma \vdash \mu \triangleright f : \sigma \triangleright f \quad A \Rightarrow \Delta \triangleright_+(\Theta.Ty_+) \tau \triangleright B} $$

$$ \text{TRANSAD}^{+-} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta \vdash \Theta}{(\Gamma \triangleright_+ \Theta[\sigma])^{-} \vdash A \quad (\Gamma \triangleright_+ \Theta[\tau])^{-} \vdash B \quad (\Gamma \triangleright_+ \Theta[\sigma])^{-} \vdash f : B[\text{id}_\Gamma \triangleright_+ \Theta[\mu]] \Rightarrow A} \quad \Gamma \vdash \mu \triangleright f : \sigma \triangleright f \quad A \Rightarrow \Delta \triangleright_+(\Theta.Ty_-) \tau \triangleright B $$

$$ \text{TRANSAD}^{+-} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta^{-} \vdash \Theta}{\Gamma \triangleright_{-} \Theta[\sigma^{-}] \vdash A \quad \Gamma \triangleright_{-} \Theta[\tau^{-}] \vdash B \quad \Gamma \triangleright_{-} \Theta[\tau^{-}] \vdash f : A[\text{id}_\Gamma \triangleright_{-} \Theta[\mu^{-}]] \Rightarrow B} \quad \Gamma \vdash \mu \triangleright f : \sigma \triangleright f \quad A \Rightarrow \Delta \triangleright_{-}(\Theta.Ty_+) \tau \triangleright B $$

$$ \Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta^{-} \vdash \Theta \quad (\Gamma \triangleright_{-} \Theta[\sigma^{-}])^{-} \vdash A \\ \text{TRANSAD}^{--} \quad \frac{(\Gamma \triangleright_{-} \Theta[\tau^{-}])^{-} \vdash B \quad (\Gamma \triangleright_{-} \Theta[\tau^{-}])^{-} \vdash f : B \Rightarrow A[(\text{id}_\Gamma \triangleright_{-} \Theta[\mu^{-}])^d]}{\Gamma \vdash \mu \triangleright f : \sigma \triangleright f \quad A \Rightarrow \Delta \triangleright_{-}(\Theta.Ty_-) \tau \triangleright B} $$

$$ \text{WKTY} \quad \frac{\vdash \Gamma \quad \Gamma^{d'} \vdash \Theta}{\Gamma \triangleright d' (\Theta.Ty_d) \vdash \uparrow : \Gamma} \quad (d, d': \text{Dir}) \quad \text{VARZTY} \quad \frac{\vdash \Gamma \quad \Gamma^d \vdash \Theta}{\Gamma \triangleright_d (\Theta.Ty_+) \triangleright_d \Theta[\uparrow^d] \vdash \emptyset^\text{ty}} \quad (d : \text{Dir}) $$

$$ \text{CTXTYDUAL} \quad \frac{\Gamma^{d'} \vdash \Theta}{\vdash (\Gamma \triangleright_{d'} \Theta.Ty_d)^{-} \equiv \Gamma^{-} \triangleright_{-d'} \Theta.Ty_{-d}} \quad (d, d': \text{Dir}) $$

$$ \text{WKTYDUAL} \quad \frac{\Gamma^{d'} \vdash \Theta}{(\Gamma \triangleright_{d'} \Theta.Ty_d)^{-} \vdash \uparrow^{-} \equiv \uparrow : \Gamma^{-}} \quad (d, d': \text{Dir}) $$
$$ \text{SUBTyDUAL} \frac{\Gamma \vdash \sigma : \Delta \ \Delta^{d'} \vdash \Theta \ (\Gamma \triangleright_{d'} \Theta[\sigma^{d'}])^d \vdash A}{\Gamma \vdash (\sigma \triangleright_d A)^- \equiv \sigma^- \triangleright_{-d} A : (\Delta \triangleright_{d'} \Theta.Ty_d)^-} \quad (d, d': \text{Dir}) $$

$$ \text{TRANSAD++DUAL} \frac{\Gamma \triangleright \mu : \sigma \Rightarrow \Delta \tau \quad \Delta \vdash \Theta}{\Gamma \triangleright_+ \Theta[\sigma] \vdash A \quad \Gamma \triangleright_+ \Theta[\tau] \vdash B \quad \Gamma \triangleright_+ \Theta[\sigma] \vdash a : A \Rightarrow B[\text{id} \triangleright \Theta[\mu]]} \quad \Gamma^- \vdash (\mu \triangleright_+ a)^- \equiv \mu^- \triangleright_- a : (\tau \triangleright_- B)^- \Rightarrow (\Delta \triangleright_+ \Theta.Ty_d)^- (\sigma \triangleright_- A)^- $$

$$ \text{TRANSAD+-DUAL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta \vdash \Theta \ (\Gamma \triangleright_+ \Theta[\sigma])^- \vdash A}{(\Gamma \triangleright_+ \Theta[\tau])^- \vdash B \quad (\Gamma \triangleright_+ \Theta[\sigma])^- \vdash a : B[(\text{id} \triangleright \Theta[\mu])^-]} \Rightarrow A \quad \Gamma^- \vdash (\mu \triangleright_- a)^- \equiv \mu^- \triangleright_+ a : (\tau \triangleright_+ B)^- \Rightarrow (\Delta \triangleright_+ \Theta.Ty_d)^- (\sigma \triangleright_- A)^- $$

$$ \text{TRANSAD+DUAL} \frac{\Gamma \triangleright \mu : \sigma \Rightarrow \Delta \tau \quad \Delta^- \vdash \Theta}{\Gamma \triangleright_- \Theta[\sigma^-] \vdash A \quad \Gamma \triangleright_- \Theta[\tau^-] \vdash B \quad \Gamma \triangleright_- \Theta[\sigma^-] \vdash a : A[\text{id} \triangleright \Theta[\mu^-]]} \Rightarrow B \quad \Gamma^- \vdash (\mu \triangleright_+ a)^- \equiv \mu^- \triangleright_- a : (\tau \triangleright_+ B)^- \Rightarrow (\Delta \triangleright_- \Theta.Ty_d)^- (\sigma \triangleright_+ A)^- $$

$$ \text{TRANSAD-DUAL} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta^- \vdash \Theta \ (\Gamma \triangleright_- \Theta[\sigma^-])^- \vdash A}{(\Gamma \triangleright_- \Theta[\tau^-])^- \vdash B \quad (\Gamma \triangleright_- \Theta[\sigma^-])^- \vdash a : B \Rightarrow A[(\text{id} \triangleright \Theta[\mu^-])^-]} \quad \Gamma^- \vdash (\mu \triangleright_- a)^- \equiv \mu^- \triangleright_+ a : (\tau \triangleright_- B)^- \Rightarrow (\Delta \triangleright_- \Theta.Ty_d)^- (\sigma \triangleright_- A)^- $$

$$ \text{SUBTLY} \frac{\Gamma \vdash \sigma : \Delta \ \Delta^{d'} \vdash \Theta \ (\Gamma \triangleright_{d'} \Theta[\sigma^{d'}])^d \vdash A}{\Gamma \vdash \uparrow \circ (\sigma \triangleright_d A) \equiv \sigma : \Delta} \quad (d, d': \text{Dir}) $$

$$ \text{SUBTyEXTVARZ} \frac{\Gamma \vdash \sigma : \Delta \ \Delta^d \vdash \Theta \ \Gamma \triangleright_d \Theta[\sigma^d] \vdash A \quad \Gamma^d \vdash \iota : \Theta[\sigma^d]}{\Gamma \vdash \Theta^{\text{ty}}[\sigma \triangleright_+ A \triangleright_d \iota] \equiv A[\text{id}_\Gamma \triangleright \iota]} \quad (d: \text{Dir}) $$

$$ \text{SUBETYTY} \frac{\Gamma \vdash \tau \quad \Delta^d \vdash \Theta \quad \Gamma \vdash \sigma : \Delta \triangleright_d \Theta.Ty_d}{\Gamma \vdash \sigma \equiv (\uparrow \circ \sigma) \triangleright \Theta^{\text{ty}}[\sigma \triangleright \text{id}] : \Delta \triangleright_d \Theta.Ty_d} \quad (d: \text{Dir}) $$

$$ \text{TRANSTLAD++} \frac{\Gamma \triangleright \mu : \sigma \Rightarrow \Delta \tau \quad \Delta \vdash \Theta}{\Gamma \triangleright_+ \Theta[\sigma] \vdash A \quad \Gamma \triangleright_+ \Theta[\tau] \vdash B \quad \Gamma \triangleright_+ \Theta[\sigma] \vdash f : A \Rightarrow B[\text{id}_\Gamma \triangleright_+ \Theta[\mu]]} \quad \Gamma \vdash \uparrow \circ (\mu \triangleright_+ f) \equiv \mu : \sigma \Rightarrow \Delta \tau $$

$$ \text{TRANSTLAD+-} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta \vdash \Theta \ (\Gamma \triangleright_+ \Theta[\sigma])^- \vdash A}{(\Gamma \triangleright_+ \Theta[\tau])^- \vdash B \quad (\Gamma \triangleright_+ \Theta[\sigma])^- \vdash f : B[(\text{id}_\Gamma \triangleright_+ \Theta[\mu])^-]} \Rightarrow A \quad \Gamma \vdash \uparrow \circ (\mu \triangleright_d f) \equiv \mu : \sigma \Rightarrow \Delta \tau $$

$$ \text{TRANSTLAD-+} \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta^- \vdash \Theta \ \Gamma \triangleright_- \Theta[\sigma^-] \vdash A}{\Gamma \vdash \uparrow \circ (\mu \triangleright_+ f) \equiv \mu : \sigma \Rightarrow \Delta \tau} \quad \Gamma \vdash \uparrow \circ (\mu \triangleright_+ f) \equiv \mu : \sigma \Rightarrow \Delta \tau $$