J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map' f g = g ≫ inr
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map f g = g ≫ inr
rw [biprod.map_eq_map']
no goals
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
P Q W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map' f g = g ≫ inr
exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.right⟩