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