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. 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.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.