C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ I = J
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ I = J
have : I.Zero = J.Zero := by
  funext X Y
  specialize w X Y
  apply congrArg Zero.mk w
case mk
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
J : HasZeroMorphisms C
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ mk = J
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ I = J
cases I
case mk.mk
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ mk = mk
case mk
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
J : HasZeroMorphisms C
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ mk = J
cases J
case mk.mk.h.e_4
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ HEq comp_zero✝¹ comp_zero✝

case mk.mk.h.e_5
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ HEq zero_comp✝¹ zero_comp✝
case mk.mk
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ mk = mk
congr
case h.h
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
X Y : C
⊢ Zero X Y = Zero X Y
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ Zero = Zero
funext X Y
case h.h
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
w : Zero.zero = Zero.zero
⊢ Zero X Y = Zero X Y
case h.h
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
X Y : C
⊢ Zero X Y = Zero X Y
specialize w X Y
no goals
case h.h
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
w : Zero.zero = Zero.zero
⊢ Zero X Y = Zero X Y
apply congrArg Zero.mk w
no goals
case mk.mk.h.e_4
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ HEq comp_zero✝¹ comp_zero✝
apply proof_irrel_heq
no goals
case mk.mk.h.e_5
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ HEq zero_comp✝¹ zero_comp✝
apply proof_irrel_heq