natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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 $k$ in the shape of opetopes.
Hence given a base type $\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 $\mathbf{B}\mathcal{U}$, the only other data being a possible marking that identifies it as just the sub-type of $k$-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 $k$-cells, then a $k$-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 $\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 $(\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:
$n$-truncation – For the language inside an (infinity,n)-category one demands that all k-morphisms for $k \geq n+1$ are marked as equivalences;
$k$-adjoints – To axiomatize that two $k$-morphism are left adjoint and right adjoint to each other, respectively, one postulates the existence of $k+1$-morphisms serving as unit of an adjunction and counit of an adjunction and of a 3-morphism marked as equivalence which axiomatizes the zig-zag identities.
Imposing $n$-trunction and adjoints for all k-morphisms for $0 \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.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq)
Xena project (using Lean)
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
Eric Finster, Opetopic Diagrams 1 - Basics (video)
Eric Finster, Opetopic Diagrams 2 - Geometry (video)
A computer proof assistant for working with opetopic type theory is
Eric Finster, Orchard (GitHub repository)
Eric Finster, Opetope! (online opetopic type theory system)
A video tutorial for Orchard is
Eric Finster, Orchard 1 - Introduction (video)
Eric Finster, Orchard 2 - Modifying the shape (video)
Eric Finster, Orchard 3 - Composition and associativity (video)
Eric Finster, Orchard 4 - Identities and invertibility (video)
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
Eric Finster, Towards Higher Universal Algebra in Type Theory, Homotopy Type Theory Electronic Seminar 2018 (recording, Agda code)
Antoine Allioux, Eric Finster, Matthieu Sozeau, Types are internal infinity-groupoids, 2021 (hal:03133144, pdf)