no goals
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ (IsInitial.uniqueUpToIso initialIsInitial HasZeroObject.zeroIsInitial).hom ≫ 0 = initial.to B
simp