Lemma posetStructureIdentity {X:hSet} (R S:PartialOrder X) : @isPosetEquivalence (X,,R) (X,,S) (idweq X) <-> (R=S)%type. 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.
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.