proposition: Lemma inducedPartialOrder {X Y} (f:X->Y) (incl:isInjective f) (R:hrel Y) (po:isPartialOrder R) : isPartialOrder (λ x x' : X, R (f x) (f x')).
proof: Proof. intros. split. - split. * intros x y z a b. exact (pr1 (pr1 po) (f x) (f y) (f z) a b). * intros x. exact (pr2 (pr1 po) (f x)). - intros x y a b. apply incl. exact (pr2 po (f x) (f y) a b). Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions