proposition: Lemma posetStructureIdentity {X:hSet} (R S:PartialOrder X) : @isPosetEquivalence (X,,R) (X,,S) (idweq X) <-> (R=S)%type.
proof: Proof. intros. split. { intros e. apply subtypePath. { intros T. apply isaprop_isPartialOrder. } induction R as [R r]; induction S as [S s]; simpl. apply funextfun; intro x; apply funextfun; intro y. unfold isPosetEquivalence in e. unfold isaposetmorphism in e; simpl in e. induction e as [e e']. unfold posetRelation in *. unfold invmap in *; simpl in *. apply hPropUnivalence. { apply e. } { apply e'. } } { intros p. induction p. apply isPosetEquivalence_idweq. } Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions