Computational Paths and the Fundamental Groupoid of a Type
Resumo
Using computational paths as the fundamental concept, we show that we can leverage Category Theory to propose the concept of fundamental groupoid of a type.
Palavras-chave:
computational paths, groupoid, type theory, fundamental groupoid, identity type
Referências
Awodey, S. (2010). Category theory. Oxford University Press.
Awodey, S. (2012). Type theory and homotopy. In Dybjer, P., Lindstro ̈m, S., Palmgren, E., and Sundholm, G., editors, Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 183–201. Springer Netherlands.
de Oliveira, A. G. and de Queiroz, R. J. G. B. (1999). A normalization procedure for the equational fragment of labelled natural deduction. Logic J. of IGPL, 7(2):173–215.
de Queiroz, R. J. G. B. and de Oliveira, A. G. (1994). Term rewriting systems with labelled deductive systems. In Proc. Brazilian Symp. on Artif. Intellig., pages 59–72.
de Queiroz, R. J. G. B., de Oliveira, A. G., and Ramos, A. F. (2016). Propositional equal- ity, identity types, and direct computational paths. South American Journal of Logic, 2(2):245–296. Special Issue A Festschrift for Francisco Miraglia, M. E. Coniglio, H. L. Mariano and V. C. Lopes (Guest Editors).
Hindley, J. R. and Seldin, J. P. (2008). Lambda-calculus and combinators: an introduc- tion. Cambridge University Press.
Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2017). On the identity type as the type of computational paths. Logic Journal of the IGPL, 25(4):562–584.
Ramos, A. F., de Queiroz, R. J. G. B., de Oliveira, A. G., and De Veras, T. M. L. (2018). Explicit computational paths. South American Journal of Logic, 4(2):441–484. Pro- ceedings of the XVIII Brazilian Logic Conference.
Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foun- dations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.
Voevodsky, V. (2014). Univalent foundations and set theory. Univalent Foundations and Set Theory, Lecture at IAS, Princeton, New Jersey, Mar 2014.
Awodey, S. (2012). Type theory and homotopy. In Dybjer, P., Lindstro ̈m, S., Palmgren, E., and Sundholm, G., editors, Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 183–201. Springer Netherlands.
de Oliveira, A. G. and de Queiroz, R. J. G. B. (1999). A normalization procedure for the equational fragment of labelled natural deduction. Logic J. of IGPL, 7(2):173–215.
de Queiroz, R. J. G. B. and de Oliveira, A. G. (1994). Term rewriting systems with labelled deductive systems. In Proc. Brazilian Symp. on Artif. Intellig., pages 59–72.
de Queiroz, R. J. G. B., de Oliveira, A. G., and Ramos, A. F. (2016). Propositional equal- ity, identity types, and direct computational paths. South American Journal of Logic, 2(2):245–296. Special Issue A Festschrift for Francisco Miraglia, M. E. Coniglio, H. L. Mariano and V. C. Lopes (Guest Editors).
Hindley, J. R. and Seldin, J. P. (2008). Lambda-calculus and combinators: an introduc- tion. Cambridge University Press.
Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2017). On the identity type as the type of computational paths. Logic Journal of the IGPL, 25(4):562–584.
Ramos, A. F., de Queiroz, R. J. G. B., de Oliveira, A. G., and De Veras, T. M. L. (2018). Explicit computational paths. South American Journal of Logic, 4(2):441–484. Pro- ceedings of the XVIII Brazilian Logic Conference.
Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foun- dations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.
Voevodsky, V. (2014). Univalent foundations and set theory. Univalent Foundations and Set Theory, Lecture at IAS, Princeton, New Jersey, Mar 2014.
Publicado
18/07/2021
Como Citar
RAMOS, Arthur F.; QUEIROZ, Ruy J. G. B. de; OLIVEIRA, Anjolina G. de.
Computational Paths and the Fundamental Groupoid of a Type. In: ENCONTRO DE TEORIA DA COMPUTAÇÃO (ETC), 6. , 2021, Evento Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2021
.
p. 22-25.
ISSN 2595-6116.
DOI: https://doi.org/10.5753/etc.2021.16371.
