Quotient Inductive-Inductive Types

Abstract

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types which are not sets in the sense of HoTT (i.e. do not satisfy uniqueness of equality proofs) such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define sets, such as the Cauchy reals, the partiality monad, and the well-typed syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs). Although there has been recent progress on a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite having many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics and show that this is equivalent to the section induction principle, which justifies the intuitively expected elimination rules.

Introduces free extension semantics.

Outline

Introduction

Cauchy Real Numbers can be represented as HITs

Sorts

Note on nested $\Sigma$ notation

We will use the following notation for nested $\Sigma$‘s:

• $x^{<n}$ is a vector of length $n$.
• $x_i^{<n}$ is the $(i+1{)}^{\mathrm{th}}$ element of the list (so indexing from $0$).
• $x^{<i}$ is the prefix list of $\bar{x}$ length $i$.
  Note that the type of each $x_i^{<n}$ may be determined by previous elements.

Definition 3

A specification of sorts is given by a list of functors built sequentially upon the previous categories sorts.

The base category for a sort signature $H^{<n}$ (defined below) has objects of the form of an $n$ tuple $P^{<n}$ where
$P_i:H_i(x^{<i})\to \mathbf{Set}$

is a type family for some $x^{<i}:{\mathcal{C}}_{i^{-}}$.
Morphisms are defined as $f:X\to Y$ along with $g^{<n}:P^{<n}\to Q^{<n}$ where

$$g_{i^{+}}:(x^{<n}:H_i(X))\to P_i(x)\to Q_i(H_i(f)(x))$$

The sort signature is a functor $H_i:{\mathcal{C}}_i\Rightarrow \mathbf{Set}$.
This represents how the constructor for sort $i$ depends on the previous sort.
For example, $H_1(A)=\mathrm{List}(A)$.

Theorem 10

Base categories are complete: For any sort signature, $H^{<n}$, the corresponding base category ${\mathcal{C}}_n$ has all small limits.

Algebras

Relative Continuity and Constructor Specifications

Definition 11 (Relative Continuity)

Let $\mathcal{C}$ be a category, let ${\mathcal{C}}_0$ be a complete category, and let $U:\mathcal{C}\Rightarrow {\mathcal{C}}_0$
be a functor. Given a small category $\mathcal{I}$ and a diagram $X:\mathcal{I}\Rightarrow \mathcal{C}$, a cone $A\Rightarrow X$ in $\mathcal{C}$ is a $U$-limit cone, or limit cone relative to $U$, if the induced cone $UA\Rightarrow UX$ is a limit cone in ${\mathcal{C}}_0$.
A functor $G:\mathcal{C}\Rightarrow \mathbf{Set}$ is continuous relative to $U$ if it maps $U$-limit cones to limit cones in $\mathbf{Set}$.

Definition 12 (Constructor Specification)

A constructor specification on a base category $\mathcal{C}$ is given by:

• A functor $F:\mathcal{C}\Rightarrow \mathbf{Set}$ called the argument functor.
• A relative continuous functor $G:{\int }^{\mathcal{C}}F\Rightarrow \mathbf{Set}$ called the target functor.

Definition 15 (Category of algebras)

Let $(F,G)$ be a constructor specification on a complete category $\mathcal{C}$. The category of algebras of $(F,G)$ is denoted by $\mathcal{C}.(F,G)$ and is defined as:

• objects are pairs $(X,\theta )$ where $X$ is an object of $\mathcal{C}$ and $\theta :(x:F(X))\to G(X,x)$
• morphisms $f:\mathcal{C}.(F,G)[(X,\theta ),(Y,\psi )]⟺$ $f:\mathcal{C}[X,Y]$ s.t. $\forall x:F(X).\psi (F(f)(x))=G(\bar{f})(\theta (x))$
  where $\bar{f}:(X,x)\to (Y,F(f)(x))$

Point Constructors

Let $\mathcal{C}$ be finitely complete, given a functor $H:\mathcal{C}\Rightarrow \mathbf{Set}$, let ${\mathcal{C}}^{\prime }$ be the extended base category with one more sort indexed over $H$. Then ${\mathcal{C}}^{\prime }$ has objects $(X,P)$ where $X:\mathcal{C}$ and $P:HX\to \mathrm{Set}$.
Define the base target functor corresponding to $H$ to be the functor $U_H:{\int }^{{\mathcal{C}}^{\prime }}(H\circ V_H)\Rightarrow \mathbf{Set}$, definte as:

$$U_H(X,P,x)=P(x)$$

Theorem 20 states that base target functors a relatively continuous.

Reindexing Target Functors

Path Constructors

Let $Eq:{\int }^{\mathbf{Set}}(\mathrm{id}\times \mathrm{id})\Rightarrow \mathbf{Set}$ be the functor defined on objects by:

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

And on morphisms by:

$$Eq(f,p_x,p_y):\equiv p_x\cdot \mathrm{ap}(f,-)\cdot p_y^{-1}$$

Then $Eq$ is a functor and it is the functor of fibers of a the natural transformation $\Delta :\mathrm{id}\Rrightarrow \mathrm{id}\times \mathrm{id}$.
Both $\mathrm{id}$ and $\mathrm{id}\times \mathrm{id}$ are relatively continuous (lemma 24), and because of this,
In any complete base category $\mathcal{C}$, with constructor specification $(F,G)$ (definition 12) and global elements $l,r:G$, then the map $E{q}_G(l,r):{\int }^{\mathcal{C}}F\to \mathrm{Set}$ defined by $E{q}_G(l,r)(X,x)=(l_{(X,x)}{=}_{G(X,x)}{r}_{(X,x)}$ extends to a relatively continuous functor.

Categories of Algebras are Complete

Elimination Principles

The Section Induction Principle

An object $X$ of a category $\mathcal{C}$ is section inductive if for ever $Y$ of $\mathcal{C}$ and morphism $p:\mathcal{C}[Y,X]$, there exists $s:\mathcal{C}[X,Y]$

Initiality, and its relation to the Section Induction Principle

Conclusions and Further Work

Definitions

Higher Inductive Type
Quotient Inductive Type
Quotient Inductive-Inductive Types
Cauchy Real Numbers
Axiom of Choice

Paper