The Agda Standard Library also uses the conventional term(s). See [Relation.Binary](https://agda.github.io/agda-stdlib/Relation.Binary.html).