TY - GEN
T1 - The directed homotopy hypothesis
AU - Dubut, Jérémy
AU - Goubault, Eric
AU - Goubault-Larrecq, Jean
N1 - Publisher Copyright:
© Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq; licensed under Creative Commons License CC-BY.
PY - 2016/8/1
Y1 - 2016/8/1
N2 - The homotopy hypothesis was originally stated by Grothendieck [13]: topological spaces should be "equivalent" to (weak) 1-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g. for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be "equivalent" to a weak form of topologically enriched categories, still very close to (1,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.
AB - The homotopy hypothesis was originally stated by Grothendieck [13]: topological spaces should be "equivalent" to (weak) 1-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g. for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be "equivalent" to a weak form of topologically enriched categories, still very close to (1,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.
KW - Directed algebraic topology
KW - Geometric models for concurrency
KW - Higher category theory
KW - Homotopy hypothesis
KW - Partially enriched categories
U2 - 10.4230/LIPIcs.CSL.2016.9
DO - 10.4230/LIPIcs.CSL.2016.9
M3 - Conference contribution
AN - SCOPUS:85012927901
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - Computer Science Logic 2016, CSL 2016
A2 - Talbot, Jean-Marc
A2 - Regnier, Laurent
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
Y2 - 29 August 2016 through 1 September 2016
ER -