An Internal Logic of Virtual Double Categories

TL;DR

This paper introduces FVDblTT, a type theory that formalizes reasoning within virtual double categories, providing a foundational internal language for formal category theory and establishing a syntax-semantics duality.

Contribution

It develops FVDblTT, a novel type theory that serves as an internal language for virtual double categories, bridging syntax and semantics in formal category theory.

Findings

FVDblTT formalizes reasoning on isomorphisms in category theory.

Establishes a biadjunction between virtual double categories and FVDblTT specifications.

Validates FVDblTT as an effective internal language for virtual double categories.

Abstract

We present a type theory called fibrational virtual double type theory (FVDblTT) designed specifically for formal category theory, which is a succinct reformulation of New and Licata's Virtual Equipment Type Theory (VETT). FVDblTT formalizes reasoning on isomorphisms that are commonly employed in category theory. Virtual double categories are one of the most successful frameworks for developing formal category theory, and FVDblTT has them as a theoretical foundation. We validate its worth as an internal language of virtual double categories by providing a syntax-semantics duality between virtual double categories and specifications in FVDblTT as a biadjunction.