Types are weak ω-groupoids

Benno Van Den Berg*, Richard Garner

*Corresponding author for this work

Research output: Contribution to journalArticle

46 Citations (Scopus)

Abstract

We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.

Original languageEnglish
Pages (from-to)370-394
Number of pages25
JournalProceedings of the London Mathematical Society
Volume102
Issue number2
DOIs
Publication statusPublished - Feb 2011
Externally publishedYes

Fingerprint Dive into the research topics of 'Types are weak ω-groupoids'. Together they form a unique fingerprint.

Cite this