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


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.


Definition Fix a type II of sorts. A polynomial over II, PolyI\Poly I, is the data of

  • A family of operations $Op:I→𝒰\Op : I \to \mathcal{U}$
  • For each operation, for each i:Ii : I, a family of sorted parameters
Param i:(f:Opi)β†’I→𝒰\Param_i : (f : \Op i) \to I \to \mathcal{U}


  • For i:Ii : I, an element f:Opif: \Op i represents an operation whose output sort is ii.

  • For f:Opif : \Op i and j:Ij : I, and element p:Param ifjp : \Param_i f\, j represents an input parameter of sort jj.

  • The Opi\Op i and Param ifj\Param_i f\, j are not truncated at set level. So operations and parameters can have higher homotopy.


A polynomial P:PolyIP : \Poly I generates an assocaiated type of trees.

Definition The inductive family TrP:I→𝒰\Tr P : I \to \mathcal{U} has constructors

  • lf:(i:I)β†’TrPI\lf : (i : I) \to \Tr P\, I
  • nd:(i:I)β†’(f:OpPi)β†’(Ο•:(j:J)β†’(p:Paramfj)β†’TrPj)β†’TrPi\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:TrPiw : \Tr P\, i, we will need its type of leaves and type of nodes


  • Leaf:(i:I)β†’(w:Tri)β†’I→𝒰\Leaf : (i : I) \to (w : \Tr i) \to I \to \mathcal{U}
  • Leaf(lfi)j:=(i=j)\Leaf (\lf i) j := (i = j)
  • Leaf(nd(f,Ο•))j:=βˆ‘ k:Iβˆ‘ p:ParamfkLeaf(Ο•kp)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.