Types are weak ω-groupoids

Benno Van Den Berg; Richard Garner

doi:10.1112/plms/pdq026

Types are weak ω-groupoids

Benno Van Den Berg^*, Richard Garner

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

76 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 language	English
Pages (from-to)	370-394
Number of pages	25
Journal	Proceedings of the London Mathematical Society
Volume	102
Issue number	2
DOIs	https://doi.org/10.1112/plms/pdq026
Publication status	Published - Feb 2011
Externally published	Yes

Access to Document

10.1112/plms/pdq026

Cite this

@article{1217f7a8fb634057b601813c4e329901,

title = "Types are weak ω-groupoids",

abstract = "We define a notion of weak ω-category internal to a model of Martin-L{\"o}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.",

author = "{Van Den Berg}, Benno and Richard Garner",

year = "2011",

month = feb,

doi = "10.1112/plms/pdq026",

language = "English",

volume = "102",

pages = "370--394",

journal = "Proceedings of the London Mathematical Society",

issn = "0024-6115",

publisher = "John Wiley & Sons",

number = "2",

}

TY - JOUR

T1 - Types are weak ω-groupoids

AU - Van Den Berg, Benno

AU - Garner, Richard

PY - 2011/2

Y1 - 2011/2

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79751520357&partnerID=8YFLogxK

U2 - 10.1112/plms/pdq026

DO - 10.1112/plms/pdq026

M3 - Article

AN - SCOPUS:79751520357

SN - 0024-6115

VL - 102

SP - 370

EP - 394

JO - Proceedings of the London Mathematical Society

JF - Proceedings of the London Mathematical Society

IS - 2

ER -

Types are weak ω-groupoids

Abstract

Access to Document

Other files and links

Fingerprint

Cite this