C : Type u₁
inst✝¹ : Category C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f ≫ IsTerminal.from hT A = g ≫ IsTerminal.from hT A
C : Type u₁
inst✝¹ : Category C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f = g
rw [← cancel_mono (hT.from A)]
no goals
C : Type u₁
inst✝¹ : Category C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f ≫ IsTerminal.from hT A = g ≫ IsTerminal.from hT A
apply hT.hom_ext