{A B C} (f : C -> A + B) (z : decompose_l f) : is_inl (f (equiv_decompose f (inl z))) := z.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.