{A A' A'' B B' B'' : Type} (h : A + B -> A' + B') (k : A' + B' -> A'' + B'') (Hb : forall b:B, is_inr (h (inr b))) (Hb' : forall b':B', is_inr (k (inr b'))) : unfunctor_sum_r k Hb' o unfunctor_sum_r h Hb == unfunctor_sum_r (k o h) (fun b => is_inr_ind (fun x' => is_inr (k x')) Hb' (h (inr b)) (Hb b)). Proof. intros b. refine (path_sum_inr A'' _). refine (unfunctor_sum_r_beta _ _ _ @ _). refine (ap k (unfunctor_sum_r_beta _ _ _) @ _). refine ((unfunctor_sum_r_beta _ _ _)^). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.