2000 character limit reached
Type theory and homotopy
Published 9 Oct 2010 in math.CT and math.LO | (1010.1810v1)
Abstract: The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Martin-L\"of into homotopy theory, resulting in new examples of higher-dimensional categories.
Paper Prompts
Sign up for free to create and run prompts on this paper using GPT-5.
Top Community Prompts
Collections
Sign up for free to add this paper to one or more collections.
