pith. sign in

arxiv: 0812.0298 · v2 · pith:Q7IX26FUnew · submitted 2008-12-01 · 🧮 math.LO · math.CT

Types are weak omega-groupoids

Benno van den Berg , Richard Garner This is my paper
classification 🧮 math.LO math.CT
keywords typeweakomega-categoryomega-groupoidstypesarisingbearscanonical
0
0 comments X
read the original abstract

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

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.