Towards a directed homotopy type theory
From MaRDI portal
Publication:6304745
DOI10.1016/J.ENTCS.2019.09.012arXiv1807.10566WikidataQ113317351 ScholiaQ113317351MaRDI QIDQ6304745
Publication date: 27 July 2018
Abstract: In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type former for Martin-L"of type theory which is roughly analogous to the identity type former originally introduced by Martin-L"of. 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 hom(a,b) is indeed the set of morphisms between the objects a and b of a 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"of's identity types.
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
This page was built for publication: Towards a directed homotopy type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6304745)
