Definition subpreorder : po A. Proof. use make_po. - exact (resrel P A). - abstract ( split; [ apply istransresrel; apply istrans_po | apply isreflresrel; apply isrefl_po ] ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All.