{A A' A'' B B' B'' : Type} (h : A + B -> A' + B') (k : A' + B' -> A'' + B'') (Ha : forall a:A, is_inl (h (inl a))) (Ha' : forall a':A', is_inl (k (inl a'))) : unfunctor_sum_l k Ha' o unfunctor_sum_l h Ha == unfunctor_sum_l (k o h) (fun a => is_inl_ind (fun x' => is_inl (k x')) Ha' (h (inl a)) (Ha a)). Proof. intros a. refine (path_sum_inl B'' _). refine (unfunctor_sum_l_beta _ _ _ @ _). refine (ap k (unfunctor_sum_l_beta _ _ _) @ _). refine ((unfunctor_sum_l_beta _ _ _)^). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.