initial/terminal objects and products

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
+  begin g          ≈⟨ sym (identity-ʳ g) ⟩
-    g
+    g ∘ 𝟙          ≈⟨ sym (≈-resp-∘ refl fh≈1) ⟩
-  ≈⟨ sym (identity-ʳ g) ⟩
+    g ∘ (f ∘ h)    ≈⟨ assoc g f h ⟩
-    g ∘ 𝟙
+    (g ∘ f) ∘ h    ≈⟨ ≈-resp-∘ gf≈1 refl ⟩
-  ≈⟨ sym (≈-resp-∘ refl fh≈1) ⟩
+    𝟙 ∘ h          ≈⟨ identity-ˡ h ⟩
-    g ∘ (f ∘ h)
+    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≈π₂ ⟩
+                         π₂′ ∎

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