Definition fromdsubtypesdirprodcarrier {X Y : UU} (A : hsubtype X) (B : hsubtype Y) (xyis : subtypesdirprod A B) : dirprod A B. Proof. intros. set (xy := pr1 xyis). set (is := pr2 xyis). set (x := pr1 xy). set (y := pr2 xy). simpl in is. simpl in y. apply (make_dirprod (tpair A x (pr1 is)) (tpair B y (pr2 is))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.