Free Extension Semantics

Idea

Free extension semantics is the method used in altenkirch2016-qiit to describe quotient inductive-inductive types by building their ambient category of algebras one constructor at a time. The starting point is a base category whose objects represent previously constructed sorts together with families of sets over them. New sorts are then added by free extension: a sort signature is given by a functor into Set, and extending by that sort produces a new base category whose objects are families indexed by the values of that functor.

Path and point constructors are treated uniformly by a pair of set-valued functors. The first is an argument functor $F:\mathcal{C}\Rightarrow \mathbf{Set}$, which assigns to each partial algebra the set of inputs for the constructor. The second is a target functor $G:{\int }^{\mathcal{C}}F\Rightarrow \mathbf{Set}$ on the Grothendieck construction of $F$, which assigns the set in which the constructor lands. An algebra structure for the constructor is then a section $(x:F(X))\to G(X,x)$. In this way, both point constructors and path constructors are expressed as free extensions of the current algebra category.

Definitions

Sort specification

A specification of sorts is given by a sequence of functors

$H_i:{\mathcal{C}}_i\Rightarrow \mathbf{Set}$

built successively from previous base categories. Intuitively, $H_i$ describes the indexing data for the next sort.

Given previously constructed sorts, the extended base category has objects of the form $(X,P)$ where $X$ is an object of the previous base category and

$P:H(X)\to \mathbf{Set}.$

So an object of the extended category is an old algebra together with a family of sets over the new sort indices.

Constructor specification

A constructor specification on a base category $\mathcal{C}$ consists of:

• an argument functor

$F:\mathcal{C}\Rightarrow \mathbf{Set}$

• a target functor

$G:{\int }^{\mathcal{C}}F\Rightarrow \mathbf{Set}$

where $G$ is required to be relatively continuous over the forgetful functor from the Grothendieck construction.

The intuition is that $F(X)$ gives the constructor inputs available in an algebra $X$, while $G(X,x)$ gives the set of outputs for an input $x:F(X)$.

Category of algebras for a constructor

Given a constructor specification $(F,G)$ on $\mathcal{C}$, the corresponding category of algebras $\mathcal{C}.(F,G)$ has:

• objects $(X,\theta )$ where $X:\mathcal{C}$ and

$\theta :(x:F(X))\to G(X,x)$

• morphisms given by morphisms in $\mathcal{C}$ that preserve the constructor action.

So adding a constructor means freely extending the current category by equipping each object with a chosen operation of the required shape.

Base target functor for a new sort

If a new sort is indexed by a functor

$H:\mathcal{C}\Rightarrow \mathbf{Set},$

then in the extended category ${\mathcal{C}}^{\prime }$ an object is $(X,P)$ with $P:H(X)\to \mathbf{Set}$. The corresponding base target functor is

$U_H:{\int }^{{\mathcal{C}}^{\prime }}(H\circ V_H)\Rightarrow \mathbf{Set}$

defined by

$U_H(X,P,x)\equiv P(x).$

This is the canonical target functor for point constructors landing in the newly added sort.

Equality target functor

Path constructors are handled by an equality functor

$Eq:{\int }^{\mathbf{Set}}(\mathrm{id}\times \mathrm{id})\Rightarrow \mathbf{Set}$

given on objects by

$Eq(X,x,y)\equiv x{=}_{X}y.$

Composing this with suitable global elements of a target functor gives a target functor for path constructors. This lets equality constructors be treated in the same extension framework as point constructors.

Remarks

• The adjective “free” refers to the fact that each stage adds exactly the structure required by the next sort or constructor, with no extra equations beyond those explicitly specified.
• The use of the Grothendieck construction is what makes constructor targets dependent on both the ambient algebra and the chosen constructor arguments.
• Relative continuity is the key semantic condition ensuring that these constructor extensions preserve the limits needed for the later initial-algebra argument.
• In altenkirch2016-qiit, this iterative free-extension perspective is used to prove that the relevant categories of algebras are complete and to relate initiality to the section induction principle.

References

altenkirch2016-qiit
Quotient Inductive-Inductive Type
Grothendieck Construction
Initial Algebra