opetopic type theory



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations



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 (infinity,infinity)-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:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:


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 March 25, 2021 at 01:59:02. See the history of this page for a list of all contributions to it.