no goals
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
ext <;> simp [← Functor.map_comp]