C : Type u₁
inst✝² : Category C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
C : Type u₁
inst✝² : Category C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g
rw [← cancel_mono (terminal.from A)]
no goals
C : Type u₁
inst✝² : Category C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
apply Subsingleton.elim