no goals
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ desc f g = fst ≫ f + snd ≫ g
ext <;> simp [add_comp]