Virtual double categories of split two-sided 2-fibrations

TL;DR

This paper develops a categorical framework for split two-sided 2-fibrations within a virtual double category setting, generalizing existing notions and establishing a two-sided Grothendieck correspondence with universal properties.

Contribution

It introduces split two-sided 2-fibrations and their virtual double category structure, extending Street's notion to sesquicategories and establishing a two-sided Grothendieck correspondence.

Findings

Constructed a virtual double category of split two-sided 2-fibrations.

Demonstrated Yoneda 2-functors satisfy a formal double-categorical Yoneda property.

Extended the Grothendieck correspondence to a two-sided setting with functorial properties.

Abstract

This paper introduces and studies split two-sided 2-fibrations and locally discrete split two-sided 2-fibrations, using a formal categorical approach. We generalise Street's notion of split two-sided fibration internal to a 2-category to one internal to a sesquicategory. Given a sesquicategory we construct a virtual double category whose horizontal (loose) morphisms are its internal split two-sided fibrations. Specialising to the sesquicategory of lax natural transformations we obtain the virtual double category of split two-sided 2-fibrations, which we study in detail. We then restrict to the sub-virtual double category of locally discrete split two-sided 2-fibrations and show that therein the usual Yoneda 2-functors satisfy a double-categorical formal notion of Yoneda morphism, which formally captures universal properties similar to those satisfied by the morphisms comprising a Yoneda structure on a 2-category. As a consequence we obtain a 'two-sided Grothendieck correspondence' of locally discrete split two-sided 2-fibrations $A \nrightarrow B$ and 2-functors $B \to Cat^{A^{op}}$. Restricting to $A = 1$, the terminal 2-category, we improve Buckley and Lambert's 'Grothendieck correspondence' for locally discrete split op-2-fibrations by extending the sense in which it is functorial.