altenkirch2016-qiit

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.

Outline

Introduction

Cauchy Real Numbers can be represented as HITs

Example 1

Mobile

Example 2

ConTy with ${\sigma }_{\mathrm{eq}}$

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

TODO 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 \mathrm{Set}$

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

$$g_{i^{+}}:\Pi x^{<n}:H_i((P_j{)}_{j<i}).P_{i}x\to Q_i(H_i((f_j{)}_{j<i})(x)$$

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

Algebras

Relative Continuity and Constructor Specifications

Point Constructors

Reindexing Target Functors

Categories of Algebras are Complete

Elimination Principles

The Section Induction Principle

Initiality, and its relation to the Section Inductionm Principle

Conclusions and Further Work

Definitions

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

Paper

Quotient Inductive-Inductive Types