際際滷

際際滷Share a Scribd company logo

Computational paths, identity type and groupoid model

Download as PPTX, PDF
Arthur Ramos
Arthur Ramos

This document proposes a new approach to modeling identity types in type theory using computational paths. [1] It introduces computational paths as syntactic objects representing proofs of equality between terms. A groupoid structure is induced on paths that models identity types. [2] Higher structures, like a bicategory, can be constructed from paths of paths. This bicategory forms a weak 2-groupoid modeling higher identity types. [3] The approach is proven compatible with previous work modeling identity types but provides a more intuitive syntactic presentation using computational paths. Future work includes fully specifying reductions between paths and studying even higher induced weak groupoid structures.

1 of 32
Download to read offline
Computational Paths, identity type, and the groupoid model LSFA 2015 Arthur Freitas Ramos Ruy de Queiroz Anjolina de Oliveira
Motivation Mathematics becoming increasingly abstract and complex Automatic Proof Checkers Type Theory: Identity type as a bridge between computer science and math Objective: To propose a more intuitive approach to the identity type
Intensional Identity Type Witness p as proof of propositional equality between two objects of the same type Connection between extensionality and intensionality Homotopy Type Theory: Semantic connection with homotopy (paths) HOFMANN - STREICHER 1994: Groupoid structure refutes the principle of the unicity of proofs of equality LUMSDAINE 2009: weak structure
Identity Type: Formal Construction
Identity Type: New Approach We propose a new approach to the identity type Objective: to be more intuitive than the classic approach Based on Computational Paths, entity originally proposed by Gabbay and Ruy de Queiroz in 1994 Paths as part of the syntax of type theory: algebra of paths (or calculus of paths) Main objectives of this work: Detailed explanation of our new approach and proof of essential properties, such as the groupoid structure
Beta Equality Given terms P e Q if we say that they are if: reduction: reduction together with : theory of
Theory of Lambda-Beta-Eta Equality Axiom: Inference rules:
Equality Theory for the Product Type
Computational Paths Composition of axioms and inference rules s that establishes the propositional equality between two terms a : A and b : A Notation a =s b : A Composition done by applications of the transitivity
Computational Paths: Example Path between and : From we obtain From we obtain To obtain the final path between and , we just need to concatenate both paths using the transitivity, obtaining:
Type Identity as the Type of Computational Paths: Formalization
Type Identity as the Type of Computational Paths: Formalization
Usage example: Symmetry Construction of :
Usage example: Transitivity Construction of :
Term Rewriting System LNDEQ-TRS Reduction between different paths Simple examples: and ; and Anjolina (1994) and Ruy & Anjolina (2011): Term rewriting system LNDEQ-TRS Total of 39 reduction rules 7 essential to the current work
Reductions Involving Symmetry and Reflexivity Obtained rules:
Reductions Involving Transitivity Obtained rules:
Reductions Involving Transitivity Obtained rule:
rw-equality Each LNDEQ-TRS is known as rw rule From s to t in 1 rule: From s to t in multiple rules: Rw-equality s =rw t: sequence R0, ....., Rn , with such that: Rw-equality is an equivalence class (since it has been defined as a transitive, symmetric and reflexive closure)
LNDRW-TRS2 Redundancies between Paths of Paths Redundancies caused by rw-equality There is a version for each redunction previously showed Exemple:
rw2-equality Rw2-equality: similar to rw-equality Rw2 is an equivalence class (analogous to rw) Special rule cd2:
Category Arw Induced by Computational Paths Objects: terms a: A Morphisms: Paths s between objects a,b: A. iff a =s b Composition: Identity: Weak category: Equality holds only up to rw-equality Associativity: Identity Laws:
ARW is a Weak Groupoid Every arrow is an isomorphism We need to show that every morphism s has an inverse morphism t Set :
Higher Strucure: 2 - Arw Category A2rw(a,b) for each pair of objects Arw Objects of A2rw(a,b) are paths s: a =s b and morphisms between paths s,r are sets of rw-equalities s =rw r Associativity and transitivity hold weakly up to rw2-equality (analogous to Arw) Considering equivalence classes of rw2, equalities hold on the nose on the second level. Structure [2 Arw] Is [2 Arw] a bicategory? Is it a weak 2-grupoid?
Bicategory Horizontal Composition Associativity and identity of the horizontal composition Interchange law Coherence law: Mac Lanes pentagon and triangle
[2 Arw] is a Bicategory Horizontal composition : Given: We define as:
[2 Arw] is a Bicategory Associativity assoc of : Natural isomorphism between Given by the isomorphism of each component: Identity : We only need to check each component: Analogous to : Use trr
[2 Arw] is a Bicategory Interchange law:
[2 Arw] is a Bicategory Coherence laws:
[2 Arw]: Results We have showed that [2 Arw] is a bicategory From the fact that [2 Arw] is a bicategory, that A2rw is a weak groupoid and Arw a groupoid, we conclude that [2 Arw] is a weak 2- groupoid It is possible to think of weak groupoids with higher number of levels. Eventually, we can think of a weak groupoid with an infinite number of levels, the weak
Conclusion We have proposed a new approach based on computer Computer paths are present in the syntax of type theory, opposite to being only a semantical interpretation Using computational paths, it is possible to induce higher groupoids. We have obtained results compatible with the ones obtained by Hofmann-Streicher for the traditional identity type
Future Work Mapping of all possible rw2-rules The study of induced weak groupoids with order higher than 2 Possibility of obtaining, to our approach based on computational paths, results similar to the ones obtained by Lumsdaine. In other words, to prove that it is possible to induce a

More Related Content

Computational paths, identity type and groupoid model

  • 1. Computational Paths, identity type, and the groupoid model LSFA 2015 Arthur Freitas Ramos Ruy de Queiroz Anjolina de Oliveira
  • 2. Motivation Mathematics becoming increasingly abstract and complex Automatic Proof Checkers Type Theory: Identity type as a bridge between computer science and math Objective: To propose a more intuitive approach to the identity type
  • 3. Intensional Identity Type Witness p as proof of propositional equality between two objects of the same type Connection between extensionality and intensionality Homotopy Type Theory: Semantic connection with homotopy (paths) HOFMANN - STREICHER 1994: Groupoid structure refutes the principle of the unicity of proofs of equality LUMSDAINE 2009: weak structure
  • 4. Identity Type: Formal Construction
  • 5. Identity Type: New Approach We propose a new approach to the identity type Objective: to be more intuitive than the classic approach Based on Computational Paths, entity originally proposed by Gabbay and Ruy de Queiroz in 1994 Paths as part of the syntax of type theory: algebra of paths (or calculus of paths) Main objectives of this work: Detailed explanation of our new approach and proof of essential properties, such as the groupoid structure
  • 6. Beta Equality Given terms P e Q if we say that they are if: reduction: reduction together with : theory of
  • 7. Theory of Lambda-Beta-Eta Equality Axiom: Inference rules:
  • 8. Equality Theory for the Product Type
  • 9. Computational Paths Composition of axioms and inference rules s that establishes the propositional equality between two terms a : A and b : A Notation a =s b : A Composition done by applications of the transitivity
  • 10. Computational Paths: Example Path between and : From we obtain From we obtain To obtain the final path between and , we just need to concatenate both paths using the transitivity, obtaining:
  • 11. Type Identity as the Type of Computational Paths: Formalization
  • 12. Type Identity as the Type of Computational Paths: Formalization
  • 13. Usage example: Symmetry Construction of :
  • 14. Usage example: Transitivity Construction of :
  • 15. Term Rewriting System LNDEQ-TRS Reduction between different paths Simple examples: and ; and Anjolina (1994) and Ruy & Anjolina (2011): Term rewriting system LNDEQ-TRS Total of 39 reduction rules 7 essential to the current work
  • 16. Reductions Involving Symmetry and Reflexivity Obtained rules:
  • 19. rw-equality Each LNDEQ-TRS is known as rw rule From s to t in 1 rule: From s to t in multiple rules: Rw-equality s =rw t: sequence R0, ....., Rn , with such that: Rw-equality is an equivalence class (since it has been defined as a transitive, symmetric and reflexive closure)
  • 20. LNDRW-TRS2 Redundancies between Paths of Paths Redundancies caused by rw-equality There is a version for each redunction previously showed Exemple:
  • 21. rw2-equality Rw2-equality: similar to rw-equality Rw2 is an equivalence class (analogous to rw) Special rule cd2:
  • 22. Category Arw Induced by Computational Paths Objects: terms a: A Morphisms: Paths s between objects a,b: A. iff a =s b Composition: Identity: Weak category: Equality holds only up to rw-equality Associativity: Identity Laws:
  • 23. ARW is a Weak Groupoid Every arrow is an isomorphism We need to show that every morphism s has an inverse morphism t Set :
  • 24. Higher Strucure: 2 - Arw Category A2rw(a,b) for each pair of objects Arw Objects of A2rw(a,b) are paths s: a =s b and morphisms between paths s,r are sets of rw-equalities s =rw r Associativity and transitivity hold weakly up to rw2-equality (analogous to Arw) Considering equivalence classes of rw2, equalities hold on the nose on the second level. Structure [2 Arw] Is [2 Arw] a bicategory? Is it a weak 2-grupoid?
  • 25. Bicategory Horizontal Composition Associativity and identity of the horizontal composition Interchange law Coherence law: Mac Lanes pentagon and triangle
  • 26. [2 Arw] is a Bicategory Horizontal composition : Given: We define as:
  • 27. [2 Arw] is a Bicategory Associativity assoc of : Natural isomorphism between Given by the isomorphism of each component: Identity : We only need to check each component: Analogous to : Use trr
  • 28. [2 Arw] is a Bicategory Interchange law:
  • 29. [2 Arw] is a Bicategory Coherence laws:
  • 30. [2 Arw]: Results We have showed that [2 Arw] is a bicategory From the fact that [2 Arw] is a bicategory, that A2rw is a weak groupoid and Arw a groupoid, we conclude that [2 Arw] is a weak 2- groupoid It is possible to think of weak groupoids with higher number of levels. Eventually, we can think of a weak groupoid with an infinite number of levels, the weak
  • 31. Conclusion We have proposed a new approach based on computer Computer paths are present in the syntax of type theory, opposite to being only a semantical interpretation Using computational paths, it is possible to induce higher groupoids. We have obtained results compatible with the ones obtained by Hofmann-Streicher for the traditional identity type
  • 32. Future Work Mapping of all possible rw2-rules The study of induced weak groupoids with order higher than 2 Possibility of obtaining, to our approach based on computational paths, results similar to the ones obtained by Lumsdaine. In other words, to prove that it is possible to induce a
AboutCopyright
息 2025 際際滷