14 lines
388 B
Agda
14 lines
388 B
Agda
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 𝟙 ⟩
|
||
𝟙
|
||
∎
|