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 : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
j✝ : J
⊢ (lift k ≫ map p) ≫ π (fun b => g b) j✝ = (lift fun j => k j ≫ p j) ≫ π (fun b => g b) j✝
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
⊢ lift k ≫ map p = lift fun j => k j ≫ p 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 : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
j✝ : J
⊢ (lift k ≫ map p) ≫ π (fun b => g b) j✝ = (lift fun j => k j ≫ p j) ≫ π (fun b => g b) j✝
simp