The recent paper "A Type Theory for Synthetic $\infty$-Categories" proposes the syntax as the theory of the strict interval. In principle, any other suitable theory could be used instead. For instance, using Joyal’s theory of disks would yield a type theory in which to study $(\infty,n)$-categories ($\theta$ categories) in Rezk's style.

Any one know some work or references on a type theory to study higher categories, more specifically, $(\infty,n)$-categories and $(r,n)$-categories ?

  • 2
    $\begingroup$ A year ago I would have felt confident saying that the paper of Riehl and Shulman you mention was the state of the art. But this is a fast-moving field and I think many people are interested in this question, so I wouldn't be surprised to see a preprint on this topic in the next six months if one hasn't appeared already. If you want to know who's working on this, it's probably worth asking Emily Riehl or Mike Shulman. $\endgroup$ – Tim Campion Aug 30 '17 at 15:09
  • $\begingroup$ Also potentially relvant: directed homotopy type theory. $\endgroup$ – Tim Campion Aug 30 '17 at 15:12

I don't know of anyone who is specifically working on generalizing our paper to the $(\infty,n)$-case. But there have been other attempts to design a type theory for higher categories, such as Finster's opetopic type theory.


I take advantage of your post to point out to you that I built algebraic models of weak (\infty,m)-categories in different geometry :

Globular : http://www.tac.mta.ca/tac/volumes/30/22/30-22.pdf

Cubical : https://arxiv.org/pdf/1702.00336.pdf

Multiple : https://arxiv.org/pdf/1702.05206.pdf

For example these globular (\infty,0)-categories are models of globular \infty-groupoids. All these models are algebras for a specific monad. For example models of cubical (\infty,1)-categories are algebras for a specific monad on the category of cubical sets (see the arxiv above, because the cubical sets that I considered are a bit poorer than the usual one, those equipped with connections, etc.). Also it is highly probable that all these monads have arities, which means that behind it there are theories such that models of it correspond exactely to algebras for these monads.

Also it is not difficult to prove, for all integer m, that these globular models of (\infty,m)-categories are in fact weak infty-categories in Batanin's sense.

A big advantage of this approach is its simplicity : It follows an old idea of Batanin and Penon that "the weak must be coherently controlled by the strict", and you need to understand only the globular models to have a good picture of the rest, because the cubical models and the multiple models follow the same kind of construction.

Last thing which is very important : Behind all these monads there are adapted langages which permit to use basic technics of logic to built free (\infty,m)-categories, for all integer m, and for all geometry (globular, cubical, multiple). For example, if you fix an integer m, and a cubical set X, you can describe inductively the free cubical weak (\infty,m)-category F(X). This last point is not difficult to be guessed : Penon had already done it for the case of of the monad of globular infty-categories, in his article "Approche polygraphique des infini-catégories non-strictes, 1999", and my monads are similar to his monad ...


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.