TY - CONF

T1 - Towards a Directed Homotopy Type Theory

AU - North, Paige Randall

PY - 2019

Y1 - 2019

N2 - In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types.

AB - In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types.

KW - dependent type theory

KW - directed homotopy theory

KW - semantics of type theory

UR - https://www.mendeley.com/catalogue/b7f833e1-077f-3e06-8c38-3dab9c528331/

UR - https://www.mendeley.com/catalogue/b7f833e1-077f-3e06-8c38-3dab9c528331/

U2 - 10.1016/j.entcs.2019.09.012

DO - 10.1016/j.entcs.2019.09.012

M3 - Paper

ER -