Lemma Poset_univalence_compute {X Y:Poset} (e:X=Y) : Poset_univalence_0 X Y e = Poset_univalence_map e.
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.