Types are weak omega-groupoids

Benno van den Berg, Richard Garner

We define a notion of weak omega-category internal to a model of Martin-Löf type theory, and prove that each type bears a canonical weak omega-category structure obtained from the…