Rumo a uma Teoria de Domínios da Homotopia
Resumo
A Teoria dos Domínios de Dana Scott fornece técnicas gerais para a obtenção de $\lambda$-modelos através da resolução de equações de domínio sobre categorias cartesianas fechadas arbitrárias. A intenção aqui é oferecer uma exposição de forma geral do projeto de generalização da Teoria dos Domínios para uma teoria que denominamos "Teoria de Domínios da Homotopia". O esforço vai no sentido de encontrar um tipo de $\lambda$-modelo com uma estrutura de $\infty$-grupóide, que permitem um salto na interpretação das igualdades do $\lambda$-calculo (ex: $\beta$-igualdade, $\eta$-igualdade etc.) para igualdades de ordem superior na mesma teoria.
Referências
Asperti A. and Longo G. (1991). Categories, Types and Structures: An Introduction to Category Theory for the working computer scientist. Foundations of Computing Series, M.I.T Press.
Hatcher A. (2001) Algebraic Topology. Cambridge University Press, New York, NY.
Hindley J. and Seldin J. (2008). Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, New York.
Hyland M. (2010) Some reasons for generalizing domain theory. Mathematical Structures in Computer Science 20, pages 239–265.
Kapulkin C., Lumsdaine P. and Voevodsky V. (2012). The simplicial model of univalent foundations. arXiv:1211.2851.
Lumsdaine P. and Shulman M. (2020). Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society 169, pages 159–208.
Lurie J. (2009). Higher Topos Theory. Princeton University Press, Princeton and Oxford.
Martı́nez-Rivillas D. and de Queiroz R. (2021). The ∞-groupoid generated by an arbitrary topological λ-model. Logic Journal of the IGPL. https://doi.org/10.1093/jigpal/jzab015 (also arXiv:1906.05729).
Martı́nez-Rivillas D. and de Queiroz R. (2020). Towards a homotopy domain theory. ArXiv:2007.15082.
Martı́nez-Rivillas D. and de Queiroz R. (2021). Solving homotopy domain equations. ArXiv:2104.01195.
Program T. U. F. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ: Institute for Advanced Study.