Category of Profunctors

definition theorem proof

Theorem 4.23. For any skeletal Quantale $\mathcal{V}$ there is a category ${\mathbf{Prof}}_{\mathcal{V}}$ whose objects are $\mathcal{V}$-categories, whose morphisms $\mathcal{X}\nrightarrow \mathcal{Y}$ are $\mathcal{V}$-profunctors, with composition

$$(\Phi ;\Psi )(p,r):=\underset{q\in \mathcal{Q}}{\bigvee }\Phi (p,q)\otimes \Psi (q,r)$$

(Definition 4.21 — Matrix Multiplication in a Quantale) and identities the unit profunctors $U_{\mathcal{X}}(x,y):=\mathcal{X}(x,y)$ (Eq. 4.25). $\mathbf{Feas}:={\mathbf{Prof}}_{\mathbf{Bool}}$ is the category of preorders and feasibility relations (Definition 4.24).

Sources: 7 Sketches §4.3 (Definitions 4.21, 4.24, Theorem 4.23, Eq. 4.25, Lemmas 4.27, 4.31, Remark 4.33, Exercises 4.22, 4.26, 4.30, 4.32), §4.5.2 (Theorem 4.63); DaoFP §17.2, §17.8 (“The Bicategory of Profunctors”).

Composition as navigation (Eq. 4.19–4.20)

Given bridges $\Phi :P\nrightarrow Q$ and $\Psi :Q\nrightarrow R$ between three cities, the composite feasibility matrix is found by a navigator: for each $p,r$, search $Q$ for a way-point $q$ reachable from $p$ AND from which $r$ is reachable — “a big OR over all possible $q$”: $(\Phi ;\Psi )(p,r)={\bigvee }_q\Phi (p,q)\wedge \Psi (q,r)$. In the example, you cannot get from $N$ to $x$ but you can from $N$ to $y$. For Cost: min-plus products of distance matrices (7S Exercise 4.22).

Unitality (Lemma 4.27)

$U_P;\Phi =\Phi =\Phi ;U_Q$. Proof. Skeletality lets us prove equality by two inequalities. (i) $\Phi (p,q)=I\otimes \Phi (p,q)\le P(p,p)\otimes \Phi (p,q)\le {\bigvee }_{p_1}P(p,p_1)\otimes \Phi (p_1,q)=(U_P;\Phi )(p,q)$ — unit law, $I\le P(p,p)$ with monotonicity of $\otimes$, the join bound, and the definition (Eq. 4.28). (ii) For each $p_1$, $P(p,p_1)\otimes \Phi (p_1,q)=P(p,p_1)\otimes \Phi (p_1,q)\otimes I\le P(p,p_1)\otimes \Phi (p_1,q)\otimes Q(q,q)\le \Phi (p,q)$ by the profunctor inequality of 7S Exercise 4.9 (Eq. 4.29); hence the join is $\le \Phi (p,q)$. $■$ (7S Exercise 4.30; in $\mathbf{Bool}$ all four steps are equalities.) Associativity (Lemma 4.31, 7S Exercise 4.32) uses distributivity of $\otimes$ over joins and skeletality.

Why skeletal? Without skeletality the unit laws hold only up to $\cong$; one can either take isomorphism classes of profunctors (as for cospans) or accept composition “up to isomorphism” — a bicategory (Remark 4.33; DaoFP §17.8: monads in $\mathbf{Prof}$ are prearrows).

Structure

• Every $\mathcal{V}$-functor embeds via its companion or conjoint; the identity functor’s companion is $U_{\mathcal{X}}$ (Example 4.35, 7S Exercise 4.36).
• Compact closed (Theorem 4.63): monoidal product is the product of $\mathcal{V}$-categories with $(\Phi \times \Psi )((x_1,y_1),(x_2,y_2))=\Phi (x_1,x_2)\otimes \Psi (y_1,y_2)$ (“stacking wires with no new interaction”; for feasibility: provide both given both, 7S Exercise 4.64); the unit is the one-object $\mathcal{V}$-category $1$ with $1(1,1)=I$ (7S Exercise 4.65: the unitors are the profunctors $\mathcal{X}\times 1\nrightarrow \mathcal{X}$ given by $\mathcal{X}(x,x^{\prime })$); the dual of $\mathcal{X}$ is ${\mathcal{X}}^{\mathrm{op}}$ with unit ${\eta }_{\mathcal{X}}:1\nrightarrow {\mathcal{X}}^{\mathrm{op}}\times \mathcal{X}$, $\eta (1,x,x^{\prime })=\mathcal{X}(x,x^{\prime })$, and counit ${\epsilon }_{\mathcal{X}}:\mathcal{X}\times {\mathcal{X}}^{\mathrm{op}}\nrightarrow 1$, $\epsilon (x,x^{\prime },1)=\mathcal{X}(x,x^{\prime })$ — “the unit and counit look like identities” (7S Exercise 4.66 checks the snake equations). See Compact Closed Category.
• In wiring-diagram terms, boxes are feasibility relations with one input and one output wire (a plain category) — but $\mathbf{Feas}$‘s monoidal and compact structure allows the rich Co-design diagrams with many ports and feedback.

JuliaLeanHaskell

Docs: plain Julia — Catlab has no dedicated API for this; related: Catlab v0.16 docs · GATlab standard library

Builds on: Bool (Monoidal Preorder) (BoolPre), Enriched Category (VCategory), Profunctor (VProfunctor) — run those notes’ Julia code first.

# Feas: compose Bool-profunctors (feasibility matrices) by Bool matrix multiplication (Eq. 4.20)
Φ = Bool[1 0 1 0 0; 1 0 1 0 1; 1 1 1 1 0; 1 1 1 1 1]      # N, E, W, S × a..e
Ψ = Bool[0 1; 1 1; 0 1; 1 1; 0 0]                        # a..e × x, y
qmul(BoolPre(), Φ, Ψ)      # [0 1; 0 1; 1 1; 1 1]: you can't get from N to x but you can to y
unit_profunctor(X::VCategory) = VProfunctor(X, X, X.hom)   # U_X(x, y) = X(x, y)

-- Mathlib has no bundled Prof_V; for V = Bool on preorders one can model composition as
-- relational composition of monotone relations (see `Rel.comp`)
#check @Rel.comp

-- Feas: objects are preorders, morphisms feasibility relations, composition by "search for a way-point"
composeFeas :: [q] -> Feas p q -> Feas q r -> Feas p r
composeFeas qs (Feas phi) (Feas psi) = Feas (\p r -> or [ phi p q && psi q r | q <- qs ])
 
unitFeas :: Preorder x => Feas x x
unitFeas = Feas leq                      -- U_X(x, y) = X(x, y)