Injective Types

> cotransitive (∀ x y z : X , x # y → x # z ∨ y # z).

If you're looking for a concrete point of reference, cotransitivity is why binary search works.