Lemma isStrongOrder_bck {X Y : UU} (f : Y → X) (gt : hrel X) : isStrongOrder gt → isStrongOrder (fun_hrel_comp f gt). Proof. intros is. split ; [ | split ]. - intros x y z. apply (istrans_isStrongOrder is). - intros x y z. apply (iscotrans_isStrongOrder is). - intros x. apply (isirrefl_isStrongOrder is). Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.