Definition coprodasstor (X Y Z : UU) : (X ⨿ Y) ⨿ Z -> X ⨿ (Y ⨿ Z). Proof. intros X0. induction X0 as [ c | z ]. induction c as [ x | y ]. apply (ii1 x). apply (ii2 (ii1 y)). apply (ii2 (ii2 z)). Defined.