nLab opetopic type theory

Contents

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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

semantics

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:

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 December 21, 2022 at 08:59:35. See the history of this page for a list of all contributions to it.