blog/posts-wip/algorithmic-xtt.md

---
title: an imperfect algorithmic presentation of xtt
date: 2023-06-12
tags: [computer, types]
bibliography: quox.bib
link-citations: true
show-toc: true
...

hello everyone. as part of my language [quox] i made a typechecking algorithm
for xtt [@xtt]. plus other stuff. but here's just the xtt part, in case anyone
is interested.

[quox]: https://git.rhiannon.website/rhi/quox

- the syntax is slightly different because it uses bidirectional typing [@bidi].
  i've tried to roll back my other arbitrary syntactic changes for this document
  to avoid confusion though. other than subtyping instead of explicit lifting,
  because that seemed significantly easier. to me at least.
- this algorithm [isn't very efficient](#compute-elim-ty). it is what currently
  exists in quox, and when i improve that stuff in future, hopefully i'll
  remember to come back and update this post.
- i also **haven't proven anything**, so if it's wrong, then i apologise for my
  hubris.

anyway. let's get started.

# syntax

mostly follows @xtt, but with a few annotations added or removed for
bidirectional reasons.

- a "term" is a type or an introduction form. it can be checked against a given
  type.
- an "elimination" is a string of elimination forms applied to either a variable
  or an annotated term. its type can be synthesised.
- substitutions take variables to _eliminations_, to preserve typeability,
  and in this presentation, syntactic well-formedness.
- $x, y$ denote term variables, and $𝑖, 𝑗$ denote dimension variables.

:::texdefs
$$
\newcommand\Ceq{\Coloneqq}
\newcommand\Or{\mathrel|}
\newcommand\E\underline
\newcommand\Bar{\mathrel|}
\newcommand\Rule[3]{
  \begin{array}{l}
    \text{\small [#3]} \\
    \displaystyle
    \frac{ \begin{gather}#1\end{gather} }{ \begin{gather}#2\end{gather} }
  \end{array}
}
$$
:::

$$
\begin{aligned}
  ε    &\Ceq 0 \Or 1 & \text{dimension constants} \\
  p, q &\Ceq 𝑖 \Or ε & \text{dimensions} \\
  ξ    &\Ceq p = q   & \text{dimension constraints} \\
  𝓀    &∈ ℕ          & \text{concrete universe levels} \\
  ℓ    &\Ceq 𝓀 \Or \top & \text{judgement levels} \\
  s, t, u, A, B, C &\Ceq
    𝒰_ℓ \Or
    (x : A) → B \Or λx. s  \Or
    (x : A) × B \Or (s, t) \Or
    & \text{terms (incl. types)} \\
  & \mathrel{\hphantom{\Ceq}}
    𝗘𝗾_{𝑖. A} \; s \; t \Or λ𝑖. s \Or
    𝗯𝗼𝗼𝗹 \Or 𝘁𝗿𝘂𝗲 \Or 𝗳𝗮𝗹𝘀𝗲 \Or \E{e} \\
  e, f, g &\Ceq
    x \Or
    f \; s \Or
    𝗳𝘀𝘁 \; e \Or 𝘀𝗻𝗱 \; e \Or
    f \; p \Or
    𝗶𝗳_{x. A} \; e \; 𝘁𝗵𝗲𝗻 \; s \; 𝗲𝗹𝘀𝗲 \; t \Or s : A \Or
    & \text{eliminations} \\
  & \mathrel{\hphantom{\Ceq}}
    [𝑖. A] ↓^p_{p'} s \Or
    A ↓^p_{p'} s \; [q \; 𝘄𝗶𝘁𝗵 \; 0 ↪ 𝑗. t₀ \Bar 1 ↪ 𝑗. t₁] \Or \\
  & \mathrel{\hphantom{\Ceq}}
    𝘁𝘆𝗰𝗮𝘀𝗲_A \; e \; \left[
      \begin{array}{lcl}
        𝒰                               & ↪ & t_𝒰 \\
        Π \; x \; y                     & ↪ & t_Π \\
        Σ \; x \; y                     & ↪ & t_Σ \\
        𝗘𝗾 \; x₀ \; x₁ \; x \; y₀ \; y₁ & ↪ & t_{𝗘𝗾} \\
        𝗯𝗼𝗼𝗹                            & ↪ & t_{𝗯𝗼𝗼𝗹}
      \end{array}
    \right] \\
  Ψ, Φ &\Ceq · \Or Ψ, 𝑖 \Or Ψ, ξ & \text{cubes} \\
  Γ, Δ &\Ceq · \Or Γ, x: A       & \text{contexts}
\end{aligned}
$$

only real levels $𝓀 ∈ ℕ$ can occur in expressions. the special level $\top$ is
for checking a type in a context where any level is accepted, for example the
type in an annotation $s : A$.

in a $𝘁𝘆𝗰𝗮𝘀𝗲$, the pattern variables are assigned this way:

- for a function type $(z : A) → B : 𝒰_𝓀$, the $Π$ case is taken with
  $x ≔ (A : 𝒰_𝓀)$ and $y ≔ ((λz. B) : 𝒰_𝓀 → 𝒰_𝓀)$.
- same for a pair type $(z : A) × B$ and the $Σ$ case.
- for an equality type $𝗘𝗾_{i. A} \; s \; t : 𝒰_𝓀$:
  - $x₀$ and $x₁$ are set to the endpoints of the type line $A$; \
    $x₀ ≔ (A[0/𝑖] : 𝒰_𝓀)$ and $x₁ ≔ (A[1/𝑖] : 𝒰_𝓀)$.
  - $x$ is an equality between them; \
    $x ≔ ((λ𝑖. A) : 𝗘𝗾_{𝑖. 𝒰_𝓀} \; A[0/𝑖] \; A[1/𝑖]$.
  - $y₀$ and $y₁$ are the terms being equated; \
    $y₀ ≔ (s : A[0/𝑖])$ and $y₁ ≔ (t : A[1/𝑖])$.

----

:::texdefs
$$
\newcommand\IN{\textcolor{#60c}}
\newcommand\OUT{\textcolor{#082}}
$$
:::

<style>
.input  { font-weight: 500; color: #60c; }
.output { font-weight: 500; color: #082; }
</style>

when introducing new judgements, the [inputs]{.input} and [outputs]{.output} are
colour coded. all judgements assume that the cube and context are well formed
(omitted).

:::rulebox
$$
\begin{gathered}
\IN{Ψ} ⊢ \IN{p} \; 𝐝𝐢𝐦 \qquad
\IN{Ψ} ⊢ \IN{p} = \IN{p'} \; 𝐝𝐢𝐦
\end{gathered}
$$
:::

# dimension checking {#dim}

the well-formedness rules are the same as in the paper. since quox uses well
scoped de bruijn indices, every value of type `Dim d` is well formed, so they
don't exist at all really.

the equality rules are just baby's first equational theory solver.


:::rulebox
$$ \IN{Ψ} \Bar \IN{Γ} ⊢ \IN{A} ⇐ 𝐭𝐲𝐩𝐞_{\IN{ℓ}} $$
:::

# type checking {#ty}

$$ \Rule{}{Ψ, 0=1 \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_ℓ}{ty-01} $$

$$ \Rule{}{Ψ \Bar Γ ⊢ 𝗯𝗼𝗼𝗹 ⇐ 𝐭𝐲𝐩𝐞_ℓ}{ty-bool} $$

$$
\Rule{
  Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_ℓ \qquad
  Ψ \Bar Γ, x : A ⊢ B ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{
  Ψ \Bar Γ ⊢ (x : A) → B ⇐ 𝐭𝐲𝐩𝐞_ℓ \\
  Ψ \Bar Γ ⊢ (x : A) × B ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{ty-pi; ty-sig}
$$

$$
\Rule{
  Ψ, 𝑖 \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_ℓ \qquad
  Ψ, 𝑖, 𝑖 = ε \Bar Γ ⊢ s_ε ⇐ A
}{
  Ψ \Bar Γ ⊢ 𝗘𝗾_{𝑖. A} \; s₀ \; s₁ ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{ty-eq}
$$

$$ \Rule{Ψ \Bar Γ ⊢ e ⇒ 𝒰_ℓ}{Ψ \Bar Γ ⊢ \E e ⇐ 𝐭𝐲𝐩𝐞_ℓ}{ty-el} $$

:::rulebox
$$ \IN{ℓ} < \IN{ℓ'} $$
:::

for comparing levels:

$$
\Rule{𝓀 <_ℕ 𝓀'}{𝓀 < 𝓀'}{lvl-nat} \qquad
\Rule{𝓀 ∈ ℕ}{𝓀 < \top}{lvl-top}
$$


:::rulebox
$$ \IN{Ψ} \Bar \IN{Γ} ⊢ \IN{s} ⇐ \IN{A} $$
:::

# term checking {#chk}

assumes that $Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_\top$.

$$ \Rule{}{Ψ, 0=1 \Bar Γ ⊢ s ⇐ A}{tm-01} $$

[reduce the expected type to whnf](#tm-red) before trying to match against it, of
course.

$$
\Rule{
  Γ ⊢ 𝐰𝐡𝐧𝐟 \; A ↦ A' \qquad
  Ψ \Bar Γ ⊢_w s ⇐ A'
}{Ψ \Bar Γ ⊢ s ⇐ A}{tm-whnf}
$$

if $s$ is syntactically a type, then defer to $𝐭𝐲𝐩𝐞$ [above](#ty).

$$ \Rule{Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_ℓ}{Ψ \Bar Γ ⊢_w A ⇐ 𝒰_ℓ}{tm-ty} $$

otherwise:

$$
\Rule{Ψ \Bar Γ, x : A ⊢ s ⇐ B}{Ψ \Bar Γ ⊢_w λx. s ⇐ (x : A) → B}{tm-lam}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ s ⇐ A \qquad
  Ψ \Bar Γ ⊢ t ⇐ B[(t:A)/x]
}{Ψ \Bar Γ ⊢_w (s, t) ⇐ (x : A) × B}{tm-pair}
$$

$$
\Rule{
  Ψ, i \Bar Γ ⊢ s ⇐ A \qquad
  Ψ, i, i = ε \Bar Γ ⊢ s = s_ε ⇐ A
}{Ψ \Bar Γ ⊢_w λ𝑖. s ⇐ 𝗘𝗾_{𝑖. A} \; s₀ \; s₁}{tm-dlam}
$$

$$
\Rule{}{
  Ψ \Bar Γ ⊢_w 𝘁𝗿𝘂𝗲 ⇐ 𝗯𝗼𝗼𝗹 \qquad Ψ \Bar Γ ⊢_w 𝗳𝗮𝗹𝘀𝗲 ⇐ 𝗯𝗼𝗼𝗹
}{tm-true; tm-false}
$$

:::aside
maybe you want to make $𝘁𝗿𝘂𝗲$ and $𝗳𝗮𝗹𝘀𝗲$ inferrable. _in my opinion_, there are
not that many cases where you end up having to write $𝘁𝗿𝘂𝗲 : 𝗯𝗼𝗼𝗹$, and, if you
have separate term/elim syntactic classes like i do, it's not worth muddying the
nice clean separation in e.g. $𝐰𝐡𝐧𝐟$ for this. in my onion. :onion:
:::

$$
\Rule{
  Ψ \Bar Γ ⊢ e ⇒ A' \qquad
  Ψ \Bar Γ ⊢ A <:_\top A'
}{Ψ \Bar Γ ⊢ \E e ⇐ A}{tm-el}
$$


:::rulebox
$$ \IN{Ψ} \Bar \IN{Γ} ⊢ \IN{e} ⇒ \OUT{A} $$
:::

# elimination synthesis {#syn}

$$ \Rule{}{Ψ, 0=1 \Bar Γ ⊢ e ⇒ 𝗯𝗼𝗼𝗹}{el-01} $$

in an inconsistent cube, the type being returned is just a placeholder.
in quox, the typechecker returns what is essentially a more
fancily-typed `Maybe`, with `Nothing` iff $Ψ ⊢ 0=1 \; 𝐝𝐢𝐦$.

$$ \Rule{x : A ∈ Γ}{Ψ \Bar Γ ⊢ x ⇒ A}{el-var} $$

$$
\Rule{
  Ψ \Bar Γ ⊢ f ⇒ (x : A) → B \qquad
  Ψ \Bar Γ ⊢ s ⇐ A
}{Ψ \Bar Γ ⊢ f \; s ⇒ B[(s:A)/x]}{el-app}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ e ⇒ (x : A) × B
}{
  Ψ \Bar Γ ⊢ 𝗳𝘀𝘁 \; e ⇒ A \qquad
  Ψ \Bar Γ ⊢ 𝘀𝗻𝗱 \; e ⇒ B[(𝗳𝘀𝘁 \; e)/x]
}{el-fst; el-snd}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ e ⇒ 𝗯𝗼𝗼𝗹 \qquad
  Ψ \Bar Γ, x : 𝗯𝗼𝗼𝗹 ⊢ A ⇐ 𝐭𝐲𝐩𝐞_\top \\
  Ψ \Bar Γ ⊢ s ⇐ A[(𝘁𝗿𝘂𝗲 : 𝗯𝗼𝗼𝗹)/x] \qquad
  Ψ \Bar Γ ⊢ t ⇐ A[(𝗳𝗮𝗹𝘀𝗲 : 𝗯𝗼𝗼𝗹)/x]
}{
  Ψ \Bar Γ ⊢ 𝗶𝗳_{x. A} \; e \; 𝘁𝗵𝗲𝗻 \; s \; 𝗲𝗹𝘀𝗲 \; t ⇒ A[e/x]
}{el-if}
$$

:::aside
maybe you want to make the head of $𝗶𝗳$ be checkable. same caveat as making
$𝘁𝗿𝘂𝗲$/$𝗳𝗮𝗹𝘀𝗲$ inferrable. i just don't think $𝗶𝗳 \; 𝘁𝗿𝘂𝗲 : 𝗯𝗼𝗼𝗹 \; 𝘁𝗵𝗲𝗻 ⋯$
comes up often enough to worry about it.
:::

$$
\Rule{
  Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_\top \qquad
  Ψ \Bar Γ ⊢ s ⇐ A
}{
  Ψ \Bar Γ ⊢ s : A ⇒ A
}{el-ann}
$$

$$
\Rule{
  Ψ, 𝑖 \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_\top \qquad
  Ψ ⊢ p \qquad Ψ ⊢ p' \qquad
  Ψ \Bar Γ ⊢ s ⇐ A[p/𝑖]
}{
  Ψ \Bar Γ ⊢ [𝑖. A] ↓^p_{p'} s ⇒ A[p'/𝑖]
}{el-coe}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_\top \qquad
  Ψ \Bar Γ ⊢ s ⇐ A \\
  Ψ, q=ε, 𝑗 \Bar Γ ⊢ t_ε ⇐ A \qquad
  Ψ, q=ε, 𝑗, 𝑗=p \Bar Γ ⊢ t_ε = s ⇐ A \\
}{
  Ψ \Bar Γ ⊢
    A ↓^p_{p'} s \; [q \; 𝘄𝗶𝘁𝗵 \; 0 ↪ 𝑗. t₀ \Bar 1 ↪ 𝑗. t₁]
    ⇒ A
}{el-comp}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_\top \qquad
  Ψ \Bar Γ ⊢ e ⇒ 𝒰_𝓀 \\
  Ψ \Bar Γ ⊢ t_𝒰 ⇐ A \qquad
  Ψ \Bar Γ ⊢ t_{𝗯𝗼𝗼𝗹} ⇐ A \\
  Ψ \Bar Γ, x : 𝒰_𝓀, y : 𝒰_𝓀 ⊢ t_Π ⇐ A \qquad
  Ψ \Bar Γ, x : 𝒰_𝓀, y : 𝒰_𝓀 ⊢ t_Σ ⇐ A \\
  Ψ \Bar Γ, x₀ : 𝒰_𝓀, x₁ : 𝒰_𝓀, x : 𝗘𝗾_{\_. 𝒰_𝓀} \; x₀ \; x₁,
            y₀ : x₀, y₁ : x₁ ⊢ t_{𝗘𝗾} ⇐ A
}{
  Ψ \Bar Γ ⊢
    𝘁𝘆𝗰𝗮𝘀𝗲_A \; e \; \left[
      \begin{array}{lcl}
        𝒰                               & ↪ & t_𝒰 \\
        Π \; x \; y                     & ↪ & t_Π \\
        Σ \; x \; y                     & ↪ & t_Σ \\
        𝗘𝗾 \; x₀ \; x₁ \; x \; y₀ \; y₁ & ↪ & t_{𝗘𝗾} \\
        𝗯𝗼𝗼𝗹                            & ↪ & t_{𝗯𝗼𝗼𝗹}
      \end{array}\right] ⇒ A
}{el-tycase}
$$


:::rulebox
$$ \IN Ψ \Bar \IN Γ ⊢ \IN A <:_{\IN ℓ} \IN B $$
:::

# subtyping {#sub}

$$
\Rule{Ψ \Bar Γ ⊢ A = A' ⇐ 𝐭𝐲𝐩𝐞_ℓ}{Ψ \Bar Γ ⊢ A <:_{ℓ} A'}{sub-eq}
\qquad
\Rule{𝓀₁ ≤ 𝓀₂ < ℓ}{Ψ \Bar Γ ⊢ 𝒰_{𝓀₁} <:_{ℓ} 𝒰_{𝓀₂}}{sub-univ}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ A' <:_{ℓ} A \qquad
  Ψ \Bar Γ ⊢ B <:_{ℓ} B'
}{
  Ψ \Bar Γ ⊢ (x : A) → B <:_{ℓ} (x : A') → B'
}{sub-Π}
\qquad
\Rule{
  Ψ \Bar Γ ⊢ A <:_{ℓ} A' \qquad
  Ψ \Bar Γ ⊢ B <:_{ℓ} B'
}{
  Ψ \Bar Γ ⊢ (x : A) × B <:_{ℓ} (x : A') × B'
}{sub-Σ}
$$

$$
\Rule{
  Ψ \Bar Γ ⊢ A <:_{ℓ} A' \qquad
  Ψ \Bar Γ ⊢ s = s' ⇐ A'[0/𝑖] \qquad
  Ψ \Bar Γ ⊢ t = t' ⇐ A'[1/𝑖]
}{
  Ψ \Bar Γ ⊢ 𝗘𝗾_{i.A} \; s \; t <:_{ℓ} 𝗘𝗾_{i. A'} \; s' \; t'
}{sub-eq}
$$


# equality {#eq}

due to boundary separation, equality is tested separately in every consistent
corner of the cube, by generating all dimension substitutions and applying each
one in turn. the judgements with $⊢_s$ are used in each corner individually.

$$
ψ, φ \Ceq · \Or ψ, ε/𝑖 \qquad \text{dimension substitutions}
$$


:::rulebox
$$ \OUT ψ ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; \IN Ψ $$
:::

## cube splitting

in general $ψ$ has multiple solutions, returned as a set.

$$
\Rule{}{· ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; ·}{sd-nil}
$$

$$
\Rule{
  ψ ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; Ψ
}{
  ψ, 0/𝑖 ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} (Ψ, 𝑖) \\
  ψ, 0/𝑖 ∈
  𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} (Ψ, 𝑖, 𝑖=0)
}{sd-0}
\qquad
\Rule{
  ψ ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; Ψ
}{
  ψ, 1/𝑖 ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} (Ψ, 𝑖) \\
  ψ, 1/𝑖 ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} (Ψ, 𝑖, 𝑖=1)
}{sd-1}
$$


:::rulebox
$$ \IN{Ψ} \Bar \IN{Γ} ⊢ \IN{A} = \IN{A'} ⇐ 𝐭𝐲𝐩𝐞_{\IN{ℓ}} $$
:::

## types {#ty-eq}

assumes that $Ψ \Bar Γ ⊢ A ⇐ 𝐭𝐲𝐩𝐞_ℓ$ and $Ψ \Bar Γ ⊢ A' ⇐ 𝐭𝐲𝐩𝐞_ℓ$.

$$
\Rule{
  ∀ ψ ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; Ψ. Γ ⊢_𝐬 A[ψ] = B[ψ] ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{
  Ψ \Bar Γ ⊢ A = B ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{eq-ty-split}
$$

$$ \Rule{𝓀 < ℓ}{Γ ⊢_𝐬 𝒰_𝓀 = 𝒰_𝓀 ⇐ 𝐭𝐲𝐩𝐞_ℓ}{eq-ty-univ} $$

$$
\Rule{
  Γ ⊢_𝐬 A = A' ⇐ 𝐭𝐲𝐩𝐞_ℓ \qquad
  Γ, x : A ⊢_𝐬 B = B' ⇐ 𝐭𝐲𝐩𝐞_ℓ \qquad
}{
  Γ ⊢_𝐬 ((x : A) → B) = ((x : A') → B) ⇐ 𝐭𝐲𝐩𝐞_ℓ \\
  Γ ⊢_𝐬 ((x : A) × B) = ((x : A') × B) ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{eq-ty-\{Π,Σ\}}
$$

$$
\Rule{
  Γ ⊢_𝐬 A[0/𝑖] = A'[0/𝑖] ⇐ 𝐭𝐲𝐩𝐞_ℓ \qquad
  Γ ⊢_𝐬 A[1/𝑖] = A'[1/𝑖] ⇐ 𝐭𝐲𝐩𝐞_ℓ \\
  Γ ⊢_𝐬 s = s' ⇐ A[0/𝑖] \qquad
  Γ ⊢_𝐬 t = t' ⇐ A[1/𝑖]
}{
  Γ ⊢_𝐬 𝗘𝗾_{i. A} \; s \; t = 𝗘𝗾_{i. A'} \; s' \; t' ⇐ 𝐭𝐲𝐩𝐞_ℓ
}{eq-ty-eq}
$$

$$ \Rule{}{Γ ⊢_𝐬 𝗯𝗼𝗼𝗹 = 𝗯𝗼𝗼𝗹 ⇐ 𝐭𝐲𝐩𝐞_ℓ}{eq-ty-bool} $$

$$ \Rule{Γ ⊢_𝐬 e = e' ⇒ 𝒰_𝓀}{Γ ⊢_𝐬 \E{e} = \E{e'} ⇐ 𝐭𝐲𝐩𝐞_𝓀}{eq-ty-el} $$


:::rulebox
$$
\begin{gathered}
\IN{Ψ} \Bar \IN{Γ} ⊢ \IN{s} = \IN{s'} ⇐ \IN{A} \\
\IN{Γ} ⊢_𝐬 \IN{s} = \IN{s'} ⇐ \IN{A}
\end{gathered}
$$
:::

## terms {#tm-eq}

assumes that $Ψ \Bar Γ ⊢ s ⇐ A$ and $Ψ \Bar Γ ⊢ s' ⇐ A$.

$$
\Rule{
  ∀ ψ ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; Ψ. Γ ⊢_𝐬 s[ψ] = s'[ψ] ⇐ A[ψ]
}{
  Ψ \Bar Γ ⊢ s = s' ⇐ A
}{eq-tm-split}
$$

$$
\Rule{
  Γ ⊢ A \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠
}{
  Γ ⊢_𝐬 s = t ⇐ A
}{eq-tm-subsing}
$$

### types

$$ \Rule{Γ ⊢_𝐬 s = t ⇐ 𝐭𝐲𝐩𝐞_𝓀}{Γ ⊢_𝐬 s = t ⇐ 𝒰_𝓀}{eq-tm-ty} $$

### functions

$$
\Rule{
  Γ, x : A ⊢_𝐬 s = t ⇐ B
}{
  Γ ⊢_𝐬 (λx. s) = (λx. t) ⇐ (x : A) → B
}{eq-tm-λ}
$$

$$
\Rule{
  Γ, x : A ⊢_𝐬 s = \E{e \; x} ⇐ B
}{
  Γ ⊢_𝐬 (λx. s) = \E e ⇐ (x : A) → B
}{eq-tm-λ-η1}
\qquad
\Rule{
  Γ, x : A ⊢_𝐬 \E{e \; x} = s ⇐ B
}{
  Γ ⊢_𝐬 \E e = (λx. s) ⇐ (x : A) → B
}{eq-tm-λ-η2}
$$

### pairs

$$
\Rule{
  Γ ⊢_𝐬 s₀ = t₀ ⇐ A \qquad
  Γ, x : A ⊢_𝐬 s₁ = t₁ ⇐ B[s₀/x]
}{
  Γ ⊢ (s₀, s₁) = (t₀, t₁) ⇐ (x : A) × B
}{eq-tm-pair}
$$

$$
\Rule{
  Γ ⊢_𝐬 s₀ = \E{𝗳𝘀𝘁 \; e} ⇐ A \qquad
  Γ ⊢_𝐬 s₁ = \E{𝘀𝗻𝗱 \; e} ⇐ B[s₀/x]
}{
  Γ ⊢ (s₀, s₁) = \E e ⇐ (x : A) × B
}{eq-tm-pair-η1}
$$

$$
\Rule{
  Γ ⊢_𝐬 \E{𝗳𝘀𝘁 \; e} = t₀ ⇐ A \qquad
  Γ ⊢_𝐬 \E{𝘀𝗻𝗱 \; e} = t₁ ⇐ B[t₀/x]
}{
  Γ ⊢ \E e = (t₀, t₁) ⇐ (x : A) × B
}{eq-tm-pair-η2}
$$

### equalities

look! uip!

$$ \Rule{}{Γ ⊢_𝐬 s₀ = s₁ ⇐ 𝗘𝗾_{i. A} \; t₀ \; t₁}{eq-tm-dλ} $$

### bool

$$
\Rule{}{Γ ⊢_𝐬 𝘁𝗿𝘂𝗲 = 𝘁𝗿𝘂𝗲 ⇐ 𝗯𝗼𝗼𝗹}{eq-tm-true} \qquad
\Rule{}{Γ ⊢_𝐬 𝗳𝗮𝗹𝘀𝗲 = 𝗳𝗮𝗹𝘀𝗲 ⇐ 𝗯𝗼𝗼𝗹}{eq-tm-false}
$$

### eliminations

$$ \Rule{Γ ⊢_𝐬 e = e' ⇒ A}{Γ ⊢_𝐬 \E e = \E{e'} ⇐ A}{eq-tm-el} $$


:::rulebox
$$
\begin{gathered}
\IN{Ψ} \Bar \IN{Γ} ⊢ \IN{e} = \IN{e'} \\
\IN{Γ} ⊢_𝐬 \IN{e} = \IN{e'} ⇒ \OUT{A}
\end{gathered}
$$
:::

## eliminations {#el-eq}

assumes that $Ψ \Bar Γ ⊢ e ⇒ A$ and $Ψ \Bar Γ ⊢ e' ⇒ A$ for some $A$.

$$
\Rule{
  ∀ ψ ∈ 𝐬𝐩𝐥𝐢𝐭_{𝐝𝐢𝐦} \; Ψ. ∃A. Γ ⊢_𝐬 e[ψ] = e'[ψ] ⇒ A
}{
  Ψ \Bar Γ ⊢ e = e'
}{eq-el-split}
$$

$$
\Rule{
  Γ ⊢ 𝐭𝐲 \; e ↦ A \qquad Γ ⊢ A \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠
}{
  Γ ⊢_𝐬 e = e' ⇒ A
}{eq-el-subsing}
$$

:::aside
the type computed for this rule can't be shared with the rest of the rules,
because they only return a type when they succeed. very unsatisfying
:::

$$ \Rule{(x : A) ∈ Γ}{Γ ⊢_𝐬 x = x ⇒ A}{eq-el-var} $$

$$
\Rule{
  Γ ⊢_𝐬 f = f' ⇒ (x : A) → B \qquad
  Γ ⊢_𝐬 s = s' ⇐ A
}{
  Γ ⊢_𝐬 f \; s = f' \; s' ⇒ B[s/x]
}{eq-el-app}
$$

$$
\Rule{
  Γ ⊢_𝐬 e = e' ⇒ (x : A) × B
}{
  Γ ⊢_𝐬 𝗳𝘀𝘁 \; e = 𝗳𝘀𝘁 \; e' ⇒ A \\
  Γ ⊢_𝐬 𝘀𝗻𝗱 \; e = 𝘀𝗻𝗱 \; e' ⇒ B[𝗳𝘀𝘁 \; e/x]
}{eq-el-\{fst,snd\}}
$$

$$
\Rule{
  Γ, x : 𝗯𝗼𝗼𝗹 ⊢_𝐬 A = A' ⇐ 𝐭𝐲𝐩𝐞_\top \qquad
  Γ ⊢_𝐬 e = e' ⇒ 𝗯𝗼𝗼𝗹 \\
  Γ ⊢_𝐬 s = s' ⇐ A[(𝘁𝗿𝘂𝗲 : 𝗯𝗼𝗼𝗹)/x] \qquad
  Γ ⊢_𝐬 t = t' ⇐ A[(𝗳𝗮𝗹𝘀𝗲 : 𝗯𝗼𝗼𝗹)/x]
}{
  Γ ⊢_𝐬 𝗶𝗳_{x.A} \; e \; 𝘁𝗵𝗲𝗻 \; s \; 𝗲𝗹𝘀𝗲 \; t =
    𝗶𝗳_{x.A'} \; e' \; 𝘁𝗵𝗲𝗻 \; s' \; 𝗲𝗹𝘀𝗲 \; t' ⇒ A[e/x]
}{eq-el-if}
$$

TODO coe

in an empty cube, there are no dimension applications or compositions.


:::rulebox
$$ \IN Γ ⊢ \IN A \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠$$
:::

# subsingleton types

if a type is a <dfn>subsingleton</dfn> (only ever has zero or one possible
values), then skip the equality check for its elements. this is used for neutral
terms e.g. two bound variables of the same equality type.

$$
\Rule{
  Γ ⊢ 𝐰𝐡𝐧𝐟 \; A ↦ A' \qquad
  Γ ⊢ A' \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠_𝐰
}{Γ ⊢ A \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠}{subsing}
$$

$$
\Rule{}{
  Γ ⊢ 𝗘𝗾_{i. A} \; s \; t \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠_𝐰
}{subsing-eq}
$$

$$
\Rule{
  Γ, x : A ⊢ B \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠
}{
  Γ ⊢ (x : A) → B \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠_𝐰
}{subsing-Π}
\qquad
\Rule{
  Γ ⊢ A \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠 \qquad
  Γ, x : A ⊢ B \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠
}{
  Γ ⊢ (x : A) × B \; 𝐬𝐮𝐛𝐬𝐢𝐧𝐠_𝐰
}{subsing-Σ}
$$


# reduction {#red}

:::rulebox
$$ \IN{Γ} ⊢ 𝐰𝐡𝐧𝐟 \; \IN{s} ↦ \OUT{s'} $$
:::

## terms {#tm-red}

assumes that $s$ is well-typed (in some consistent cube).

types and introduction forms are already in whnf. so the only case non-trivial
case is for embedded eliminations.

$$
\Rule{Γ ⊢ 𝐰𝐡𝐧𝐟 \; e ↦ e'}{Γ ⊢ 𝐰𝐡𝐧𝐟 \; \E e ↦ \E{e'}}{whnf-embed}
\qquad
\Rule{\text{$t$ is not an elimination}}{Γ ⊢ 𝐰𝐡𝐧𝐟 \; t ↦ t}{whnf-none}
$$


:::rulebox
$$
\begin{gathered}
\IN{Γ} ⊢ 𝐰𝐡𝐧𝐟 \; \IN{e} ↦ \OUT{e'} \\
\IN{Γ} ⊢ \IN{e} ⇝ \OUT{e'}
\end{gathered}
$$
:::

## eliminations {#el-red}

assumes that $e$ is well-typed (in some consistent cube).

keep stepping the outermost expression until no more rules apply.

$$ \Rule{Γ ⊢ e ⇝^! e'}{Γ ⊢ 𝐰𝐡𝐧𝐟 \; e ↦ e'}{whnf-el} $$

### function application

$$ \Rule{Γ ⊢ e ⇝ e'}{Γ ⊢ e \; t ⇝ e' \; t}{step-app-head} $$

$$
\Rule{}{
  Γ ⊢ ((λx. t) : (x : A) → B) \; s ⇝ (t[(s:A)/x] : B[(s:A)/x])
}{step-app-β}
$$

$$
\Rule{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Π \; x \; C ↦ (A, B) \qquad
  𝐥𝐞𝐭 \; \hat{s}[𝑗] ≔ [𝑖. A] ↓^q_𝑗 s
}{
  Γ ⊢ (([𝑖. C] ↓^p_q s) \; t) ⇝
    [𝑖. B[\hat{s}[i]/x]] ↓^p_q ((t : C[p/𝑖]) \; \hat{s}[p])
}{step-app-coe}
$$

where $\IN Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Π \; \IN{x} \; \IN{C} ↦ (\OUT A, \OUT B)$ is:

$$ \Rule{}{Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Π \; x \; ((y : A) → B) ↦ (A, B[x/y])}{split-Π-con} $$

$$
\Rule{
  Γ ⊢ 𝐭𝐲 \; e ↦ 𝒰_𝓀 \\
  𝐥𝐞𝐭 \; A ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \; [Π \; x  \; \_ ↪ x \Bar \_ ↪ 𝗯𝗼𝗼𝗹] \\
  𝐥𝐞𝐭 \; B ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \; [Π \; \_ \; y  ↪ y \Bar \_ ↪ 𝗯𝗼𝗼𝗹]
}{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Π \; x \; \E e ↦ (A, B \; x)
}{split-Π-neut}
$$

$A$ lives in $Γ$ and $B$ lives in $(Γ, x:A)$.

### pair projections

$$
\Rule{Γ ⊢ e ⇝ e'}{
  Γ ⊢ 𝗳𝘀𝘁 \; e ⇝ 𝗳𝘀𝘁 \; e' \qquad
  Γ ⊢ 𝘀𝗻𝗱 \; e ⇝ 𝘀𝗻𝗱 \; e'
}{step-\{fst,snd\}-head}
$$

$$
\Rule{}{
  Γ ⊢ 𝗳𝘀𝘁 ((s, t) : (x : A) × B) ⇝ (s : A) \\
  Γ ⊢ 𝘀𝗻𝗱 ((s, t) : (x : A) × B) ⇝ (t : B[s/x])
}{step-\{fst,snd\}-β}
$$

$$
\Rule{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Σ \; x\ ; C ↦ (A, B)
}{
  Γ ⊢ 𝗳𝘀𝘁 ([𝑖. C] ↓^p_q s) ⇝ [𝑖. A] ↓^p_q 𝗳𝘀𝘁 \; (s : A[p/𝑖])
}{step-fst-coe}
$$

$\IN Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Σ \; \IN{x} \; \IN{C} ↦ (\OUT A, \OUT B)$ is:

$$
\Rule{}{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Σ \; x \; ((y : A) × B) ↦ (A, B[x/y])
}{split-Σ-con}
\qquad
\Rule{
  Γ ⊢ 𝐭𝐲 \; e ↦ 𝒰_𝓀 \\
  𝐥𝐞𝐭 \; A ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \; [Σ \; x \; y ↪ x \Bar \_ ↪ 𝗯𝗼𝗼𝗹] \\
  𝐥𝐞𝐭 \; B ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \; [Σ \; x \; y ↪ y \Bar \_ ↪ 𝗯𝗼𝗼𝗹]
}{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_Σ \; x \; \E e ↦ (A, B \; x)
}{split-Σ-neut}
$$

$A$ lives in $Γ$ and $B$ lives in $(Γ, x:A)$.

### dimension application

$$ \Rule{Γ ⊢ e ⇝ e'}{Γ ⊢ e \; p ⇝ e' \; p}{step-dapp-head} $$

$$
\Rule{}{
  Γ ⊢ ((λ𝑖. t) : 𝗘𝗾_{𝑖. A} \; s₀ \; s₁) \; ε ⇝ (s_ε : A[ε/𝑖])
}{step-dapp-β-end}
$$

$$
\Rule{}{
  Γ ⊢ ((λ𝑖. t) : 𝗘𝗾_{𝑖. A} \; s₀ \; s₁) \; 𝑗 ⇝ (t[𝑗/𝑖] : A[𝑗/𝑖])
}{step-dapp-β-var}
$$

$$
\Rule{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_{𝗘𝗾} \; 𝑖 \; C ↦ (A₀, A₁, A, s₀, s₁)
}{
  Γ ⊢ ([𝑗. C] ↓^p_{p'} t) \; q ⇝
    [𝑗. A[q/𝑖]] ↓^p_{p'} (t : (𝗘𝗾_{𝑖.A} \; s₀ \; s₁)[p/𝑗]) \;
      [q \; 𝘄𝗶𝘁𝗵 \; 0 ↪ 𝑗. s₀ \Bar 1 ↪ 𝑗. s₁]
}{step-dapp-coe}
$$

this heterogeneous composition is defined in @xtt in terms of composition and
coercion.
$\IN Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_{𝗘𝗾} \; \IN 𝑖 \; \IN C ↦
 (\OUT{A₀}, \OUT{A₁}, \OUT A, \OUT{s₀}, \OUT{s₁})$
is:

$$
\Rule{}{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_{𝗘𝗾} \; 𝑖 \; (𝗘𝗾_{j. A} \; s₀ \; s₁) ↦
    (A[0/𝑗], A[1/𝑗], A[𝑖/𝑗], s₀, s₁)
}{split-Eq-con}
$$

$$
\Rule{
  Γ ⊢ 𝐭𝐲 \; e ↦ 𝒰_𝓀 \\
  𝐥𝐞𝐭 \; A₀ ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \;
    [𝗘𝗾 \; a₀ \; a₁ \; a \; x₀ \; x₁ ↪ a₀ \Bar \_ ↪ 𝗯𝗼𝗼𝗹] \\
  𝐥𝐞𝐭 \; A₁ ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \;
    [𝗘𝗾 \; a₀ \; a₁ \; a \; x₀ \; x₁ ↪ a₁ \Bar \_ ↪ 𝗯𝗼𝗼𝗹] \\
  𝐥𝐞𝐭 \; A ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \;
    [𝗘𝗾 \; a₀ \; a₁ \; a \; x₀ \; x₁ ↪ a \Bar \_ ↪ 𝗯𝗼𝗼𝗹] \\
  𝐥𝐞𝐭 \; s₀ ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \;
    [𝗘𝗾 \; a₀ \; a₁ \; a \; x₀ \; x₁ ↪ x₀ \Bar \_ ↪ 𝗯𝗼𝗼𝗹] \\
  𝐥𝐞𝐭 \; s₁ ≔ 𝘁𝘆𝗰𝗮𝘀𝗲_{𝒰_𝓀} \; e \;
    [𝗘𝗾 \; a₀ \; a₁ \; a \; x₀ \; x₁ ↪ x₁ \Bar \_ ↪ 𝗯𝗼𝗼𝗹]
}{
  Γ ⊢ 𝐬𝐩𝐥𝐢𝐭_{𝗘𝗾} \; 𝑖 \; \E e ↦ (A₀, A₁, A \; 𝑖, s₀, s₁)
}{split-Eq-neut}
$$

if $C$ lives in some cube $Ψ$, then $A$ lives in $(Ψ, i)$, and the others
live in $Ψ$.

### conditional

$$
\Rule{Γ ⊢ e ⇝ e'}{
  Γ ⊢ 𝗶𝗳_{x. A} \; e \; 𝘁𝗵𝗲𝗻 \; s₀ \; 𝗲𝗹𝘀𝗲 \; s₁ ⇝
      𝗶𝗳_{x. A} \; e' \; 𝘁𝗵𝗲𝗻 \; s₀ \; 𝗲𝗹𝘀𝗲 \; s₁}{step-if-head}
$$

$$
\Rule{}{
  Γ ⊢ 𝗶𝗳_{x. A} \; 𝘁𝗿𝘂𝗲:𝗯𝗼𝗼𝗹 \; 𝘁𝗵𝗲𝗻 \; s₀ \; 𝗲𝗹𝘀𝗲 \; s₁ ⇝
      (s₀ : A[(𝘁𝗿𝘂𝗲:𝗯𝗼𝗼𝗹)/x]) \\
  Γ ⊢ 𝗶𝗳_{x. A} \; 𝗳𝗮𝗹𝘀𝗲:𝗯𝗼𝗼𝗹 \; 𝘁𝗵𝗲𝗻 \; s₀ \; 𝗲𝗹𝘀𝗲 \; s₁ ⇝
      (s₁ : A[(𝗳𝗮𝗹𝘀𝗲:𝗯𝗼𝗼𝗹)/x])
}{step-if-true; step-if-false}
$$

$$
\Rule{}{
  Γ ⊢ 𝗶𝗳_{x.A} \; [𝑖.C] ↓^p_q t \; 𝘁𝗵𝗲𝗻 \; s₀ \; 𝗲𝗹𝘀𝗲 \; s₁ ⇝
      𝗶𝗳_{x.A} \; t : 𝗯𝗼𝗼𝗹 \; 𝘁𝗵𝗲𝗻 \; s₀ \; 𝗲𝗹𝘀𝗲 \; s₁
}{step-if-coe}
$$

if the expression is well-typed, as we are assuming, then $C$ can only be
something that reduces to $𝗯𝗼𝗼𝗹$.


### coercion

$$
\Rule{Γ ⊢ e ⇝ e'}{Γ ⊢ [𝑖. \E e] ↓^p_q s ⇝ [𝑖. \E{e'}] ↓^p_q s}{step-coe-ty}
\qquad
\Rule{𝑖 ∉ 𝐟𝐝𝐯 \; C}{Γ ⊢ [𝑖. C] ↓^p_q s ⇝ s : C}{step-coe-non}
$$

### composition

$$
\Rule{}{Γ ⊢ C ↓^p_p s \; [q \; 𝘄𝗶𝘁𝗵 ⋯] ⇝ s : C}{step-comp-id}
$$

$$
\Rule{}{
  Γ ⊢ A ↓^p_{p'} s \; [ε \; 𝘄𝗶𝘁𝗵 \; 0 ↪ 𝑗.s₀ \Bar 1 ↪ 𝑗.s₁] ⇝
    s_ε[p'/𝑗] : A
}{step-comp-end}
$$

### type case

$$
\Rule{Γ ⊢ e ⇝ e'}{
  Γ ⊢ 𝘁𝘆𝗰𝗮𝘀𝗲_C \; e \; [⋯] ⇝ 𝘁𝘆𝗰𝗮𝘀𝗲_C \; e' \; [⋯]
}{step-tycase-head}
$$

$$
\Rule{}{
  Γ ⊢ 𝘁𝘆𝗰𝗮𝘀𝗲_C \; 𝗯𝗼𝗼𝗹:𝒰_𝓀 \; [𝗯𝗼𝗼𝗹 ↪ s \Bar ⋯] ⇝ s : C \\
  \begin{split}
  Γ ⊢ 𝘁𝘆𝗰𝗮𝘀𝗲_C \; ((x : A) → B) : 𝒰_𝓀 \; [Π \; x \; y ↪ s \Bar ⋯] \\
    {} ⇝ s[(A:𝒰_𝓀)/x, ((λx. B) : 𝒰_𝓀 → 𝒰_𝓀)/y] : C
  \end{split} \\
  \text{etc}
}{step-tycase-bool; etc}
$$

### annotation

$$
\Rule{}{Γ ⊢ \E e : A ⇝ e}{step-ann-nest}
\qquad
\Rule{Γ ⊢ e ⇝ e'}{Γ ⊢ s : \E e ⇝ s : \E{e'}}{step-ann-ty}
$$


:::rulebox
$$ \IN Γ ⊢ 𝐭𝐲 \; \IN e ↦ \OUT A $$
:::

## compute elim type {#compute-ty}

assumes $Ψ \Bar Γ ⊢ e ⇒ A$ for some $Ψ$, and just recovers the $A$ without
doing any other checking.

:::aside
yeah. im trying to remove it

- __why not just pass the type in?__ \
  that gets you e.g. the type of $f \; s$, but that isn't enough information to
  know the type of $f$
:::

$$ \Rule{(x : A) ∈ Γ}{Γ ⊢ 𝐭𝐲 \; x ↦ A}{rety-var} $$

$$
\Rule{
  Γ ⊢ 𝐭𝐲 \; f ↦ (x : A) → B
}{
  Γ ⊢ 𝐭𝐲 (f \; s) ↦ B[(s:A)/x]
}{rety-app}
\qquad
\Rule{
  Γ ⊢ 𝐭𝐲 \; e ↦ (x : A) × B
}{
  Γ ⊢ 𝐭𝐲 (𝗳𝘀𝘁 \; e) ↦ A \\
  Γ ⊢ 𝐭𝐲 (𝘀𝗻𝗱 \; e) ↦ B[(𝗳𝘀𝘁 \; e)/x]
}{rety-\{fst,snd\}}
$$

$$
\Rule{
  Γ ⊢ 𝐭𝐲 \; f ↦ 𝗘𝗾_{𝑖.A} \; s \; t
}{
  Γ ⊢ 𝐭𝐲 (f \; p) ↦ A[p/𝑖]
}{rety-dapp}
\qquad
\Rule{}{
  Γ ⊢ 𝐭𝐲 (𝗶𝗳_{x.A} \; e \; 𝘁𝗵𝗲𝗻 \; s \; 𝗲𝗹𝘀𝗲 \; t) ↦ A[e/x]
}{rety-if}
$$

$$
\Rule{}{
  Γ ⊢ 𝐭𝐲 ([𝑖.C] ↓^p_q s) ↦ C[q/𝑖]
}{rety-coe}
\qquad
\Rule{}{
  Γ ⊢ 𝐭𝐲 (A ↓^p_{p'} s \; [q \; 𝘄𝗶𝘁𝗵 ⋯]) ↦ A
}{rety-comp}
$$

$$
\Rule{}{
  Γ ⊢ 𝐭𝐲 (𝘁𝘆𝗰𝗮𝘀𝗲_A \; e \; [⋯]) ↦ A
}{rety-tycase}
$$


# references {#refs}