Definition equality_cases {P Q : UU} (x x' : P ⨿ Q) : UU. Proof. intros. induction x as [p|q]. - induction x' as [p'|q']. + exact (p = p'). + exact empty. - induction x' as [p'|q']. + exact empty. + exact (q = q'). Defined.