# 用户: 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 computes Fibonacci numbers, and is a variable, then is a neutral form, but it is no longer neutral when we substitute , since it then computes to . The frontier of instability is an element of (recall that this is just a formula like specifying a face of the cube) in which neutral forms ‘decays’ and becomes reducible.

We use and for normal forms, for neutral forms. Effectively, we are defining two types 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.Usual types don’t change apart from preserving the frontier of instability annotation.Note that types of normal forms are not required to be normal. So below is silently supposed to be .Path types change the frontier, naturally. We only write out non-dependent paths for simplicity. We use for paths, and for judgemental equalities.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.Compare this with the rule in MLTT: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.Also, there is an implicit conversion operation that turns neutral forms (in other words, elements of the inductive type ) into terms . 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

(...) -locality?