proposition: Lemma Poset_univalence_compute {X Y:Poset} (e:X=Y) : Poset_univalence_0 X Y e = Poset_univalence_map e.
proof: Proof. try reflexivity. Abort. Theorem Poset_univalence (X Y:Poset) : X=Y ≃ X≅Y. Proof. intros. assert (k : pr1weq (Poset_univalence_0 X Y) ~ @Poset_univalence_map X Y). { intro e. apply isinj_pr1_PosetEquivalence. induction e. reflexivity. } exact (remakeweq k). Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions