期刊
JOURNAL OF LOGIC AND COMPUTATION
卷 -, 期 -, 页码 -出版社
OXFORD UNIV PRESS
DOI: 10.1093/logcom/exad071
关键词
Category theory; labelled natural deduction; term rewriting system; computational paths; algebraic topology
This paper demonstrates how to formalize the concept of computational paths as equalities between two terms of the same type using a labelled deduction system. With this formalization, the fundamental groupoid of a path-connected type and the concept of isomorphism between types are constructed. It is also shown that computational paths determine a weak category and a weak groupoid.
On the basis of a labelled deduction system (LND$_{ED-}$TRS), we demonstrate how to formalize the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. This has allowed us to carry out a formal counterpart to equality between paths which is dealt with in homotopy theory, but this time with an approach using the device of term-rewriting paths. Using such formal calculus dealing with paths, we construct the fundamental groupoid of a path-connected $ X $ type and we define the concept of isomorphism between types. Next, we show that the computational paths determine a weak category, which will be called $ \mathcal {C}_{paths} $. Finally, we show that the weak category $ \mathcal {C}_{paths} $ determines a weak groupoid.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据