Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
The homotopy theory of type theories
Stockholm University, Faculty of Science, Department of Mathematics.
Number of Authors: 22018 (English)In: Advances in Mathematics, ISSN 0001-8708, E-ISSN 1090-2082, Vol. 337, p. 1-38Article in journal (Refereed) Published
Abstract [en]

We construct a left semi-model structure on the category of intensional type theories (precisely, on CxlCat(Id,1,Sigma(,Pi ext))). This presents an infinity-category of such type theories; we show moreover that there is an infinity-functor Cl-infinity from there to the infinity-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

Place, publisher, year, edition, pages
2018. Vol. 337, p. 1-38
Keywords [en]
Homotopy type theory, Higher category theory, Internal language, Model category
National Category
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-161941DOI: 10.1016/j.aim.2018.08.003ISI: 000446649200001OAI: oai:DiVA.org:su-161941DiVA, id: diva2:1262581
Available from: 2018-11-12 Created: 2018-11-12 Last updated: 2018-11-12Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Lumsdaine, Peter LeFanu
By organisation
Department of Mathematics
In the same journal
Advances in Mathematics
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 70 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf