C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)
let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)
have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := iso hF hG
⊢ IsZero (F.obj X)
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)
let e : F ≅ G := hF.iso hG
no goals
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := iso hF hG
⊢ IsZero (F.obj X)
exact (isZero_zero _).of_iso (e.app X)