blog/posts-wip/algorithmic-xtt.md

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

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

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

 \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

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

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

reduce the expected type to whnf 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.

 \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. 🧅 :::

$$ \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

 \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

$$ \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

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

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

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

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 subsingleton (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

:::rulebox

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

:::

terms

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

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

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