C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g
haveI := hI.isIso_to f
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g
haveI := hI.isIso_to g
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))