fact: Definition unfunctor_sum_l_compose {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)).
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall