A type theory for invertibility in weak $\omega$-categories

TL;DR

This paper introduces a conservative extension of a dependent type theory to formalize invertibility in weak ω-categories, enabling concise descriptions and semantics of equivalences and fibrations in higher category theory.

Contribution

It develops ICaTT, a new type theory extension for weak ω-categories, with an implementation for formalizing invertible cells and their properties.

Findings

Formalization of invertibility properties in ICaTT

Implementation of the theory for basic properties of invertible cells

Semantics of ICaTT in marked weak ω-categories

Abstract

We present a conservative extension ICaTT of the dependent type theory CaTT for weak $\omega$-categories with a type witnessing coinductive invertibility of cells. This extension allows for a concise description of the "walking equivalence" as a context, and of a set of maps characterising $\omega$-equifibrations as substitutions. We provide an implementation of our theory, which we use to formalise basic properties of invertible cells. These properties allow us to give semantics of ICaTT in marked weak $\omega$-categories, building a fibrant marked $\omega$-category out of every model of ICaTT.