Homotopy Type Theory Eric Finster, Towards Higher Universal Algebra in Type Theory > history (Rev #15, changes)

Idea

While homotopy type theory formalizes homotopy theory, it is not a priori clear – and in fact is or was an open problem – how to formalize general homotopy-coherent structures of higher algebra/higher category theory: Since these typically involve an infinite hierarchy of coherence-conditions, these cannot be axiomatized directly, but one needs some scheme that generates them. This turned out to be subtle.

Eric Finster had previously considered another variant of type theory, called opetopic type theory which natively talks about infinity-categories and their higher coherences by type-theoretically formalizing the structure of opetopic sets. In new work Finster 18 he gives something like an implementation of aspects of opetopic type theory within homotopy type theory and provides evidence that this yields a tool to solve the general problem of coherences of higher algebra/higher category theory within homotopy type theory.

Polynomials serve as a notion of “higher signature”. Following ideas from the categorical approach to universal algebra, we are going to encode the relations or axioms of our structure using a monadic multiplication on P.

References

• Eric Finster, Towards Higher Universal Algebra in Type Theory, Homotopy Type Theory Electronic Seminar 2018 (compact pdf slides, original pdf slides, recording)

• Agda code at: github.com/ericfinster/higher-alg

• Notes on a definition of higher structure.

The idea of opetopic sets that Finster 18 is inspired by goes back to

• John Baez, James Dolan, Higher-Dimensional Algebra III: n-Categories and the Algebra of Opetopes, arXiv:q-alg/9702014

Eric’s talk

In Eric’s Agda formalisation and talk, a polynomial has its parameter sorts encoded with the parameter. We will follow a suggestion by Mike to have a $\SortOf$ function instead. This should make some definitions less cluttered.

Let $I : \mathcal{U}$ be a type of sorts. A polynomial over $I$ consists of the following data:

• A family of operations $\Op : I \to \mathcal{U}$
• For each operation, a family of parameters $\Param_i : (f : \Op i) \to \mathcal{U}$
• A function $\SortOf : (f : \Op i) \to \Param f \to I$

We define the type of operations of a polynomial $P$ as:

A polynomial $P : \Poly I$ generates a type of trees:

The inductive famiy $\Tr_P : I \to \mathcal{U}$ has constructors

• $\lf : (i : I) \to \Tr_P i$
• $\nd : (i : I) \to (f : \Op_P i) \to (\phi : (p : \Param f) \to \Tr_P (\SortOf(f,p))) \to \Tr_P i$

For a tree $w : \Tr_P i$ we define its type of leaves by induction on $w$.

• $\Leaf( (\lf i), j) \equiv (i =_I j)$
• $\Leaf( \nd (f, \phi), j) \equiv \sum_{p : \Param f} \Leaf(\phi(p), j)$

and its type of nodes:

• $\Nodes(\lf i, jg) \equiv \mathbf{0}$
• $\Nodes(\nd(f,\phi), jg) \equiv ((i,f) = jg) + \sum_{p : \Param f} \Node(\phi(p), jg)$

Let $w : \Tr_i P$ be a tree and $f : Op_P i$ an operation. A frame from $w$ to $f$ is an equivalence:

i.e. the type of leaves of the tree is equivalent to the type of parameters of the operator.

A polynomial relation for $P$ is a type family:

Let $P : \Poly I$ and let $R$ be a relation on $P$. The slice of $P$ by $R$, denoted $P // R$, is the polynomial with sorts $\Ops$ defined as follows:

TODO: Continue writing this out. Essentially following this coq file

Definitions and Examples

Here we collect the definitions and ideas that were given in Eric’s talk. We can also use the Agda formalisation for reference too.

A polynomial $P : \Poly I$ generates an associated type of trees.

For a tree $w : \Tr (P, i)$, we will need its type of leaves and type of nodes