Theorem PosetEquivalence_rect (X Y : Poset) (P : X ≅ Y -> UU) : (∏ e : X = Y, P (Poset_univalence_map e)) -> ∏ f, P f. Proof. intros ih ?. set (p := ih (invmap (Poset_univalence _ _) f)). set (h := homotweqinvweq (Poset_univalence _ _) f). exact (transportf P h p). 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.