MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I've read somewhere (probably in the nlab) that higher category theory has application in logic. By the way since now the only applications of higher category theory I've seen are in homotopy theory and mathematical physics, so I was wondering if anyone could give me some example of applications of higher categorical methods in logic (any reference would be appreciated).

share|cite|improve this question

You would probably enjoy checking out homotopy type theory and Vladimir Voevodsky's corresponding program of univalent foundations for mathematics. Steve Awodey's survey article (linked to from that site) is a good starting point, and includes a spelling-out of a homotopical interpretation of Martin-Lof type theory.

share|cite|improve this answer

To elaborate on Peter Arndt's answer a bit: indeed, considering terms as 1-cells and rewriting rules as 2-cells, you can indeed obtain a rather productive higher categorical view on various constructions of rewriting theory. Morally, this would mean that cofibrant replacements in various model categories (of modules, or associative algebras) can be described in a rather pleasant geometric way, - computing syzygies becomes building higher-dimensional cells of a cell complex from the low-dimensional ones. There are several good references to master this kind of viewpoint, best processed when viewed together. Those are the paper of Craig Squier "Word problems and a homological finiteness condition for monoids" from which all sort of started, when it comes to theoretical computer science, at least (this paper re-discovered in a somewhat different context results from a paper of David Anick "On the homology of associative algebras"), the paper of Jean-Louis Loday "Homotopical syzygies", and indeed, recent papers of the French computer science school, such as Yves Lafont, Francois Metayer, Yves Guiraud, Philippe Malbos and many others.

share|cite|improve this answer
There is a workshop called "Catégories supérieures, polygraphes, homotopie" in Paris: I have listened to many talks related to these questions there. People are welcome. – Jonathan Chiche Feb 24 '12 at 12:45
Oh yes, that's a good idea to have that link here. To people not familiar with the French system: what Jonathan called a workshop is more commonly called a working group (continuous meetings where participants present various results in the area studied by the working group). – Vladimir Dotsenko Feb 24 '12 at 13:17

Another group of related applications are those in rewriting theory, concurrency theory, directed homotopy theory etc. For this check out the pages of Yves Lafont and his collaborators.

share|cite|improve this answer

There should be a lot of stuff concerning this in papers and books of Michael Makkai.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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