Sort (Inductive Inductive Type)

Definition

In the theory of inductive-inductive types, a sort is one of the mutually defined type formers. An inductive-inductive definition is formally specified by a signature consisting of a context of sorts followed by a context of constructors.

Context of Sorts

The sorts of an inductive-inductive type form a telescope. Each subsequent sort may depend on the previously defined sorts. If we denote the universe of types by $U$, a context of sorts is a valid typing context where each type is formed using $U$ and the preceding variables.

For a signature with $n$ sorts, the context of sorts is given by:

$x_1:U,x_2:A_2(x_1),\dots ,x_n:A_n(x_1,\dots ,x_{n-1})$

where each $A_i$ is a type family constructed from the preceding sorts.

Example

When defining the syntax of dependent type theory as an inductive-inductive type, the sorts represent the distinct syntactic categories. We define contexts and types over contexts. The sorts are given by the telescope:

$\text{Con}:U,\text{Ty}:\text{Con}\to U$

Here, $\text{Con}$ is the first sort, and $\text{Ty}$ is the second sort, which depends on the first. The constructors for contexts and types are then defined over this context of sorts.

References

• Forsberg, F. N. (2013). Inductive-inductive definitions. PhD thesis, Swansea University.

• Kaposi, A., & Kovács, A. (2018). A syntax for mutual inductive families. Proceedings of the ACM on Programming Languages.