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