{A B : Type} {z z' : A + B} (c : code_sum z z') : z = z'. Proof. destruct z, z'. - apply ap, c. - elim c. - elim c. - apply ap, c. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.