Lemma isaprop_isaposetmorphism {X Y : Poset} (f : X -> Y) : isaprop (isaposetmorphism f). Proof. intros. apply impredtwice; intros. apply impred_prop. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.