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).
Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)
|
8
5
|
|
||
|
|
|
11
|
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. |
||
|
|
You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.
|
8
|
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. |
||
|
|
|
4
|
There should be a lot of stuff concerning this in papers and books of Michael Makkai. |
||
|
|
|
8
|
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. |
||||||||
|
