no goals
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (mapBiprod F X Y).hom ≫ desc (F.map f) (F.map g) = F.map (desc f g)
rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]