proposition: Lemma Poset_univalence_compute {X Y:Poset} (e:X=Y) : Poset_univalence X Y e = Poset_univalence_map e.
proof: Proof. reflexivity. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions