Theorem isdecpropdirprod {X Y : UU} (isx : isdecprop X) (isy : isdecprop Y) : isdecprop (X × Y). Proof. intros. assert (isp : isaprop (X × Y)) by apply (isofhleveldirprod 1 _ _ (isdecproptoisaprop _ isx) (isdecproptoisaprop _ isy)). induction (pr1 isx) as [ x | nx ]. - induction (pr1 isy) as [ y | ny ]. + apply (isdecpropif _ isp (ii1 (make_dirprod x y))). + assert (nxy : neg (X × Y)). { intro xy. induction xy as [ x0 y0 ]. apply (ny y0). } apply (isdecpropif _ isp (ii2 nxy)). - assert (nxy : neg (X × Y)). { intro xy. induction xy as [ x0 y0 ]. apply (nx x0). } apply (isdecpropif _ isp (ii2 nxy)). Defined.