On the identity type as the type of computational paths

DOI10.1093/JIGPAL/JZX015zbMATH Open1405.03024arXiv1504.04759OpenAlexW2963961857MaRDI QIDQ4644591FDOQ4644591

Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina de Oliveira 

Publication date: 8 January 2019

Published in: Logic Journal of the IGPL (Search for Journal in Brave)

Abstract: We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity type, as defined by our approach, induces a groupoid structure. This result is on par with the fact that the traditional identity type induces a groupoid, as exposed by Hofmann & Streicher (1994).

Full work available at URL: https://arxiv.org/abs/1504.04759

Recommendations

• Identity in homotopy type theory. Part I: The justification of path induction
• Idempotents in intensional type theory
• Path categories and propositional identity types
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Interpreting higher computations as types with totality
• Computations on types
• Computational types from a logical perspective
• Topological and simplicial models of identity types
• Hindman's theorem and idempotent types
• Expressing computational complexity in constructive type theory

zbMATH Keywords

category theorytype theorygroupoid modelterm rewriting systemsidentity typeuniqueness of identity proofscomputational pathsequality proofshigher categorical structurespath-based constructions

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Groupoids, semigroupoids, semigroups, groups (viewed as categories) (18B40)

Cited In (4)

• Towards a homotopy domain theory
• Path categories and propositional identity types
• The justification of identity elimination in Martin-Löf's type theory
• Homotopy theoretic models of identity types

This page was built for publication: On the identity type as the type of computational paths

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4644591)