Definition decidable_dirprod (X Y : UU) : decidable X -> decidable Y -> decidable (X × Y). Proof. intros b c. induction b as [b|b']. - induction c as [c|c']. + apply ii1. exact (b,,c). + apply ii2. clear b. intro k. apply c'. exact (pr2 k). - clear c. apply ii2. intro k. apply b'. exact (pr1 k). Defined.