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