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