C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f = default
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ HasZeroObject C
refine' ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩⟩
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f = default
calc
  f = f ≫ 𝟙 _ := (Category.comp_id _).symm
  _ = f ≫ 0 := by congr!
  _ = 0 := HasZeroMorphisms.comp_zero _ _
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
⊢ ∀ (a : ⊥_ C ⟶ X), a = default
aesop_cat
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f ≫ 𝟙 (⊥_ C) = f ≫ 0
congr!