Showing changes from revision #6 to #7:
Added | Removed | Changed
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 is yields a tool to solve the general problem of coherences of higher algebra/higher category theory within homotopy type theory.
Eric Finster, Towards Higher Universal Algebra in Type Theory, Homotopy Type Theory Electronic Seminar 2018 (pdf slides, recording)
Agda code at: github.com/ericfinster/higher-alg
The idea of opetopic sets that Finster 18 is inspired by goes back to
Collecting Here we collect the definitions and trying ideas them that out were here. given The idea is to go through the definitions in Eric’s talk. We can also use the talk and the definitions in the agda formalisation to for play reference around too. with.
Fix a type $I$ of sorts. A polynomial over $I$, $\Poly I$, is the data of
Definition Fix a type $I$ of sorts. A polynomial over $I$, $\Poly I$, is the data of
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.
In HoTT book notation, we can write the previous definition as:
A polynomial $P : \Poly I$ generates an associated type of trees.
The type of trees associated to a polynomial $P : \Poly I$ is an inductive family? $\Tr P : I \to \mathcal{U}$ that has constructors
RemarkFor a tree $w : \Tr (P, i)$, we will need its type of leaves and type of nodes
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.
The type of leaves of a tree $P : \Poly I$ is given by:
The type of nodes of a tree $P : \Poly I$ is given by:
A polynomial $P : \Poly I$ generates an assocaiated type of trees.
Definition The inductive family $\Tr P : I \to \mathcal{U}$ has constructors
For a tree $w : \Tr (P, i)$, we will need its type of leaves and type of nodes
Definition
Revision on December 7, 2018 at 11:04:32 by Ali Caglayan. See the history of this page for a list of all contributions to it.