Function Property for `rel`

Stream: Is there code for X?

[Marcus Rossel]

Is there a definition of the "function"-property of a relation, in the sense of : "it associates every instance of the first type to exactly one instance of the second type"?
And if so, is there a method for turning a rel α β into α → β?

[Yury G. Kudryashov]

We have docs#relator.right_unique and docs#relator.left_total

[Yury G. Kudryashov]

(BTW, they should be made non-classes because we have 0 instances)

[Yury G. Kudryashov]

You can use docs#classical.some to get f : α → β from ∀ x, ∃ y, r x y.