Refactor the 'Categories.Object.Zero' module

src/Categories/Object/Duality.agda

@@ -17,6 +17,7 @@ open import Categories.Object.Initial C
 open import Categories.Object.Product op
 open import Categories.Object.Coproduct C
 
+open import Categories.Object.Zero
 
 IsInitial⇒coIsTerminal : ∀ {X} → IsInitial X → IsTerminal X
 IsInitial⇒coIsTerminal is⊥ = record
@@ -72,6 +73,40 @@ coProduct⇒Coproduct A×B = record
   where
   module A×B = Product A×B
 
+-- Zero objects are autodual
+IsZero⇒coIsZero : ∀ {Z} → IsZero C Z → IsZero op Z
+IsZero⇒coIsZero is-zero = record
+  { isInitial = record { ! = ! ; !-unique = !-unique }
+  ; isTerminal = record { ! = ¡ ; !-unique = ¡-unique }
+  }
+  where
+    open IsZero is-zero
+
+coIsZero⇒IsZero : ∀ {Z} → IsZero op Z → IsZero C Z
+coIsZero⇒IsZero co-is-zero = record
+  { isInitial = record { ! = ! ; !-unique = !-unique }
+  ; isTerminal = record { ! = ¡ ; !-unique = ¡-unique }
+  }
+  where
+    open IsZero co-is-zero
+
+coZero⇒Zero : Zero op → Zero C
+coZero⇒Zero zero = record
+  { 𝟘 = 𝟘
+  ; isZero = coIsZero⇒IsZero isZero
+  }
+  where
+    open Zero zero
+
+Zero⇒coZero : Zero C → Zero op
+Zero⇒coZero zero = record
+  { 𝟘 = 𝟘
+  ; isZero = IsZero⇒coIsZero isZero
+  }
+  where
+    open Zero zero
+
+-- Tests to ensure that dualities are involutive up to definitional equality.
 private
   coIsTerminal⟺IsInitial : ∀ {X} (⊥ : IsInitial X) →
     coIsTerminal⇒IsInitial (IsInitial⇒coIsTerminal ⊥) ≡ ⊥
@@ -92,3 +127,19 @@ private
 
   coProduct⟺Coproduct : ∀ {A B} (p : Coproduct A B) → coProduct⇒Coproduct (Coproduct⇒coProduct p) ≡ p
   coProduct⟺Coproduct _ = ≡.refl
+
+  coIsZero⟺IsZero : ∀ {Z} {zero : IsZero op Z} →
+    IsZero⇒coIsZero (coIsZero⇒IsZero zero) ≡ zero
+  coIsZero⟺IsZero = ≡.refl
+
+  IsZero⟺coIsZero : ∀ {Z} {zero : IsZero C Z} →
+    coIsZero⇒IsZero (IsZero⇒coIsZero zero) ≡ zero
+  IsZero⟺coIsZero = ≡.refl
+
+  coZero⟺Zero : ∀ {zero : Zero op} →
+    Zero⇒coZero (coZero⇒Zero zero) ≡ zero
+  coZero⟺Zero = ≡.refl
+
+  Zero⟺coZero : ∀ {zero : Zero C} →
+    coZero⇒Zero (Zero⇒coZero zero) ≡ zero
+  Zero⟺coZero = ≡.refl

src/Categories/Object/Kernel.agda

@@ -42,7 +42,7 @@ record IsKernel {A B K} (k : K ⇒ A) (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) wher
   universal-∘ : f ∘ k ∘ h ≈ zero⇒ 
   universal-∘ {h = h} = begin
     f ∘ k ∘ h ≈⟨ pullˡ commute ⟩
-    zero⇒ ∘ h ≈⟨ pullʳ (⟺ (¡-unique (¡ ∘ h))) ⟩
+    zero⇒ ∘ h ≈⟨ zero-∘ʳ h ⟩
     zero⇒ ∎
 
 record Kernel {A B} (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where

src/Categories/Object/Kernel/Properties.agda

@@ -27,39 +27,39 @@ private
     A B : Obj
     f : A ⇒ B
 
--- We can express kernels as pullbacks along the morphism '! : ⊥ ⇒ A'.
-Kernel⇒Pullback : Kernel f → Pullback f !
+-- We can express kernels as pullbacks along the morphism '¡ : ⊥ ⇒ A'.
+Kernel⇒Pullback : Kernel f → Pullback f ¡
 Kernel⇒Pullback {f = f} kernel = record
   { p₁ = kernel⇒
-  ; p₂ = ¡
+  ; p₂ = !
   ; isPullback = record
     { commute = commute
     ; universal = λ {C} {h₁} {h₂} eq → universal {h = h₁} $ begin
       f ∘ h₁ ≈⟨ eq ⟩
-      ! ∘ h₂ ≈˘⟨ refl⟩∘⟨ ¡-unique h₂ ⟩
+      ¡ ∘ h₂ ≈˘⟨ refl⟩∘⟨ !-unique h₂ ⟩
       zero⇒ ∎
     ; unique = λ {C} {h₁} {h₂} {i} k-eq h-eq → unique $ begin
       h₁ ≈˘⟨ k-eq ⟩
       kernel⇒ ∘ i ∎
     ; p₁∘universal≈h₁ = ⟺ factors
-    ; p₂∘universal≈h₂ = ¡-unique₂ _ _
+    ; p₂∘universal≈h₂ = !-unique₂
     }
   }
   where
     open Kernel kernel
 
--- All pullbacks along the morphism '! : ⊥ ⇒ A' are also kernels.
-Pullback⇒Kernel : Pullback f ! → Kernel f
+-- All pullbacks along the morphism '¡ : ⊥ ⇒ A' are also kernels.
+Pullback⇒Kernel : Pullback f ¡ → Kernel f
 Pullback⇒Kernel {f = f} pullback = record
   { kernel⇒ = p₁
   ; isKernel = record
     { commute = begin
       f ∘ p₁ ≈⟨ commute ⟩
-      ! ∘ p₂ ≈˘⟨ refl⟩∘⟨ ¡-unique p₂ ⟩
+      ¡ ∘ p₂ ≈˘⟨ refl⟩∘⟨ !-unique p₂ ⟩
       zero⇒ ∎
     ; universal = λ eq → universal eq
     ; factors = ⟺ p₁∘universal≈h₁
-    ; unique = λ eq → unique (⟺ eq) (⟺ (¡-unique _))
+    ; unique = λ eq → unique (⟺ eq) (⟺ (!-unique _))
     }
   }
   where
@@ -72,9 +72,9 @@ Kernel⇒Equalizer {f = f} kernel = record
   ; isEqualizer = record
     { equality = begin
       f ∘ kernel⇒ ≈⟨ commute ⟩
-      zero⇒       ≈⟨ pushʳ (¡-unique (¡ ∘ kernel⇒)) ⟩
+      zero⇒       ≈˘⟨ zero-∘ʳ kernel⇒ ⟩
       zero⇒ ∘ kernel⇒ ∎
-    ; equalize = λ {_} {h} eq → universal (eq ○ pullʳ (⟺ (¡-unique (¡ ∘ h))))
+    ; equalize = λ {_} {h} eq → universal (eq ○ zero-∘ʳ h)
     ; universal = factors
     ; unique = unique
     }
@@ -89,9 +89,9 @@ Equalizer⇒Kernel {f = f} equalizer = record
   ; isKernel = record
     { commute = begin
       f ∘ arr      ≈⟨ equality ⟩
-      zero⇒ ∘ arr ≈⟨ pullʳ (⟺ (¡-unique (¡ ∘ arr))) ⟩
+      zero⇒ ∘ arr  ≈⟨ zero-∘ʳ arr ⟩
       zero⇒ ∎
-    ; universal = λ {_} {h} eq → equalize (eq ○ pushʳ (¡-unique (¡ ∘ h)))
+    ; universal = λ {_} {h} eq → equalize (eq ○ ⟺ (zero-∘ʳ h))
     ; factors = universal
     ; unique = unique
     }
@@ -111,8 +111,8 @@ module _ (K : Kernel f) where
 module _ (has-kernels : ∀ {A B} → (f : A ⇒ B) → Kernel f) where
 
   -- The kernel of a kernel is isomorphic to the zero object.
-  kernel²-zero : ∀ {A B} {f : A ⇒ B} → Kernel.kernel (has-kernels (Kernel.kernel⇒ (has-kernels f))) ≅ zero
-  kernel²-zero {B = B} {f = f} = pullback-up-to-iso kernel-pullback (pullback-mono-mono !-Mono)
+  kernel²-zero : ∀ {A B} {f : A ⇒ B} → Kernel.kernel (has-kernels (Kernel.kernel⇒ (has-kernels f))) ≅ 𝟘
+  kernel²-zero {B = B} {f = f} = pullback-up-to-iso kernel-pullback (pullback-mono-mono (¡-Mono 𝒞 {z = 𝒞-Zero}))
     where
       K : Kernel f
       K = has-kernels f
@@ -122,8 +122,8 @@ module _ (has-kernels : ∀ {A B} → (f : A ⇒ B) → Kernel f) where
       K′ : Kernel K.kernel⇒
       K′ = has-kernels K.kernel⇒
 
-      kernel-pullback : Pullback ! !
-      kernel-pullback = Pullback-resp-≈ (glue-pullback (Kernel⇒Pullback K) (swap (Kernel⇒Pullback K′))) (!-unique (f ∘ !)) refl
+      kernel-pullback : Pullback ¡ ¡ 
+      kernel-pullback = Pullback-resp-≈ (glue-pullback (Kernel⇒Pullback K) (swap (Kernel⇒Pullback K′))) (¡-unique (f ∘ ¡)) refl
 
       pullback-mono-mono : ∀ {A B} {f : A ⇒ B} → Mono f → Pullback f f
       pullback-mono-mono mono = record

src/Categories/Object/Zero.agda

@@ -5,59 +5,56 @@ open import Categories.Category
 -- a zero object is both terminal and initial.
 module Categories.Object.Zero {o ℓ e} (C : Category o ℓ e) where
 
-open import Level using (_⊔_)
+open import Level
 
 open import Categories.Object.Terminal C
 open import Categories.Object.Initial C
 
 open import Categories.Morphism C
+open import Categories.Morphism.Reasoning C
 
 open Category C
 open HomReasoning
 
+record IsZero (Z : Obj) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    isInitial : IsInitial Z
+    isTerminal : IsTerminal Z
+
+  open IsInitial isInitial public
+    renaming
+    ( ! to ¡
+    ; !-unique to ¡-unique
+    ; !-unique₂ to ¡-unique₂
+    )
+  open IsTerminal isTerminal public
+
+  zero⇒ : ∀ {A B : Obj} → A ⇒ B
+  zero⇒ = ¡ ∘ !
+
+  zero-∘ˡ : ∀ {X Y Z} → (f : Y ⇒ Z) → f ∘ zero⇒ {X} ≈ zero⇒
+  zero-∘ˡ f = pullˡ (⟺ (¡-unique (f ∘ ¡)))
+
+  zero-∘ʳ : ∀ {X Y Z} → (f : X ⇒ Y) → zero⇒ {Y} {Z} ∘ f ≈ zero⇒
+  zero-∘ʳ f = pullʳ (⟺ (!-unique (! ∘ f)))
+
 record Zero : Set (o ⊔ ℓ ⊔ e) where
- field
-   zero : Obj
-   !    : ∀ {A} → zero ⇒ A
-   ¡    : ∀ {A} → A ⇒ zero
-
- zero⇒ : ∀ {A B : Obj} → A ⇒ B
- zero⇒ {A} = ! ∘ ¡
-
- field
-   !-unique : ∀ {A} (f : zero ⇒ A) → ! ≈ f
-   ¡-unique : ∀ {A} (f : A ⇒ zero) → ¡ ≈ f
-
- ¡-unique₂ : ∀ {A} (f g : A ⇒ zero) → f ≈ g
- ¡-unique₂ f g = ⟺ (¡-unique f) ○ ¡-unique g
-
- !-unique₂ : ∀ {A} (f g : zero ⇒ A) → f ≈ g
- !-unique₂ f g = ⟺ (!-unique f) ○ !-unique g
-
-
- initial : Initial
- initial = record
-   { ⊥        = zero
-   ; ⊥-is-initial = record
-     { !        = !
-     ; !-unique = !-unique
-     }
-   }
-
- terminal : Terminal
- terminal = record
-   { ⊤        = zero
-   ; ⊤-is-terminal = record
-     { !        = ¡
-     ; !-unique = ¡-unique
-     }
-   }
-
- module initial  = Initial initial
- module terminal = Terminal terminal
-
- !-Mono : ∀ {A} → Mono (! {A})
- !-Mono = from-⊤-is-Mono {t = terminal} !
-
- ¡-Epi : ∀ {A} → Epi (¡ {A})
- ¡-Epi = to-⊥-is-Epi {i = initial} ¡
+  field
+    𝟘 : Obj
+    isZero : IsZero 𝟘
+
+  open IsZero isZero public
+
+  terminal : Terminal
+  terminal = record { ⊤-is-terminal = isTerminal }
+
+  initial : Initial
+  initial = record { ⊥-is-initial = isInitial }
+
+open Zero
+
+¡-Mono : ∀ {A} {z : Zero} → Mono (¡ z {A})
+¡-Mono {z = z} = from-⊤-is-Mono {t = terminal z} (¡ z)
+
+!-Epi : ∀ {A} {z : Zero} → Epi (! z {A})
+!-Epi {z = z} = to-⊥-is-Epi {i = initial z} (! z)