On the identity type as the type of computational paths

DOI10.1093/JIGPAL/JZX015MaRDI QIDQ4644591zbMATHOpenAlexFDO

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)

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

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)

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).

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

Cited in

(4)

• Towards a homotopy domain theory
• Homotopy theoretic models of identity types
• The justification of identity elimination in Martin-Löf's type theory
• Path categories and propositional 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)