Commit 2020-09-02 19:38 9d42f6c6

feat(order/rel_iso): define rel_hom (relation-preserving maps) (#3946) Creates a typeclass for (unidirectionally) relation-preserving maps that are not necessarily injective (In the case of <= relations, this is essentially a bundled monotone map) Proves that these transfer well-foundedness between relations