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

Showing changes from revision #7 to #8: Added | Removed | Changed

## 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 is yields a tool to solve the general problem of coherences of higher algebra/higher category theory within homotopy type theory.

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

## Eric’s talk

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

###### Definition

Fix a type $I$ of sorts. A polynomial over $I$, $\Poly I$, is the data of

• A family of operations $\Op : I \to \mathcal{U}$
• For each operation, for each $i : I$, a family of sorted parameters
$\Param_i : (f : \Op i) \to I \to \mathcal{U}$
###### Remark
• For $i : I$, an element $f: \Op i$ represents an operation whose output sort is $i$.

• For $f : \Op i$ and $j : I$, and element $p : \Param_i(f, j)$ represents an input parameter of sort $j$.

• The $\Op i$ and $\Param_i (f, j)$ are not truncated at set level. So operations and parameters can have higher homotopy.

• In HoTT book notation, we can write the previous definition as:

$\Poly I \equiv \sum_{\Op : I \to \mathcal{U}}\prod_{i : I} \Param_i$
$\Param_i \equiv \prod_{f : \Op i}I \to \mathcal{U}$

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

###### Example

We start with the simplest non-trivial example, when $I \equiv \mathbf{1}$ the unit type?. Looking at $\Poly \mathbf{1}$ we clearly have $\Op : \mathbf{1} \to \mathcal{U}\simeq \mathcal{U}$. So $\Op$ is simply a type. Next we have $\Param : (f : \Op) \to \mathbf{1} \to \mathcal{U}\simeq \Op \to \mathcal{U}$ so $\Param$ is just a family of types indexed over the type $\Op$.

Now if $\Op \equiv \Fin_3$ then there would be 3 operations. Take one of these operations and call it $o_1$, $\Param$ would then have to chose what the type of parameters should be, let’s choose $\Fin_2$. This would mean that $o_1$ would be an operation ($o_1 : \Op$) with two parameters $p : \Fin_2 \equiv \Param o_1$. Note $o_1$ is very much like the operator in an abstract syntax tree in this case.

When the type of sorts $I$ gets more structure, the objects we discuss get complicated quickly. Even letting $\Param o_1$ be some arbitrary type gives us an interesting object.

###### Definition

The type of trees associated to a polynomial $P : \Poly I$ is an inductive family? $\Tr P : I \to \mathcal{U}$ that has constructors

• $\lf : (i : I) \to \Tr(P, i)$
• $\nd : (i : I) \to (f : \Op(P,i)) \to (\phi : (j : I) \to (p : \Param_i (f, j)) \to \Tr(P, j)) \to \Tr(P, i)$

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

###### Definition

The type of trees associated to a polynomial $P : \Poly I$ is an inductive family? $\Tr P : I \to \mathcal{U}$ that has constructors

• $\lf : (i : I) \to \Tr(P, i)$
• $\nd : (i : I) \to (f : \Op(P,i)) \to (\phi : (j : I) \to (p : \Param_i (f, j)) \to \Tr(P, j)) \to \Tr(P, i)$
###### Definition

The type of leaves of a tree $P : \Poly I$ is given by:

• $\Leaf : (i : I) \to (w : \Tr i) \to I \to \mathcal{U}$
• $\Leaf_i((\lf i), j) \equiv (i = j)$
• $\displaystyle\Leaf_i ( \nd(f, \phi),j) \equiv \sum_{k : I} \sum_{p : \Param (f, k)} \Leaf_i ((\phi (k, p)), j)$

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

###### Definition

The type of nodes leaves of a tree $P : \Poly I$ is given by:

•  \Node \Leaf : (i : I) \to (w : \Tr i) \to (j I : I) \to \Op \mathcal{U} j \to \Type
•  \Node_i \Leaf_i((\lf ((\lf i), j, j) g) \equiv \mathbf{0} (i = j)
•  \displaystyle \displaystyle\Leaf_i \Node_i ( (\nd(f,\phi),j,g) \nd(f, \phi),j) \equiv ((i,f)=(j,g)) + \sum_{k : I} \sum_{p : \Param(f,k)} \Param \Node_i (f, ( k)} \phi( \Leaf_i j, ((\phi p), (k, j, p)), g) j)
###### Definition
• Let $P : \Poly I$ be a polynomial $w : \Tr(P,i)$ a tree and $f : \Op(P,i)$ an operation. A frame from $w$ to $f$ is a family of equivalences?
$(j:I) \to \Leaf_i(w,j) \simeq \Param(P,f,j)$

The type of nodes of a tree $P : \Poly I$ is given by:

• $\Node : (i : I) \to (w : \Tr i) \to (j : I) \to \Op j \to \Type$
• $\Node_i ((\lf i), j, g) \equiv \mathbf{0}$
• $\displaystyle \Node_i (\nd(f,\phi),j,g) \equiv ((i,f)=(j,g)) + \sum_{k : I} \sum_{p : \Param(f,k)} \Node_i ( \phi( j, p), j, g)$
###### Definition
• Let $P : \Poly I$ be a polynomial $w : \Tr(P,i)$ a tree and $f : \Op(P,i)$ an operation. A frame from $w$ to $f$ is a family of equivalences?
$(j:I) \to \Leaf_i(w,j) \simeq \Param(P,f,j)$

Revision on December 7, 2018 at 13:37:28 by Ali Caglayan. See the history of this page for a list of all contributions to it.