Partial Functional Relation

A Relation is a partial functional relation if for b 1 , b 2 subscript 𝑏 1 subscript 𝑏 2 b_{1},b_{2} , if R ⁢ ( a , b 1 ) 𝑅 𝑎 subscript 𝑏 1 R(a,b_{1}) and R ⁢ ( a , b 2 ) 𝑅 𝑎 subscript 𝑏 2 R(a,b_{2}) for any a 𝑎 a , then b 1 = b 2 subscript 𝑏 1 subscript 𝑏 2 b_{1}=b_{2} .

In an Allegory

We can rephrase the above definition into the language of an Allegory by defining partial functionality as R ∘ R † ≤ id 𝑅 superscript 𝑅 † id R\circ R^{\dagger}\leq\mathrm{id} . If we unfold this in the Category of Relations, then we get ∀ b 1 , b 2 . ( ∃ a . R ( a , b 1 ∧ R ( a , b 2 ) ) ) → b 1 = b 2 \forall b_{1},b_{2}.\;(\exists a.\;R(a,b_{1}\land R(a,b_{2})))\to b_{1}=b_{2} , which is precisely the definition given above.