On the identity type as the type of computational paths
From MaRDI portal
Publication:4644591
DOI10.1093/jigpal/jzx015zbMath1405.03024arXiv1504.04759MaRDI QIDQ4644591
Ruy J. G. B. de Queiroz, Anjolina de Oliveira, Arthur F. Ramos
Publication date: 8 January 2019
Published in: Logic Journal of the IGPL (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1504.04759
category theory; term rewriting systems; type theory; groupoid model; identity type; uniqueness of identity proofs; computational paths; equality proofs; higher categorical structures; path-based constructions
68Q42: Grammars and rewriting systems
18B40: Groupoids, semigroupoids, semigroups, groups (viewed as categories)