case w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
j✝ : J
⊢ ι (fun b => f b) j✝ ≫ map p ≫ desc k = ι (fun b => f b) j✝ ≫ desc fun j => p j ≫ k j
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
⊢ map p ≫ desc k = desc fun j => p j ≫ k j
ext
no goals
case w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
j✝ : J
⊢ ι (fun b => f b) j✝ ≫ map p ≫ desc k = ι (fun b => f b) j✝ ≫ desc fun j => p j ≫ k j
simp