13. Deductive squares [0037]

Let $\mathbb C$ be a 2-category equipped with a class $\mathbb E$ of squares called exacts (for example, the exact squares in the sense of $H$ or $H^\op$ or $M$, cf. (Guitart, 1980)), and let $K$ be a class of morphisms of $\mathbb C$ called “canonical comparisons” (for example, monomorphisms of $\mathbb C$, or epimorphisms, or morphisms in $\mathbb C$ having an adjoint 1-cell,…). In the same notation of §9 we give the following definition.

[0038] Definition 13·a (Deductive square).

A square

will be called $\mathbb E$-$K$-deductive if the following data exist:

  • an exact $\mathbb E$-modification $\lambda$ from $(S,T)$ to
  • an exact $\mathbb E$-modification $\mu$ from $(U,V)$ to
  • a morphism $k : a’\to b’$ of $K$ such that $k * \lambda=\mu$.

The 2-category $\Rel_{\mathbb E,K}(\mathbb C)$ has objects those of $\mathbb C$ and as morphisms the elements of $Re(\mathbb E)$, called relations, and 2-morphisms generated by the $\mathbb E$-$K$-deductive squares, that will be called proofs.

This way to describe the 2-category of relations improves the one given in §3 of (Guitart, 1980).