We now define the three-dimensional multiverse of logics.
<aside> 🌱 All of this can be visualized — it just hasn’t been drawn yet!
</aside>
Proposition. Bifibrant double categories and double functors, vertical profunctors and vertical transformations form a double category, which we call $bf.\mathrm{Dbl\mathbb{C}at}$.
Proposition. Horizontal profunctors and horizontal transformations, double profunctors and double transformations form a double category, which we call $bf.\mathrm{Dbl\mathbb{P}rof}$.
Proposition. $bf.\mathrm{Dbl\mathbb{C}at}\leftarrow bf.\mathrm{Dbl\mathbb{P}rof}\to bf.\mathrm{Dbl\mathbb{C}at}$ is a fibered logic.
Proof. Substitution of double functors in a horizontal profunctor, and vertical transformations in a double profunctor, are defined by pullback. Sequential composition of vertical profunctors preserves this substitution, in the same way as for matrix profunctors.
Composition of horizontal profunctors is defined in the same way as that of matrix categories: by a codescent object, which adjoins a coherent associator for the middle action — in fact, all the proofs are essentially the same. The only difference is now $\mathbb{B}$ is a general bifibrant double category, rather than a weave double category $\langle\mathbb{B}\rangle$.
Let $\mathcal{R}(\mathbb{A,B})$ and $\mathcal{S}(\mathbb{B,C})$ be horizontal profunctors.
The parallel composite $(\mathcal{R\otimes S})(\mathbb{A,C})$ is formed as follows. To the composite matrix category $\mathcal{R}\otimes_\mathbb{M}\mathcal{S}$ we adjoin for every $B:\mathbb{B}(\mathrm{B_0,B_1})$ an associator $\mathrm{B_0}.(R\circ B,S)\cong \mathrm{B_1}.(R,B\circ S)$, by iso-coinserter.