Definition StrongOrder_bck {X Y : UU} (f : Y → X) (gt : StrongOrder X) : StrongOrder Y := (fun_hrel_comp f gt) ,, isStrongOrder_bck f _ (pr2 gt).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.