Definition StrongOrder_setquot {X : UU} {R : eqrel X} {L : StrongOrder X} (is : iscomprelrel R L) : StrongOrder (setquot R) := quotrel is,, isStrongOrder_setquot is (pr2 L).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.