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).
4 Answers
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.
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.
-
3$\begingroup$ There is a workshop called "Catégories supérieures, polygraphes, homotopie" in Paris: pps.jussieu.fr/gdt-h-ncat. I have listened to many talks related to these questions there. People are welcome. $\endgroup$ Commented Feb 24, 2012 at 12:45
-
$\begingroup$ 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). $\endgroup$ Commented Feb 24, 2012 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.
There should be a lot of stuff concerning this in papers and books of Michael Makkai.