open import Category.Core

module Category.Properties {ℓ₁ ℓ₂} (𝐂 : Category {ℓ₁} {ℓ₂}) where
  open Category 𝐂

  unique-identity : ∀ {A} → ∀ (f : Hom A A) → (∀ {B} → ∀ (g : Hom A B) → g ∘ f ≡ g) → f ≡ 𝟙
  unique-identity f H =
    begin
      f
    ≡⟨ sym (identity-ˡ f) ⟩
      𝟙 ∘ f
    ≡⟨ H 𝟙 ⟩
      𝟙
    ∎