Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A type theory for invertibility in weak $ω$-categories

Thibaut Benjamin, Camil Champin, Ioannis Markakis

TL;DR

A conservative extension ICaTT of the dependent type theory CaTT for weak $\omega$-categories with a type witnessing coinductive invertibility of cells is presented, allowing for a concise description of the walking equivalence as a context, and of a set of maps characterising $\omega$-equifibrations as substitutions.

Abstract

We present a conservative extension ICaTT of the dependent type theory CaTT for weak $ω$-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 $ω$-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 $ω$-categories, building a fibrant marked $ω$-category out of every model of ICaTT.

A type theory for invertibility in weak $ω$-categories

TL;DR

A conservative extension ICaTT of the dependent type theory CaTT for weak -categories with a type witnessing coinductive invertibility of cells is presented, allowing for a concise description of the walking equivalence as a context, and of a set of maps characterising -equifibrations as substitutions.

Abstract

We present a conservative extension ICaTT of the dependent type theory CaTT for weak -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 -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 -categories, building a fibrant marked -category out of every model of ICaTT.
Paper Structure (26 sections, 27 theorems, 69 equations, 4 figures)

This paper contains 26 sections, 27 theorems, 69 equations, 4 figures.

Table of Contents

  1. Introduction
  2. The type theory CaTT
  3. Weak ω-categories
  4. Models of clans
  5. Models of CaTT
  6. Invertible cells
  7. The type theory ICaTT
  8. The raw syntax
  9. The type of invertibility structures
  10. Invertibility of coherence terms
  11. The walking equivalence
  12. Recursor for invertibility structures
  13. Meta-theoretic considerations
  14. Internal proofs using invertibility
  15. Implementation and additional features
  16. ...and 11 more sections

Key Result

lemma 1

There exists a natural bijection between types $\Gamma \vdash A$ of CaTT of dimension $n$ and substitutions $\Gamma \vdash \chi_{A} \colon \mathbb{S}^{n}$, and a natural bijection between terms $\Gamma \vdash t \colon A$ of dimension $n$ and substitutions $\Gamma \vdash \chi_{t} \colon \mathbb{D}^{n

Figures (4)

  • Figure 1: Left cancellator of a composite of invertible cells $C = \gamma(b)^{\mathop{\mathrm{linv}}\nolimits}\ast (\gamma(a)^{\mathop{\mathrm{linv}}\nolimits} \ast \gamma(a)) \ast \gamma(b)$.
  • Figure 2: Relating left inverse to right inverse
  • Figure 3: Left cancellator of a composite of invertible cells. Here $C = (b^{\mathop{\mathrm{linv}}\nolimits}\ast a^{\mathop{\mathrm{linv}}\nolimits}) \ast (\llbracket a\rrbracket[\gamma] \ast \llbracket b\rrbracket[\gamma])$.
  • Figure 4: Rules of the theory ICaTT

Theorems & Definitions (58)

  • lemma 1
  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • theorem 1
  • proposition 1
  • definition 7
  • ...and 48 more