# A Type-Theoretical Definition of Weak {\omega}-Categories

## TL;DR

This paper develops a dependent type theory that models weak {}-categories, generalizing previous definitions and providing a formal, canonical framework with an implemented proof system.

## Contribution

It introduces a type-theoretical framework for weak {}-categories based on globular presheaves and coherators, with a canonical characterization of pasting schemes and an implementation.

## Key findings

- Provides a formal type-theoretical model of weak {}-categories.
- Defines pasting schemes as derivable contexts within the type theory.
- Includes an implemented proof system for the proposed framework.

## Abstract

We introduce a dependent type theory whose models are weak {\omega}-categories, generalizing Brunerie's definition of {\omega}-groupoids. Our type theory is based on the definition of {\omega}-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of {\omega}-groupoids. In this setup, {\omega}-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an {\omega}-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.