Total Relation

A Relation R : A × B → Ω : 𝑅 → 𝐴 𝐵 Ω R:A\times B\to\Omega is total if for every a : A : 𝑎 𝐴 a:A , there merely exists some b : B : 𝑏 𝐵 b:B such that R ⁢ ( a , b ) 𝑅 𝑎 𝑏 R(a,b) .

In an Allegory

We can rephrase the above definition into the language of an Allegory by defining totality as id ≤ R † ∘ R id superscript 𝑅 † 𝑅 \mathrm{id}\leq R^{\dagger}\circ R . If we unfold things in the Category of Relations, we get that ∀ x , y . x = y → ∃ b . R ⁢ ( x , b ) ∧ R ⁢ ( y , b ) formulae-sequence for-all 𝑥 𝑦 𝑥 𝑦 → 𝑏 𝑅 𝑥 𝑏 𝑅 𝑦 𝑏 \forall x,y.\;x=y\to\exists b.\;R(x,b)\land R(y,b) , which is equivalent to the above definition.