nLab opetopic type theory

Contents

Context

Directed Type Theory

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Contents

Idea

Opetopic type theory (Finster 12) is a higher dimensional directed homotopy type theory for omega-categories, i.e. of infinity-categories in the full sense of ( , ) (\infty,\infty) -categories. Specifically, it realizes the higher-dimensional horn-filler conditions in the definition of opetopic omega-categories due to Palm as inference rules of term introduction for a higher-dimensional kind of formal logic (but it presently ignores the saturation condition on the thin cells).

Where in homotopy type theory there is an identity type of any type axiomatizing the infinity-groupoid structure of that type in, effectively, the style of a globular omega-groupoid, in opetopic type theory there is axiomatized instead a type of k-morphisms for all kk in the shape of opetopes.

Hence given a base type B𝒰\mathbf{B}\mathcal{U} – and a priori there is just one, to be thought of as the categorically delooped type universe, see below – a type is thus effectively identified with the shape of an opetope and thought of as the type of k-morphisms in B𝒰\mathbf{B}\mathcal{U}, the only other data being a possible marking that identifies it as just the sub-type of kk-equivalences of the given opetopic shape.

The only deduction rule is opetopic type formation and a term introduction rule which expresses the evident Kan filler-like condition saying that if a term of given opetopic shape is an outer horn (here: a “nook”) of kk-cells, then a kk-dimensional filler term is deduced, and if an outer or inner horn has a boundary by equivalences then a filler term marked as an equivalence is deduced.

Due to the genuinely omega-categorical nature of the setup, it makes sense to think of the (a priori) unique base type B𝒰\mathbf{B}\mathcal{U} as the categorical delooping of a type universe 𝒰 ×\mathcal{U}^\times being a monoidal (infinity,n)-category omega-category, and hence of the 1-endomorphisms (hence the terms of shape the directed interval (B𝒰B𝒰)(\mathbf{B}\mathcal{U}\to \mathbf{B}\mathcal{U}) ) as being the types in that universe. Composition of 1-morphism hence implies a type formation for multiplicative conjunction-types in a directed kind of linear homotopy type theory.

Introducing an axiom to this system just means postulating terms of (the type of) the shape of prescribed opetopes. For example:

Imposing nn-trunction and adjoints for all k-morphisms for 0kn0 \leq k \leq n therefore axiomatizes the language for a free (infinity,n)-category with adjoints on a single object. Categorical looping (which is immediate and primitive in the system, as above) hence gives the free (infinity,n)-category with duals on a single object.

This is the structure to which the cobordism hypothesis applies. Of course the proof of the cobordism hypothesis is not formulated in opetopic type theory and one would have to show that the language it is formulated in is suitably equivalent to that of opetopic type theory, but inspection in low dimension shows that the higher dimensional traces that opetopic type theory produces are of just the right kind.

proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

based on cubical type theory:

based on modal type theory:

based on simplicial type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:

References

Opetopic type theory is due to

It syntactically implements the definition of opetopic omega-category due to

by interpreting the higher-dimensional horn-filler conditions given there as inference rules.

(Palm shows that any opetopic set satisfying these filler conditions satisfies the property of Michael Makkai‘s definition of a opetopic set that qualifies as an opetopic omega-category. The converse is presently unknown.)

The higher dimensional string diagram-notation used here for opetopes was introduced (as “zoom complexes” in section 1.1) in

Animated exposition of this higher-dimensional string-diagram notation is in

A computer proof assistant for working with opetopic type theory is

A video tutorial for Orchard is

Apparently Orchard is discontinued in favour of an online version of similar functionality:

Something like an implementation of aspects of opetopic type theory within homotopy type theory is described in

Last revised on May 21, 2023 at 14:08:23. See the history of this page for a list of all contributions to it.