## Links * [Eric's talk](https://www.youtube.com/watch?v=hlCVHVtAlqQ) * [Eric's formalisation in agda](https://github.com/ericfinster/higher-alg) ## Introduction 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$