TOWARDS THE THEORY OF PROOF-RELEVANT CATEGORIES

Embargo until
Date
2022-07-18
Journal Title
Journal ISSN
Volume Title
Publisher
Johns Hopkins University
Abstract
We introduce a general framework of \emph{proof-relevant algebras} for $T$-categories, where $T$ is the free strict $\omega$-category monad on globular sets. Through some general considerations about enrichment and internalisation in virtual double categories we give a shape functor $\ainl\SWCat\bS\TCat$ and prove a rich comparison of algebras under this functor. Using this framework and some supporting theory we explore definitions of \emph{proof-relevant category} and \emph{proof-relevant functor}, which are proof-relevant algebras of the shape of the strict $\omega$-categories $\bone$ and $\{\cdot\to\cdot\}$ respectively. Proof-relevant categories are higher-category-like structures in which composition is multi-valued, unbiased, witnessed by proofs, and there is a calculus of proofs. The definition we give for proof-relevant category is a variation of Leinster's model $L'$ \cite{leinsterDef}. Proof-relevant functors are the natural adaption of functor to the proof-relevant setting: mapping is multi-valued and unbiased, and values are witnessed by proofs. In exploring these definitions we give some of the early theory of co-inductive equivalences in the proof-relevant setting, and this made efficient by a compact notation for globular pasting diagrams. We conclude with an application of our proof-relevant algebra framework to proof-relevant functor composition, and suggest further definitions in this vein.
Description
Keywords
higher category theory
Citation