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 of sorts. A polynomial over , , is the data of
A family of operations $$
For each operation, for each , a family of sorted parameters
Remark
For , an element represents an operation whose output sort is .
For and , and element represents an input parameter of sort .
The and are not truncated at set level. So operations and parameters can have higher homotopy.
Trees
A polynomial generates an assocaiated type of trees.
Definition The inductive family has constructors
Leave and Nodes
For a tree , we will need its type of leaves and type of nodes
Definition
Revision on December 6, 2018 at 23:15:30 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.