Nominal type theory

Nullary parametricity (arity 0) is a form of nominal type theory: its intended model is the “constructive Schanuel topos” over a base, consisting of presheaves on the category of finite sets and monomorphisms. From the nominal perspective, an n-dimensional term is regarded as depending on n variables or “names”, with rel acting as weakening and sym permuting the names. Thus we generally combine -arity 0 with -direction w,wk for weakening.

It is curious that observational nullary parametricity gives us something akin to a “nominal” type theory without any explicit reference to names at all. Rather, the dimension of an object indicates how many “names” it depends on, and permutation of those names is accomplished explicitly by sym and other permutations. For example, the fresh quantifier И of nominal type theory can be defined using Higher coinductive types:

def И (A : Type) : Type ≔ codata [
| x .subst.w : A .
]

Intuitively, И A is the type of terms of A that “bind” a dependence on one additional fresh name. Accordingly, if we have an element a : wk (И A) . in the context of an additional name, then a .subst : wk A . is an element of A depending only on this same additional name, in which that name has been “substituted” for the fresh name bound in a. And if we have b : (И A)⁽ʷʷ⁾ . . depending on two additional names, we have both b .subst.1 : A⁽ʷʷ⁾ . . and b .subst.2 : A⁽ʷʷ⁾ . ., which respectively substitute each of the additional names for the fresh one bound in b.