Links between homotopy theory and type theory

Autor:	Bertot, Yves
Přispěvatelé:	Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), This work was partially supported by Institute for Advanced Study, Princeton, Stephen Watt, James Davenport, Alan Sexton, Petr Sojka, Josef Urban, Bertot, Yves
Jazyk:	angličtina
Rok vydání:	2014
Předmět:	[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] Mathematics::K-Theory and Homology Mathematics::Category Theory [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Mathematics::Algebraic Topology
Zdroj:	CICM-Conference on Intelligent Computer Mathematics CICM-Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal
Popis:	International audience; This short note reviews the relations between homotopy theory and type theory, especially the similarity between paths in homotopy and proofs of equality in type theory.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::4571949c12f386bb7efca597d49036d5 https://hal.inria.fr/hal-00987248/file/paper.pdf Zobrazit plný text záznamu