Definition make_posetmorphism (X Y : Poset) : ∏ t : X → Y, isaposetmorphism t → ∑ f : X → Y, isaposetmorphism f := tpair (fun f : X -> Y => isaposetmorphism f).
Require Import UniMath.Foundations.UnivalenceAxiom.