## Contents * table of contents {:toc} ## Idea While [[nLab:homotopy type theory]] formalizes [[nLab:homotopy theory]], it is not a priori clear -- and in fact is or was an open problem -- how to formalize general homotopy-[[nLab:coherence|coherent]] [[nLab:structures]] of [[nLab:higher algebra]]/[[nLab:higher category theory]]: Since these typically involve an _infinite_ hierarchy of [[nLab:coherence]]-conditions, these cannot be [[nLab:axiom|axiomatized]] directly, but one needs some scheme that generates them. This turned out to be subtle. [[nLab:Eric Finster]] had previously considered another variant of [[nLab:type theory]], called _[[nLab:opetopic type theory]]_ which natively talks about [[nLab:infinity-categories]] and their higher [[nLab:coherences]] by type-theoretically formalizing the [[nLab:structure]] of [[nLab:opetopic sets]]. In new work [Finster 18](#Finster2018) he gives something like an implementation of aspects of [[nLab:opetopic type theory]] _within_ [[nLab:homotopy type theory]] and provides evidence that this yields a tool to solve the general problem of [[nLab:coherences]] of [[nlab:higher algebra]]/[[nLab:higher category theory]] within [[nLab:homotopy type theory]]. ## References {#Link} * {#Finster2018} [[Eric Finster]], _Towards Higher Universal Algebra in Type Theory_, [Homotopy Type Theory Electronic Seminar](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html) 2018 ([pdf slides](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Finster-2018-12-6-HoTTEST.pdf), [recording](https://www.youtube.com/watch?v=hlCVHVtAlqQ)) * [[nLab:Agda]] code at: [github.com/ericfinster/higher-alg](https://github.com/ericfinster/higher-alg) The idea of [[nLab:opetopic sets]] that [Finster 18](#Finster2018) is inspired by goes back to * [[nlab:John Baez]], [[nlab:James Dolan]], _Higher-Dimensional Algebra III: n-Categories and the Algebra of Opetopes_, [arXiv:q-alg/9702014](https://arxiv.org/abs/q-alg/9702014) ## 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. +-- {: .num_defn} ###### Definition Fix a [[type]] $I$ of sorts. A **polynomial** over $I$, $\Poly I$, is the data of * A [[type family|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}$$ =-- +-- {: .num_remark} ###### 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}$$ =-- +-- {: .num_remark} ###### 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. =-- A polynomial $P : \Poly I$ generates an associated type of trees. +-- {: .num_defn} ###### 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)$ =-- For a tree $w : \Tr (P, i)$, we will need its type of leaves and type of nodes +-- {: .num_defn} ###### 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)$ =-- +-- {: .num_defn} ###### Definition 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) $ =-- +-- {: .num_defn} ###### 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)$$ =--