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

Contents

Idea

While homotopy type theory formalizes homotopy theory, it is not a priori clear – and in fact is or was an open problem – how to formalize general homotopy-coherent structures of higher algebra/higher category theory: Since these typically involve an infinite hierarchy of coherence-conditions, these cannot be axiomatized directly, but one needs some scheme that generates them. This turned out to be subtle.

Eric Finster had previously considered another variant of type theory, called opetopic type theory which natively talks about infinity-categories and their higher coherences by type-theoretically formalizing the structure of opetopic sets. In new work Finster 18 he gives something like an implementation of aspects of opetopic type theory within homotopy type theory and provides evidence that this yields a tool to solve the general problem of coherences of higher algebra/higher category theory within homotopy type theory.

Polynomials serve as a notion of “higher signature”. Following ideas from the categorical approach to universal algebra, we are going to encode the relations or axioms of our structure using a monadic multiplication on P.

The idea of opetopic sets that Finster 18 is inspired by goes back to

Eric’s talk

In Eric’s Agda formalisation and talk, a polynomial has its parameter sorts encoded with the parameter. We will follow a suggestion by Mike to have a SortOf\SortOf function instead. This should make some definitions less cluttered.

Let I:𝒰I : \mathcal{U} be a type of sorts. A polynomial over II consists of the following data:

  • A family of operations Op:I𝒰\Op : I \to \mathcal{U}
  • For each operation, a family of parameters Param i:(f:Opi)𝒰\Param_i : (f : \Op i) \to \mathcal{U}
  • A function SortOf:(f:Opi)ParamfI\SortOf : (f : \Op i) \to \Param f \to I

We define the type of operations of a polynomial PP as:

Ops i:IOp Pi \Ops \equiv \sum_{i : I} \Op_P i

A polynomial P:PolyIP : \Poly I generates a type of trees:

The inductive famiy Tr P:I𝒰\Tr_P : I \to \mathcal{U} has constructors

  • lf:(i:I)Tr Pi\lf : (i : I) \to \Tr_P i
  • nd:(i:I)(f:Op Pi)(ϕ:(p:Paramf)Tr P(SortOf(f,p)))Tr Pi\nd : (i : I) \to (f : \Op_P i) \to (\phi : (p : \Param f) \to \Tr_P (\SortOf(f,p))) \to \Tr_P i

For a tree w:Tr Piw : \Tr_P i we define its type of leaves by induction on ww.

Leaf i:(w:Tr Pi)I𝒰 \Leaf_i : (w : Tr_P i) \to I \to \mathcal{U}
  • Leaf((lfi),j)(i= Ij)\Leaf( (\lf i), j) \equiv (i =_I j)
  • Leaf(nd(f,ϕ),j) p:ParamfLeaf(ϕ(p),j)\Leaf( \nd (f, \phi), j) \equiv \sum_{p : \Param f} \Leaf(\phi(p), j)

and its type of nodes:

Node i:(w:Tr Pi)Ops𝒰 \Node_i : (w : \Tr_P i) \to \Ops \to \mathcal{U}
  • Nodes(lfi,jg)0\Nodes(\lf i, jg) \equiv \mathbf{0}
  • Nodes(nd(f,ϕ),jg)((i,f)=jg)+ p:ParamfNode(ϕ(p),jg)\Nodes(\nd(f,\phi), jg) \equiv ((i,f) = jg) + \sum_{p : \Param f} \Node(\phi(p), jg)

Let w:Tr iPw : \Tr_i P be a tree and f:Op Pif : Op_P i an operation. A frame from ww to ff is an equivalence:

Frame(w,f) j:ILeaf(w,j)Param i(f)\Frame(w,f) \equiv \sum_{j:I} \Leaf(w,j) \simeq \Param_i(f)

i.e. the type of leaves of the tree is equivalent to the type of parameters of the operator.

A polynomial relation for PP is a type family:

R:i:I(f:Opi)(w:Tri)(α:Frame(w,f))𝒰 R :{i : I} \to (f : \Op i) \to (w : \Tr i) (\alpha : \Frame(w,f)) \to \mathcal{U}

Let P:PolyIP : \Poly I and let RR be a relation on PP. The slice of PP by RR, denoted P//RP // R, is the polynomial with sorts Ops\Ops defined as follows:

TODO: Continue writing this out. Essentially following this coq file

Definitions and Examples

Here we collect the definitions and ideas that were given in Eric’s talk. We can also use the Agda formalisation for reference too.

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}
Remark
  • 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 i(f,j)p : \Param_i(f, j) represents an input parameter of sort jj.

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

  • In HoTT book notation, we can write the previous definition as:

PolyI Op:I𝒰 i:IParam i\Poly I \equiv \sum_{\Op : I \to \mathcal{U}}\prod_{i : I} \Param_i
Param i f:OpiI𝒰\Param_i \equiv \prod_{f : \Op i}I \to \mathcal{U}
Example

We start with the simplest non-trivial example, when I1I \equiv \mathbf{1} the unit type?. Looking at Poly1\Poly \mathbf{1} we clearly have Op:1𝒰𝒰\Op : \mathbf{1} \to \mathcal{U}\simeq \mathcal{U}. So Op\Op is simply a type. Next we have Param:(f:Op)1𝒰Op𝒰\Param : (f : \Op) \to \mathbf{1} \to \mathcal{U}\simeq \Op \to \mathcal{U} so Param\Param is just a family of types indexed over the type Op\Op.

Now if OpFin 3\Op \equiv \Fin_3 then there would be 3 operations. Take one of these operations and call it o 1o_1, Param\Param would then have to chose what the type of parameters should be, let’s choose Fin 2\Fin_2. This would mean that o 1o_1 would be an operation (o 1:Opo_1 : \Op) with two parameters p:Fin 2Paramo 1p : \Fin_2 \equiv \Param o_1. Note o 1o_1 is very much like the operator in an abstract syntax tree in this case.

When the type of sorts II gets more structure, the objects we discuss get complicated quickly. Even letting Paramo 1\Param o_1 be some arbitrary type gives us an interesting object.

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

Definition

The type of trees associated to a polynomial P:PolyIP : \Poly I is an inductive family? TrP:I𝒰\Tr P : I \to \mathcal{U} that has constructors

  • lf:(i:I)Tr(P,i)\lf : (i : I) \to \Tr(P, i)
  • nd:(i:I)(f:Op(P,i))(ϕ:(j:I)(p:Param i(f,j))Tr(P,j))Tr(P,i)\nd : (i : I) \to (f : \Op(P,i)) \to (\phi : (j : I) \to (p : \Param_i (f, j)) \to \Tr(P, j)) \to \Tr(P, i)

For a tree w:Tr(P,i)w : \Tr (P, i), we will need its type of leaves and type of nodes

Definition

The type of leaves of a tree P:PolyIP : \Poly I is given by:

  • Leaf:(i:I)(w:Tri)I𝒰\Leaf : (i : I) \to (w : \Tr i) \to I \to \mathcal{U}
  • Leaf i((lfi),j)(i=j)\Leaf_i((\lf i), j) \equiv (i = j)
  • Leaf i(nd(f,ϕ),j) k:I p:Param(f,k)Leaf i((ϕ(k,p)),j)\displaystyle\Leaf_i ( \nd(f, \phi),j) \equiv \sum_{k : I} \sum_{p : \Param (f, k)} \Leaf_i ((\phi (k, p)), j)
Definition

The type of nodes of a tree P:PolyIP : \Poly I is given by:

  • Node:(i:I)(w:Tri)(j:I)OpjType\Node : (i : I) \to (w : \Tr i) \to (j : I) \to \Op j \to \Type
  • Node i((lfi),j,g)0\Node_i ((\lf i), j, g) \equiv \mathbf{0}
  • Node i(nd(f,ϕ),j,g)((i,f)=(j,g))+ k:I p:Param(f,k)Node i(ϕ(j,p),j,g)\displaystyle \Node_i (\nd(f,\phi),j,g) \equiv ((i,f)=(j,g)) + \sum_{k : I} \sum_{p : \Param(f,k)} \Node_i ( \phi( j, p), j, g)
Definition

Let P:PolyIP : \Poly I be a polynomial w:Tr(P,i)w : \Tr(P,i) a tree and f:Op(P,i)f : \Op(P,i) an operation. A frame from ww to ff is a family of equivalences?

Frame(w,f):(j:I)Leaf i(w,j)Param(P,f,j)\Frame(w,f):(j:I) \to \Leaf_i(w,j) \simeq \Param(P,f,j)
Definition

A polynomial relation for PP is a type family:

R:(i:I)(f:Opi)(w:Tri)(α:Frame(w,f)𝒰R : (i:I) (f:\Op i)(w : \Tr i)(\alpha : \Frame(w,f) \to \mathcal{U}

Revision on February 16, 2019 at 08:39:32 by Leo?. See the history of this page for a list of all contributions to it.