C : Type u₁
inst✝ : Category C
X Y : C
t : IsInitial X
f : Y ⟶ X
this : IsSplitEpi f
⊢ Epi f
C : Type u₁
inst✝ : Category C
X Y : C
t : IsInitial X
f : Y ⟶ X
⊢ Epi f
haveI := t.isSplitEpi_to f
no goals
C : Type u₁
inst✝ : Category C
X Y : C
t : IsInitial X
f : Y ⟶ X
this : IsSplitEpi f
⊢ Epi f
infer_instance