Dual Equipments

The significance of fibrations to categorical logic is well-understood [2]. Elementary existential fibrations (EEFs), for example, model specifications of regular logic, the fragment of first-order logic whose logical operations consist only of $\top ,\wedge ,$ and $\exists$.

In [3], Nasu established an equivalence between EEFs and a flavour of equipment, building on a construction from Shulman in [4], effectively bringing the logical connections associated with the fibrations into the double-categorical realm. Equipments are double categories for which the data of the tight structure is effectively encoded as part of the loose structure, in the form of companions and conjoints associated to each tight morphism. A typical example is the equipment $ℝ$el, whose objects are sets, tight morphisms $f:A\to B$ are functions, loose morphisms $R:A\begin{array}{c}\mapsto \\ \to \hfill \end{array}C$ are relations $R\subseteq A\times C$ (composed in the usual way), and there is a unique cell

iff the implication $(a,c)\in R\Rightarrow (f(a),g(c))\in S$ holds. $ℝ$el is an equipment, in which the companion of a tight morphism $f:A\to B$ is its graph $f_{\ast }=\{(a,b)|f(x)=y\}\subseteq A\times B$, and the conjoint $f^{\ast }$ of $f$ is the opposite relation $f^{\ast }\subseteq B\times A$. The fibration underlying $ℝ$el is $Sub(Set)$, the subobject fibration on $Set$.

A general goal of ours is to extend Nasu’s correspondence to lift more logically significant aspects of fibrations into double categories to study them there, in order to leverage the additional expressive power of double categories. In this talk, our main focus will be on the dual fibration construction. Given any fibration $p:ℰ\to ℬ$, one may define the dual fibration of $p$, denoted $p^{\bullet }:{ℰ}^{\bullet }\to ℬ$ over the same base category, where ${ℰ}^{\bullet }$ is obtained by taking fibrewise opposites in $ℰ$. According to Nasu’s result, in order for $p^{\bullet }$ to correspond to an equipment, which we denote $𝔹il(p^{\bullet })$, it must be elementary existential, meaning that $p$ must satisfy the duals of these properties to begin with. In this case, one could say that $𝔹il(p^{\bullet })$ is the dual equipment of the equipment $𝔹il(p)$ associated with $p$. In this talk, we will characterize these properties in both logical and double-categorical terms, and show the functorial semantics for dualizable equipments.

Our motivating example for dual equipments is the double category $ℝ$el^∙, which has the same objects, tight and loose morphisms as $ℝ$el, but where the composition of two relations $A\stackrel{𝑅}{\begin{array}{c}\mapsto \\ \to \hfill \end{array}}B\stackrel{𝑆}{\begin{array}{c}\mapsto \\ \to \hfill \end{array}}C$ is given by $R\oplus S≔\{(a,c)|\forall b\in B.(a,b)\in R\vee (b,c)\in S\}$ and cells $\alpha$ as above exist iff the converse implication $(f(a),g(c))\in S\Rightarrow (a,c)\in R$ holds. $ℝ$el^∙ is also an equipment, with companions and conjoints being given by complements of graphs of functions and their opposites, respectively, and its underlying fibration is (up to equivalence) the dual fibration of $Sub(Set)$. These “dual" notions of composing relations also appear in the study of linear logic via linear bicategories, and we expect dual equipments to connect to linear logic as well. This talk will also address some logical properties of $ℝ$el^∙, and the properties of $ℝ$el that induce them.