#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 is 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} [[nLab:Eric Finster]] ([[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 ([recording](https://www.youtube.com/watch?v=hlCVHVtAlqQ)) * [[nLab:Agda]] code at: [github.com/ericfinster/higher-alg](https://github.com/ericfinster/higher-alg) * [[nlab:John Baez]], [[nlab:James Dolan]], _Higher-dimensional Algebra and Topological Quantum Field Theory_, [arXiv:q-alg/9503002](https://arxiv.org/pdf/q-alg/9503002.pdf) # Towards Higher Universal Algebra in Type Theory Collecting the definitions and trying them out here. The idea is to go through the definitions in the talk and the definitions in the agda formalisation to play around with. ## Polynomials **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. ## Trees A polynomial $P : \Poly I$ generates an assocaiated type of trees. **Definition** The inductive family $\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 : (j : J) \to (p : \Param (f, j)) \to \Tr(P, j)) \to \Tr(P, i)$ ## Leave and Nodes For a tree $w : \Tr (P, i)$, we will need its type of leaves and type of nodes **Definition** * $\Leaf : (i : I) \to (w : \Tr i) \to I \to \mathcal{U}$ * $\Leaf (\lf i) j := (i = j)$ * $\displaystyle\Leaf (\nd(f, \phi))j := \sum_{k : I} \sum_{p : \Param (f, k)} \Leaf(\phi (k, p)) j$