Homotopy Type Theory Eric Finster, Towards Higher Universal Algebra in Type Theory > history (Rev #1)

Links

• Eric’s talk
• Eric’s formalisation in agda

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

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$