用户: Trebor/Normal Forms in Cubical Type Theory

As usual, normal forms are defined mutually inductively with neutral forms. However, neutral forms are parametrized with a frontier of instability. For example, if $F:\mathbb{N}\to \mathbb{N}$ computes Fibonacci numbers, and $p:F=F$ is a variable, then $i:\mathbb{I}⊢p(i)(6)$ is a neutral form, but it is no longer neutral when we substitute $i\mapsto 0$, since it then computes to $F(6)=8$. The frontier of instability is an element of $\varphi :\mathbb{F}$ (recall that this is just a formula like $(i=0)\vee (j=1)$ specifying a face of the cube) in which neutral forms ‘decays’ and becomes reducible.

We use $\Gamma ⊢a{:}_{\text{nf}}A$ and $\Gamma ⊢A\text{nf type}$ for normal forms, $\Gamma ⊢a{:}_{\text{ne}}^{\varphi }A$ for neutral forms. Effectively, we are defining two types $\text{Normal}(\Gamma ,A),\text{Neutral}(\Gamma ,A,\varphi )$ as mutually quotient-inductive types.

Remark 0.1. It is unusual to define normal forms as quotient-inductive types, because normal forms are exactly there to get rid of quotient equalities. However, these quotients doesn’t make anything hard to decide algorithmically, so we give them a pass.

The rest of this comes from a transcription of J. Sterling’s thesis, §7.2. Variables are never unstable.$$\frac{(x:A)\in \Gamma }{\Gamma ⊢x{:}_{\text{ne}}^{0=1}A}$$Usual types don’t change apart from preserving the frontier of instability annotation.$$\frac{\Gamma ⊢A\text{nf type}\Gamma ,x:A⊢B\text{nf type}}{\Gamma ⊢{\sum }_{x:A}B\text{nf type}}\frac{\Gamma ⊢A\text{nf type}\Gamma ,x:A⊢B\text{nf type}}{\Gamma ⊢{\prod }_{x:A}B\text{nf type}}$$Note that types of normal forms are not required to be normal. So $A$ below is silently supposed to be $\Gamma ⊢A\text{type}$.$$\frac{\Gamma ⊢a{:}_{\text{nf}}A\Gamma ⊢b{:}_{\text{nf}}B[x/a]}{\Gamma ⊢(a,b){:}_{\text{nf}}{\sum }_{x:A}B}\frac{\Gamma ⊢p{:}_{\text{ne}}^{\varphi }{\sum }_{x:A}B}{\Gamma ⊢{\pi }_1(p){:}_{\text{ne}}^{\varphi }A}\frac{\Gamma ⊢p{:}_{\text{ne}}^{\varphi }{\sum }_{x:A}B}{\Gamma ⊢{\pi }_2(p){:}_{\text{ne}}^{\varphi }B[x/{\pi }_1(p)]}$$$$\frac{\Gamma ,x:A⊢b{:}_{\text{nf}}B}{\Gamma ⊢\lambda x.b{:}_{\text{nf}}{\prod }_{x:A}B}\frac{\Gamma ⊢f{:}_{\text{ne}}^{\varphi }{\prod }_{x:A}B\Gamma ⊢a{:}_{\text{nf}}A}{\Gamma ⊢f(a){:}_{\text{ne}}^{\varphi }B[x/a]}$$Path types change the frontier, naturally. We only write out non-dependent paths for simplicity. We use $a=b$ for paths, and $a\equiv b$ for judgemental equalities.$$\frac{\Gamma ⊢A\text{nf type}\Gamma ⊢a_1,a_2{:}_{\text{nf}}A}{\Gamma ⊢a_1=a_2\text{nf type}}\frac{\Gamma ,i:\mathbb{I}⊢a{:}_{\text{nf}}A}{\Gamma ⊢\lambda i.a{:}_{\text{nf}}a[i/0]=a[i/1]}$$$$\frac{\Gamma ⊢p{:}_{\text{ne}}^{\varphi }{a}_1=a_2\Gamma ⊢i:\mathbb{I}}{\Gamma ⊢p(i){:}_{\text{ne}}^{\varphi \vee (i=0)\vee (i=1)}A}$$The above are extensional types in that neutral forms of these types are never normal because we can $\eta$-expand. For intensional types, neutral forms are also normal. But since there is a frontier of instability, we must stablize them before converting a neutral into a normal.$$\frac{}{\Gamma ⊢\text{Ans}\text{nf type}}\frac{}{\Gamma ⊢\text{yes}{:}_{\text{nf}}\text{Ans}}\frac{}{\Gamma ⊢\text{no}{:}_{\text{nf}}\text{Ans}}$$$$\frac{\Gamma ⊢a{:}_{\text{ne}}^{\varphi }\text{Ans}\Gamma ,\varphi ⊢\tilde{a}{:}_{\text{nf}}\text{Ans}\Gamma ,\varphi ⊢\tilde{a}=a:\text{Ans}}{\Gamma ⊢\uparrow (a,\tilde{a}){:}_{\text{nf}}\text{Ans}}$$Compare this with the rule in MLTT:$$\frac{\Gamma ⊢a{:}_{\text{ne}}^{}\text{Ans}}{\Gamma ⊢\uparrow (a){:}_{\text{nf}}\text{Ans}}$$This $\uparrow$ represents the coercion of neutral forms into normal forms, and is usually implicit in presentations.

In addition, if a neutral form is unstable, we quotient it away so that it doesn’t lead to any redundant information. But note that this is only a path constructor of the quotient inductive type of neutrals, and it does not concern the original syntax.$$\frac{\Gamma ⊢\varphi \Gamma ⊢a:A}{\Gamma ⊢a{:}_{\text{ne}}^{\varphi }A}\frac{\Gamma ⊢\varphi \Gamma ⊢a{:}_{\text{ne}}^{\varphi }A\Gamma ⊢a_0:A\Gamma ⊢\stackrel{\text{(judgemental eq.)}}{\overbrace{a\equiv a_0}}:A}{\Gamma ⊢\underset{\text{(path constructor in metatheory)}}{\underbrace{a\equiv a_0}}{:}_{\text{ne}}^{\varphi }A}$$$$\frac{\Gamma ⊢\varphi \Gamma ⊢a:\text{Ans}\Gamma ⊢\tilde{a}{:}_{\text{nf}}\text{Ans}\Gamma ⊢\tilde{a}\equiv a:\text{Ans}}{\Gamma ⊢\uparrow (a,\tilde{a})\equiv \tilde{a}{:}_{\text{nf}}\text{Ans}}$$Also, there is an implicit conversion operation that turns neutral forms $\Gamma ⊢a{:}_{\text{ne}}^{\varphi }A$ (in other words, elements of the inductive type $\text{Neutral}(\Gamma ,A,\varphi )$) into terms $\Gamma ⊢a:A$. This conversion need to map equal neutral forms into judgementally equal terms. Similarly there is a function converting normal forms into terms. They are inductively defined together with all the normal and neutral forms.

(...) hcomp, stuck hcomp, universes are tedious

(...) $\mathbb{F}$-locality?