From 7841632fb636118a38a302445e2dea39c50c7b8a Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 13 Oct 2024 22:19:48 -0700 Subject: [PATCH] initial/terminal objects and products --- src/Category/Definitions.agda | 154 ++++++++++++++++++++++++++++++---- src/Category/Utils.agda | 28 +++++++ 2 files changed, 167 insertions(+), 15 deletions(-) create mode 100644 src/Category/Utils.agda diff --git a/src/Category/Definitions.agda b/src/Category/Definitions.agda index 682761f..7074c01 100644 --- a/src/Category/Definitions.agda +++ b/src/Category/Definitions.agda @@ -1,5 +1,6 @@ open import Category.Core -open import Data.Product using (_×_; Σ-syntax; ∃-syntax; _,_) +open import Category.Utils using (Σ!; Σ!-syntax) +open import Data.Product using (_×_; Σ-syntax; ∃-syntax; _,_; proj₁; proj₂) module Category.Definitions {ℓ₁ ℓ₂ ℓ₃} (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃}) where @@ -7,7 +8,7 @@ open Category 𝐂 private variable - a b : Obj + a b c : Obj f : Hom a b g : Hom b a @@ -22,20 +23,14 @@ IsInverse f g = IsLeftInverse f g × IsRightInverse f g inverse-unique : (f : Hom a b) → (g h : Hom b a) → IsInverse f g → IsInverse f h → g ≈ h inverse-unique f g h (gf≈1 , fg≈1) (hf≈1 , fh≈1) = - begin - g - ≈⟨ sym (identity-ʳ g) ⟩ - g ∘ 𝟙 - ≈⟨ sym (≈-resp-∘ refl fh≈1) ⟩ - g ∘ (f ∘ h) - ≈⟨ assoc g f h ⟩ - (g ∘ f) ∘ h - ≈⟨ ≈-resp-∘ gf≈1 refl ⟩ - 𝟙 ∘ h - ≈⟨ identity-ˡ h ⟩ - h - ∎ + begin g ≈⟨ sym (identity-ʳ g) ⟩ + g ∘ 𝟙 ≈⟨ sym (≈-resp-∘ refl fh≈1) ⟩ + g ∘ (f ∘ h) ≈⟨ assoc g f h ⟩ + (g ∘ f) ∘ h ≈⟨ ≈-resp-∘ gf≈1 refl ⟩ + 𝟙 ∘ h ≈⟨ identity-ˡ h ⟩ + h ∎ where open HomReasoning + open Eq IsIsomorphism : (f : Hom a b) → Set _ IsIsomorphism f = ∃[ g ] IsInverse f g @@ -45,3 +40,132 @@ _⁻¹ f {g , _} = g _≅_ : Obj → Obj → Set _ a ≅ b = Σ[ f ∈ Hom a b ] IsIsomorphism f + +mono : {a b : Obj} → Hom a b → Set _ +mono {a} f = (c : Obj) → (g h : Hom c a) → f ∘ g ≈ f ∘ h → g ≈ h + +epi : {a b : Obj} → Hom a b → Set _ +epi {_} {b} f = (c : Obj) → (g h : Hom b c) → g ∘ f ≈ h ∘ f → g ≈ h + +mono-syntax : (a b : Obj) → Hom a b → Set _ +mono-syntax a b f = mono f + +syntax mono-syntax a b f = f :: a ↣ b + +epi-syntax : (a b : Obj) → Hom a b → Set _ +epi-syntax a b f = epi f + +syntax epi-syntax a b f = f :: a ↠ b + +left-inverse→mono : (f : Hom a b) → (f⁻¹ : Hom b a) → IsLeftInverse f f⁻¹ → mono f +left-inverse→mono f f⁻¹ left-inverse c g h f∘g≈f∘h = + begin g ≈⟨ sym (identity-ˡ g) ⟩ + 𝟙 ∘ g ≈⟨ sym (≈-resp-∘ left-inverse refl) ⟩ + (f⁻¹ ∘ f) ∘ g ≈⟨ sym (assoc f⁻¹ f g) ⟩ + f⁻¹ ∘ (f ∘ g) ≈⟨ ≈-resp-∘ refl f∘g≈f∘h ⟩ + f⁻¹ ∘ (f ∘ h) ≈⟨ assoc f⁻¹ f h ⟩ + (f⁻¹ ∘ f) ∘ h ≈⟨ ≈-resp-∘ left-inverse refl ⟩ + 𝟙 ∘ h ≈⟨ identity-ˡ h ⟩ + h + ∎ + where open HomReasoning + open Eq + +right-inverse→epi : (f : Hom a b) → (f⁻¹ : Hom b a) → IsRightInverse f f⁻¹ → epi f +right-inverse→epi f f⁻¹ right-inverse c g h g∘f≈h∘f = + begin g ≈⟨ sym (identity-ʳ g) ⟩ + g ∘ 𝟙 ≈⟨ sym (≈-resp-∘ refl right-inverse) ⟩ + g ∘ (f ∘ f⁻¹) ≈⟨ assoc g f f⁻¹ ⟩ + (g ∘ f) ∘ f⁻¹ ≈⟨ ≈-resp-∘ g∘f≈h∘f refl ⟩ + (h ∘ f) ∘ f⁻¹ ≈⟨ sym (assoc h f f⁻¹) ⟩ + h ∘ (f ∘ f⁻¹) ≈⟨ ≈-resp-∘ refl right-inverse ⟩ + h ∘ 𝟙 ≈⟨ identity-ʳ h ⟩ + h ∎ + where open HomReasoning + open Eq + +initial : (a : Obj) → Set _ +initial a = ∀ (c : Obj) → Σ! (Hom a c) _≈_ + +terminal : (a : Obj) → Set _ +terminal a = ∀ (c : Obj) → Σ! (Hom c a) _≈_ + +initial-uniq : (a b : Obj) → initial a → initial b → a ≅ b +initial-uniq a b a-i b-i = + let (f , _) = a-i b in + let (g , _) = b-i a in + let (aa , aa-uniq) = a-i a in + let (bb , bb-uniq) = b-i b in + f , g , (begin + g ∘ f ≈⟨ sym (aa-uniq (g ∘ f)) ⟩ + aa ≈⟨ aa-uniq 𝟙 ⟩ + 𝟙 ∎) , + (begin + f ∘ g ≈⟨ sym (bb-uniq (f ∘ g)) ⟩ + bb ≈⟨ bb-uniq 𝟙 ⟩ + 𝟙 ∎ + ) + where open HomReasoning + open Eq + +terminal-uniq : (a b : Obj) → terminal a → terminal b → a ≅ b +terminal-uniq a b a-t b-t = + let (f , _) = b-t a in + let (g , _) = a-t b in + let (aa , aa-uniq) = a-t a in + let (bb , bb-uniq) = b-t b in + f , g , (begin + g ∘ f ≈⟨ sym (aa-uniq (g ∘ f)) ⟩ + aa ≈⟨ aa-uniq 𝟙 ⟩ + 𝟙 ∎) , + (begin + f ∘ g ≈⟨ sym (bb-uniq (f ∘ g)) ⟩ + bb ≈⟨ bb-uniq 𝟙 ⟩ + 𝟙 ∎) + where open HomReasoning + open Eq + +product : ∀ (a b a×b : Obj) → Set _ +product a b a×b = Σ[ π₁ ∈ Hom a×b a ] + Σ[ π₂ ∈ Hom a×b b ] + ∀ (c : Obj) → (x₁ : Hom c a) → (x₂ : Hom c b) → + Σ![ u ∈ Hom c a×b / _≈_ ] + π₁ ∘ u ≈ x₁ × π₂ ∘ u ≈ x₂ + +product-uniq : ∀ (a b a×b a×b′ : Obj) → product a b a×b → product a b a×b′ → a×b ≅ a×b′ +product-uniq a b a×b a×b′ (π₁ , π₂ , u) (π₁′ , π₂′ , u′) + using (f , (π₁∘g≈π₁′ , π₂∘g≈π₂′) , _) ← u′ a×b π₁ π₂ + using (g , (π₁′∘f≈π₁ , π₂′∘f≈π₂) , _) ← u a×b′ π₁′ π₂′ + using (id , _ , id-uniq) ← u a×b π₁ π₂ + using (id′ , _ , id′-uniq) ← u′ a×b′ π₁′ π₂′ + = f , g , ( + begin g ∘ f ≈⟨ sym (id-uniq (g ∘ f) (gfsat₁ , gfsat₂)) ⟩ + id ≈⟨ id-uniq 𝟙 (identity-ʳ π₁ , identity-ʳ π₂) ⟩ + 𝟙 ∎ + ) , ( + begin f ∘ g ≈⟨ sym (id′-uniq (f ∘ g) (fgsat₁ , fgsat₂)) ⟩ + id′ ≈⟨ id′-uniq 𝟙 (identity-ʳ π₁′ , identity-ʳ π₂′) ⟩ + 𝟙 ∎ + ) + where open HomReasoning + open Eq + gfsat₁ : π₁ ∘ (g ∘ f) ≈ π₁ + gfsat₁ = begin π₁ ∘ (g ∘ f) ≈⟨ assoc π₁ g f ⟩ + (π₁ ∘ g) ∘ f ≈⟨ ≈-resp-∘ π₁′∘f≈π₁ refl ⟩ + π₁′ ∘ f ≈⟨ π₁∘g≈π₁′ ⟩ + π₁ ∎ + gfsat₂ : π₂ ∘ (g ∘ f) ≈ π₂ + gfsat₂ = begin π₂ ∘ (g ∘ f) ≈⟨ assoc π₂ g f ⟩ + (π₂ ∘ g) ∘ f ≈⟨ ≈-resp-∘ π₂′∘f≈π₂ refl ⟩ + π₂′ ∘ f ≈⟨ π₂∘g≈π₂′ ⟩ + π₂ ∎ + fgsat₁ : π₁′ ∘ (f ∘ g) ≈ π₁′ + fgsat₁ = begin π₁′ ∘ (f ∘ g) ≈⟨ assoc π₁′ f g ⟩ + (π₁′ ∘ f) ∘ g ≈⟨ ≈-resp-∘ π₁∘g≈π₁′ refl ⟩ + π₁ ∘ g ≈⟨ π₁′∘f≈π₁ ⟩ + π₁′ ∎ + fgsat₂ : π₂′ ∘ (f ∘ g) ≈ π₂′ + fgsat₂ = begin π₂′ ∘ (f ∘ g) ≈⟨ assoc π₂′ f g ⟩ + (π₂′ ∘ f) ∘ g ≈⟨ ≈-resp-∘ π₂∘g≈π₂′ refl ⟩ + π₂ ∘ g ≈⟨ π₂′∘f≈π₂ ⟩ + π₂′ ∎ diff --git a/src/Category/Utils.agda b/src/Category/Utils.agda new file mode 100644 index 0000000..9396b29 --- /dev/null +++ b/src/Category/Utils.agda @@ -0,0 +1,28 @@ +open import Data.Product using (Σ; ∃; _×_) +open import Level using (Level; _⊔_) + +module Category.Utils where + +private + variable + a b ℓ : Level + +∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ) +∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y) + +∃!-syntax : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ) +∃!-syntax = ∃! + +syntax ∃!-syntax _≈_ (λ x → B) = ∃![ x / _≈_ ] B + +Σ! : (A : Set a) → (A → A → Set ℓ) → Set (a ⊔ ℓ) +Σ! A _≈_ = Σ A (λ x → ∀ y → x ≈ y) + +Σ!-st : (A : Set a) → (A → A → Set ℓ) → (B : A → Set b) → Set (a ⊔ b ⊔ ℓ) +Σ!-st A _≈_ B = Σ A (λ x → B x × ∀ y → B y → x ≈ y) + +Σ!-syntax : (A : Set a) → (A → A → Set ℓ) → (B : A → Set b) → Set (a ⊔ b ⊔ ℓ) +Σ!-syntax = Σ!-st + +infix 2 Σ!-syntax +syntax Σ!-syntax A _≈_ (λ x → B) = Σ![ x ∈ A / _≈_ ] B