Definition tosubtypesdirprodcarrier {X Y : UU} (A : hsubtype X) (B : hsubtype Y) (xisyis : dirprod A B) : subtypesdirprod A B. Proof. intros. set (xis := pr1 xisyis). set (yis := pr2 xisyis). set (x := pr1 xis). set (isx := pr2 xis). set (y := pr1 yis). set (isy := pr2 yis). simpl in isx. simpl in isy. apply (tpair (subtypesdirprod A B) (make_dirprod x y) (make_dirprod isx isy)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.