Determinisation of relational substitutions in ordered categories with domain

Restating a unification problem as a single relational substitution instead of as multiple functional substitutions (or terms), a solution becomes a “determiniser” arrow and allows formalisation in the context of locally ordered categories with domain. This relies on the determinacy concept of “characterisation by domain” introduced by Desharnais and Möller for Kleene algebras with domain; this is here applied in the weakest possible setting.We …