Computational Paths and the Fundamental Groupoid of a Type
ResumoUsing computational paths as the fundamental concept, we show that we can leverage Category Theory to propose the concept of fundamental groupoid of a type.
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.