# 用户: 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:N→N$ computes Fibonacci numbers, and $p:F=F$ is a variable, then $i:I⊢p(i)(6)$ is a neutral form, but it is no longer neutral when we substitute $i↦0$, since it then computes to $F(6)=8$. The frontier of instability is an element of $ϕ:F$ (recall that this is just a formula like $(i=0)∨(j=1)$ specifying a face of the cube) in which neutral forms ‘decays’ and becomes reducible.

We use $Γ⊢a:_{nf}A$ and $Γ⊢Anf type$ for normal forms, $Γ⊢a:_{ne}A$ for neutral forms. Effectively, we are defining two types $Normal(Γ,A),Neutral(Γ,A,ϕ)$ 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.$Γ⊢x:_{ne}A(x:A)∈Γ $Usual types don’t change apart from preserving the frontier of instability annotation.$Γ⊢∑_{x:A}Bnf typeΓ⊢Anf typeΓ,x:A⊢Bnf type Γ⊢∏_{x:A}Bnf typeΓ⊢Anf typeΓ,x:A⊢Bnf type $Note that types of normal forms are not required to be normal. So $A$ below is silently supposed to be $Γ⊢Atype$.$Γ⊢(a,b):_{nf}∑_{x:A}BΓ⊢a:_{nf}AΓ⊢b:_{nf}B[x/a] Γ⊢π_{1}(p):_{ne}AΓ⊢p:_{ne}∑_{x:A}B Γ⊢π_{2}(p):_{ne}B[x/π_{1}(p)]Γ⊢p:_{ne}∑_{x:A}B $$Γ⊢λx.b:_{nf}∏_{x:A}BΓ,x:A⊢b:_{nf}B Γ⊢f(a):_{ne}B[x/a]Γ⊢f:_{ne}∏_{x:A}BΓ⊢a:_{nf}A $Path types change the frontier, naturally. We only write out non-dependent paths for simplicity. We use $a=b$ for paths, and $a≡b$ for judgemental equalities.$Γ⊢a_{1}=a_{2}nf typeΓ⊢Anf typeΓ⊢a_{1},a_{2}:_{nf}A Γ⊢λi.a:_{nf}a[i/0]=a[i/1]Γ,i:I⊢a:_{nf}A $$Γ⊢p(i):_{ne}AΓ⊢p:_{ne}a_{1}=a_{2}Γ⊢i:I $The above are *extensional* types in that neutral forms of these types are never normal because we can $η$-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.$Γ⊢Ansnf type Γ⊢yes:_{nf}Ans Γ⊢no:_{nf}Ans $$Γ⊢↑(a,a~):_{nf}AnsΓ⊢a:_{ne}AnsΓ,ϕ⊢a~:_{nf}AnsΓ,ϕ⊢a~=a:Ans $Compare this with the rule in MLTT:$Γ⊢↑(a):_{nf}AnsΓ⊢a:_{ne}Ans $This $↑$ 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.$Γ⊢a:_{ne}AΓ⊢ϕΓ⊢a:A Γ⊢(path constructor in metatheory)a≡a_{0} :_{ne}AΓ⊢ϕΓ⊢a:_{ne}AΓ⊢a_{0}:AΓ⊢a≡a_{0} (judgemental eq.) :A $$Γ⊢↑(a,a~)≡a~:_{nf}AnsΓ⊢ϕΓ⊢a:AnsΓ⊢a~:_{nf}AnsΓ⊢a~≡a:Ans $Also, there is an implicit conversion operation that turns neutral forms $Γ⊢a:_{ne}A$ (in other words, elements of the inductive type $Neutral(Γ,A,ϕ)$) into terms $Γ⊢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

(...) $F$-locality?