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

$$ \text{TRANSADETA+} \quad \frac{\Delta \vdash \Theta \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \triangleright_+ \Theta.Ty_+ \tau}{\Gamma \vdash \mu \equiv (\uparrow \circ \mu) \triangleright \Theta^{\text{ty}}[[\mu \triangleright_+ \text{id}] : \sigma \Rightarrow \Delta \triangleright_+ \Theta.Ty_+ \tau]} \quad \text{(d: Dir)} $$

$$ \text{TRANSADETA-} \quad \frac{\Delta^- \vdash \Theta \quad \Gamma \vdash \mu : \sigma \Rightarrow \Delta \triangleright_- \Theta.Ty_+ \tau}{\Gamma \vdash \mu \equiv (\uparrow \circ \mu) \triangleright \Theta^{\text{ty}}[[\mu \triangleright_- \text{id}] : \sigma \Rightarrow \Delta \triangleright_- \Theta.Ty_+ \tau]} \quad \text{(d: Dir)} $$

$$ \text{TRANSHDAD+} \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 : A \Rightarrow B[\text{id}_{\Gamma} \triangleright_+ \Theta[[\mu^*]]]} \quad \frac{\Gamma \vdash \Theta^{\text{ty}}[[\mu \triangleright_+ f \triangleright_1]] \equiv f[\text{id} \triangleright_1] : A[\text{id} \triangleright_1] \Rightarrow B[\text{id} \triangleright_1 \langle \Theta[[\mu^*]] \rangle]}{\Gamma \vdash \Theta^{\text{ty}}[[\mu \triangleright_+ f \triangleright_1]] \equiv f[\text{id} \triangleright_1] : A[\text{id} \triangleright_1] \Rightarrow B[\text{id} \triangleright_1 \langle \Theta[[\mu^*]] \rangle]} \quad \text{(d: Dir)} $$

$$ \text{TRANSHDAD-} \quad \frac{\Gamma \vdash \mu : \sigma \Rightarrow \Delta \tau \quad \Delta^- \vdash \Theta \quad \Gamma \triangleright_- \Theta[\sigma^-] \vdash A}{\Gamma \triangleright_- \Theta[\tau^-] \vdash B \quad \Gamma \triangleright_- \Theta[\tau^-] \vdash f : A[\text{id}_{\Gamma} \triangleright_- \Theta[[\mu^-]]] \Rightarrow B} \quad \frac{\Gamma \vdash \Theta^{\text{ty}}[[\mu \triangleright_+ f \triangleright_1]] \equiv f[\text{id} \triangleright_1] : A[\text{id} \triangleright_1] \Rightarrow B[\text{id} \triangleright_1 \langle \Theta[[\mu^*]] \rangle]}{\Gamma \vdash \Theta^{\text{ty}}[[\mu \triangleright_+ f \triangleright_1]] \equiv f[\text{id} \triangleright_1] : A[\text{id} \triangleright_1] \Rightarrow B[\text{id} \triangleright_1 \langle \Theta[[\mu^*]] \rangle]} \quad \text{(d: Dir)} $$

### D.7 Rules for Pi

$$ \text{PiTY} \quad \frac{\Gamma^- \vdash A \quad \Gamma \triangleright_- A \vdash B}{\Gamma \vdash \Pi A.B} $$

$$ \text{LAMTM} \quad \frac{\Gamma^- \vdash A \quad \Gamma \triangleright_- A \vdash B \quad \Gamma \triangleright_- A \vdash t : B}{\Gamma \vdash \lambda t : \Pi A.B} $$

$$ \text{APPTM} \quad \frac{\Gamma^- \vdash A \quad \Gamma \triangleright_- A \vdash B \quad \Gamma \vdash f : \Pi A.B \quad \Gamma \vdash x : A}{\Gamma \vdash f @ x : B[\text{id}_\Gamma \triangleright t]} $$

$$ \text{PiSUB} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^- \vdash A \quad \Delta \triangleright_- A \vdash B}{\Gamma \vdash \Pi A.B[\sigma] \equiv \Pi A[\sigma].B[(\sigma \circ \uparrow) \triangleright \Theta^{\text{tm}}_{A[\sigma]})]} \quad \text{(d: Dir)} $$

$$ \text{LAMSUB} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^- \vdash A \quad \Delta \triangleright_- A \vdash B \quad \Delta \triangleright_- A \vdash t : B}{\Gamma \vdash \lambda t[\sigma] \equiv \lambda(t[(\sigma \circ \uparrow) \triangleright \Theta^{\text{tm}}_{A[\sigma]})])} \quad \text{(d: Dir)} $$

$$ \text{APPSUB} \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^- \vdash A \quad \Delta \triangleright_- A \vdash B \quad \Delta \vdash f : \Pi A.B \quad \Delta \vdash x : A}{\Gamma \vdash (f @ x)[\sigma] \equiv f[\sigma] @ x[\sigma] : \Delta} $$

$$ \beta \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^- \vdash A \quad \Delta \triangleright_- A \vdash B \quad \Delta \triangleright_- A \vdash b : B \quad \Delta \vdash x : A}{\Gamma \vdash \lambda b @ x \equiv b[(\sigma \circ \uparrow) \triangleright \Theta^{\text{tm}}_{A[\sigma]})]} $$

$$ \eta \quad \frac{\Gamma \vdash \sigma : \Delta \quad \Delta^- \vdash A \quad \Delta \triangleright_- A \vdash B \quad \Delta \vdash f : \Pi A.B}{\Gamma \vdash f \equiv \lambda(f[\uparrow]) @ \Theta^{\text{tm}}_A} $$

$$ \text{PiAD} \quad \frac{\Gamma \vdash a : A' \Rightarrow A}{\Gamma \triangleright A' \vdash b : B[\Theta^{\text{tm}}(a)] \Rightarrow B'} \quad \frac{\Gamma \vdash \Pi[\text{a} \triangleright \text{b}] : \Pi A.B \Rightarrow \Pi A'.B'}{\Gamma \vdash \Pi[\text{a} \triangleright \text{b}] : \Pi A.B} $$
$$ \begin{array}{r@{\quad}l@{\quad}l} \text{APPPIAD} & \Gamma \vdash f : \Pi A.B & \Gamma \vdash u : A' \\ & \frac{\Gamma \vdash a : A' \Rightarrow A \quad \Gamma \triangleright A' \vdash b : B[\emptyset^{\text{tm}}\langle a \rangle] \Rightarrow B'}{\Gamma \vdash (f\langle\Pi[[a \triangleright b]]\rangle) u \equiv (f(u\langle a \rangle))\langle b[u] \rangle : B'[u]} & \text{TELToPITY} \frac{\Gamma^- \vdash \Theta \quad \Gamma \triangleright_- \Theta \vdash A}{\Gamma \vdash \Pi\Theta.A} \end{array} $$

$$ \text{TELToPIEMP} \quad \frac{\Gamma \vdash A}{\Gamma \vdash \Pi \diamond A \equiv A} \qquad \text{TELToPIEXT} \quad \frac{\Gamma^- \vdash \Theta \quad \Gamma^- \triangleright_+ \Theta \vdash A \quad \Gamma \triangleright_- (\Theta \triangleright A) \vdash B}{\Gamma \vdash \Pi(\Theta \triangleright A).B \equiv \Pi\Theta.\Pi A.B} $$

$$ \text{TELToPISUB} \quad \frac{\Gamma \vdash \sigma\Delta \quad \Delta^- \vdash \Theta \quad \Delta \triangleright_- \Theta \vdash A}{\Gamma \vdash \Pi\Theta.A[\sigma] \equiv \Pi\Theta[\sigma].A[\sigma \triangleright \text{vinst}]} $$

## D.8 Inductive types

$$ \text{DATADESCDEF} \quad \frac{\vdash \Gamma_{par} \quad \Gamma_{par} \vdash \Theta_{ind}}{\text{DataDesc}(\Gamma_{par}, \Theta_{ind}) \coloneqq \overline{\text{ConDesc}(\Gamma_{par}, \Theta_{ind})}} $$

$$ \text{CONDESCDEF} \quad \frac{\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]}{\{nrec := \Theta_{nr}; \text{rec} := r; \text{ind} := \iota\} : \text{ConDesc}(\Gamma_{par}, \Theta_{ind})} $$

$$ \text{RECDESCDEF} \quad \frac{\Gamma_{par} \vdash \Theta_{ind} \quad \Gamma_{par} \vdash \Theta_{nr} \quad (\Gamma_{par} \triangleright \Theta_{nr})^{-} \vdash \Theta_{ar} \quad (\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})} $$

$$ \text{INDTY} \quad \frac{I : \text{DataDesc}(\Gamma_{par}, \Theta_{ind})}{\Gamma_{par} \triangleright \Theta_{ind} \vdash \text{ind}(I)} $$

$$ \text{INDCSTR} \quad \frac{I : \text{DataDesc}(\Gamma_{par}, \Theta_{ind}) \quad c : \text{ConDesc}(\Gamma_{par}, \Theta_{ind}) \quad ic : c \in I}{\Gamma_{par} \triangleright \text{conData}(c)[\text{id} \triangleright \text{ind}(I)] \vdash \text{constr}(ic) : \text{ind}(I)[\text{id} \triangleright c_{.\text{ind}}[\uparrow]]} $$

$$ \text{CONDATADEF} \quad \frac{c : \text{ConDesc}(\Gamma_{par}, \Theta_{ind})}{\Gamma_{par} \triangleright_+ (\Theta_{ind} \cdot \text{Ty}_+)^- \vdash \text{conData}(c) \coloneqq (c_{.nrec}[\uparrow] \triangleright \text{recDatas}(c_{.rec}))} $$

$$ \text{RECDATAS} \quad \frac{\vdash \Gamma_{par} \quad \Gamma_{par} \vdash \Theta_{ind} \quad \Gamma_{par} \vdash \Theta_{nr} \quad c : \overline{\text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})}}{\Gamma_{par} \triangleright_+ (\Theta_{ind} \cdot \text{Ty}_+)^- \triangleright \Theta_{nr}[\uparrow] \vdash \text{recDatas}(c)} $$

$$ \text{RECDATASEMP} \quad \frac{\Gamma_{par} \vdash \Gamma_{par} \vdash \Theta_{ind} \quad \Gamma_{par} \vdash \Theta_{nr}}{\Gamma_{par} \triangleright_+ (\Theta_{ind} \cdot \text{Ty}_+)^- \triangleright \Theta_{nr}[\uparrow] \vdash \text{recDatas}(\diamond) \equiv \diamond} $$

$$ \text{RECDATASEXT} \quad \frac{c : \overline{\text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})} \quad r : \text{RecDesc}(\Gamma_{par}, \Theta_{ind}, \Theta_{nr})}{\Gamma_{par} \triangleright_+ (\Theta_{ind} \cdot \text{Ty}_+)^- \triangleright \Theta_{nr}[\uparrow] \vdash \text{recDatas}(c \triangleright r) \equiv \text{recDatas}(c) \triangleright \text{recData}(r)[\uparrow]} $$
$$
\text{RECDATADEF} \quad \frac{r : \text{RecDesc}(\Gamma_{\text{par}}, \Theta_{\text{ind}}, \Theta_{\text{nr}})}{\Gamma_{\text{par}} \triangleright_+ (\Theta_{\text{ind}} \cdot \text{Ty}_+) \triangleright \Theta_{\text{nr}}[\uparrow] \vdash \text{recData}(r) :\equiv \\ \qquad \qquad \qquad \qquad \Pi r \cdot \text{arit}[\uparrow \triangleright \text{id}]. (\theta^{\text{ty}}[(\uparrow \circ \uparrow) \triangleright (r \cdot \text{rind}[(\uparrow \circ \uparrow \circ \uparrow) \triangleright \text{vinst}[\uparrow] \triangleright \text{vinst}]))}
$$

$$
\begin{array}{l}
\text{INDADEQPAR} \quad \frac{I : \text{DataDesc}(\Gamma_{\text{par}}, \diamond) \quad c : \text{ConDesc}(\Gamma_{\text{par}}, \diamond) \quad ic : c \in I \\
\qquad \Delta \vdash \mu : p \Rightarrow_{\Gamma_{\text{par}}} p' \quad \Delta \vdash \text{arg} : \text{conData}[p \triangleright \text{ind}(I)[p]] \\
\qquad \qquad \Delta \vdash \text{constr}(ic)[p \triangleright \text{arg}]\langle\text{ind}(I)[\llbracket \mu \rrbracket]\rangle \equiv \\
\qquad \qquad \qquad \text{constr}(ic)[p' \triangleright \text{arg}\langle(\text{conData}(c)[\text{id} \triangleright \text{ind}(I)])\rrbracket\rangle] : \text{ind}(I)[p']}
\end{array}
$$

$$
\text{INDADEQ} \quad \frac{I : \text{DataDesc}(\Gamma_{\text{par}}, \Theta_{\text{ind}}) \quad c : \text{ConDesc}(\Gamma_{\text{par}}, \Theta_{\text{ind}}) \quad ic : c \in I \quad \Delta \vdash \mu : p \Rightarrow_{\Gamma_{\text{par}}} p' \\
\qquad \Delta \vdash \text{argn} : c_{\cdot \text{nrec}}[p] \quad \Delta \vdash \text{argr} : \text{recDatas}(c_{\cdot \text{rec}})[p \triangleright \text{ind}(I)[p \triangleright \text{id}] \triangleright \text{argn}]}{\Delta \vdash \text{constr}(ic)[p \triangleright \text{argn} \triangleright \text{argr}]\langle\text{ind}(I)[\llbracket \mu \rrbracket \triangleright c_{\cdot \text{ind}}[p \triangleright \text{argn}]\rrbracket\rangle \equiv \\
\qquad \qquad \text{constr}(ic)[p' \triangleright (\text{argn} \triangleright \text{argr})\langle(\text{conData}(c)[\text{id} \triangleright \text{ind}(I)])\rrbracket\rangle] : \text{ind}(I)[p' \triangleright c_{\cdot \text{ind}}[p \triangleright \text{argn}]\langle\Theta_{\text{ind}}[\llbracket \mu \rrbracket]\rangle]}
$$