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

Showing changes from revision #0 to #1: Added | Removed | Changed

## 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$

Revision on December 6, 2018 at 18:15:30 by Ali Caglayan. See the history of this page for a list of all contributions to it.