{A B} (z z' : A + B) : Type := match z, z' with | inl a, inl a' => a = a' | inr b, inr b' => b = b' | _, _ => Empty end.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.