{A A' B B' : Type} (h : A + B -> A' + B') (Hb : forall b:B, is_inr (h (inr b))) : inr o unfunctor_sum_r h Hb == h o inr. Proof. intros b; unfold unfunctor_sum_r; apply inr_un_inr. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.