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
Semantics of higher inductive types
Stockholm University, Faculty of Science, Department of Mathematics.
Number of Authors: 22020 (English)In: Mathematical proceedings of the Cambridge Philosophical Society (Print), ISSN 0305-0041, E-ISSN 1469-8064, Vol. 169, no 1, p. 159-208Article in journal (Refereed) Published
Abstract [en]

Higher inductive typesare a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the synthetic development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion ofcell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category hasweakly stable typal initial algebrasfor any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (infinity, 1)-category is presented by some model category to which our results apply.

Place, publisher, year, edition, pages
2020. Vol. 169, no 1, p. 159-208
National Category
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-183955DOI: 10.1017/S030500411900015XISI: 000545996900008OAI: oai:DiVA.org:su-183955DiVA, id: diva2:1469972
Available from: 2020-09-23 Created: 2020-09-23 Last updated: 2022-02-25Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records

Lefanu Lumsdaine, Peter

Search in DiVA

By author/editor
Lefanu Lumsdaine, Peter
By organisation
Department of Mathematics
In the same journal
Mathematical proceedings of the Cambridge Philosophical Society (Print)
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 37 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