rename Empty to Zero

This commit also contains a slight refactor of `EmptySet`. There is no
need for this type to depend on the unit.

src/Categories/Category/Instance/EmptySet.agda

@@ -6,11 +6,9 @@ open import Level
 -- Here EmptySet is not given an explicit name, it is an alias for Lift o ⊥
 module Categories.Category.Instance.EmptySet where
 
-open import Data.Unit
-open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality using (refl)
 
 open import Categories.Category.Instance.Sets
 open import Categories.Category.Instance.Setoids
@@ -20,23 +18,25 @@ module _ {o : Level} where
   open Init (Sets o)
 
   EmptySet-⊥ : Initial
-  EmptySet-⊥ = record { ⊥ = Lift o ⊥ ; ⊥-is-initial = record { ! = λ { {A} (lift x) → ⊥-elim x } ; !-unique = λ { f () } } }
+  EmptySet-⊥ .Initial.⊥ = ⊥
+  EmptySet-⊥ .Initial.⊥-is-initial .IsInitial.! ()
 
 module _ {c ℓ : Level} where
   open Init (Setoids c ℓ)
 
   EmptySetoid : Setoid c ℓ
   EmptySetoid = record
-    { Carrier = Lift c ⊥
-    ; _≈_     = λ _ _ → Lift ℓ ⊤
+    { Carrier = ⊥
+    ; _≈_     = λ ()
+    ; isEquivalence = record { refl = λ { {()} } ; sym = λ { {()} }  ; trans = λ { {()} } }
     }
 
   EmptySetoid-⊥ : Initial
   EmptySetoid-⊥ = record
     { ⊥            = EmptySetoid
     ; ⊥-is-initial = record
       { !        = record
-        { to = λ { () }
+        { to = λ ()
         ; cong  = λ { {()} }
         }
       ; !-unique = λ { _ {()} }

src/Categories/Category/Instance/Properties/Setoids/Extensive.agda

@@ -44,9 +44,9 @@ Setoids-Extensive ℓ = record
         { commute = λ { {()}}
         ; universal = λ {C f g} eq → record
            { to = λ z → conflict A B (eq {z})
-           ; cong = λ z → tt
+           ; cong = λ {x} _ → conflict A B (eq {x})
            }
-        ; unique = λ _ _ → tt
+        ; unique = λ {_} {_} {_} {_} {eq} _ _ {x} → conflict A B (eq {x})
         ; p₁∘universal≈h₁ = λ {_ _ _ eq x} → conflict A B (eq {x})
         ; p₂∘universal≈h₂ = λ {_ _ _ eq y} → conflict A B (eq {y})
         }

src/Categories/Category/Instance/Zero.agda

@@ -1,58 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level
+module Categories.Category.Instance.Zero {o ℓ e} where
 
--- ⊥ is Initial
-
-module Categories.Category.Instance.Zero where
-
-open import Data.Empty using (⊥; ⊥-elim)
-open import Function renaming (id to idf)
-
-open import Categories.Category
-open import Categories.Functor
-open import Categories.Category.Instance.Cats
-import Categories.Object.Initial as Init
-
--- Unlike for ⊤ being Terminal, Agda can't deduce these, need to be explicit
-module _ {o ℓ e : Level} where
-  open Init (Cats o ℓ e)
-
-  Zero : Category o ℓ e
-  Zero = record
-    { Obj       = Lift o ⊥
-    ; _⇒_       = λ _ _ → Lift ℓ ⊥
-    ; _≈_       = λ _ _ → Lift e ⊥
-    ; id        = λ { { lift () } }
-    ; _∘_       = λ a _ → a -- left-biased rather than strict
-    ; assoc     = λ { {lift () } }
-    ; sym-assoc = λ { {lift () } }
-    ; identityˡ = λ { {()} }
-    ; identityʳ = λ { {()} }
-    ; identity² = λ { {()} }
-    ; ∘-resp-≈  = λ { () }
-    ; equiv     = record
-      { refl = λ { {()} }
-      ; sym = idf
-      ; trans = λ a _ → a
-      }
-    }
-
-  Zero-⊥ : Initial
-  Zero-⊥ = record
-    { ⊥ = Zero
-    ; ⊥-is-initial = record
-      { ! = record
-        { F₀ = λ { (lift x) → ⊥-elim x }
-        ; F₁ = λ { (lift ()) }
-        ; identity = λ { {lift ()} }
-        ; homomorphism = λ { {lift ()} }
-        ; F-resp-≈ = λ { () }
-        }
-      ; !-unique = λ f → record
-        { F⇒G = record { η = λ { () } ; commute = λ { () } ; sym-commute = λ { () } }
-        ; F⇐G = record { η = λ { () } ; commute = λ { () } ; sym-commute = λ { () } }
-        ; iso = λ { (lift ()) }
-        }
-      }
-    }
+open import Categories.Category.Instance.Zero.Core {o} {ℓ} {e} public
+open import Categories.Category.Instance.Zero.Properties {o} {ℓ} {e} public

src/Categories/Category/Instance/Zero/Core.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Category.Instance.Zero.Core {o ℓ e}  where
+
+open import Categories.Category.Core using (Category)
+open import Data.Empty.Polymorphic using (⊥)
+
+open Category
+
+-- A level-polymorphic empty category
+Zero : Category o ℓ e
+Zero .Obj = ⊥

src/Categories/Category/Instance/Zero/Properties.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Category.Instance.Zero.Properties {o ℓ e} where
+
+open import Data.Empty.Polymorphic using (⊥-elim)
+
+open import Categories.Category using (Category)
+open import Categories.Functor using (Functor)
+open import Categories.Category.Instance.Cats using (Cats)
+open import Categories.Category.Instance.Zero.Core using (Zero)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
+open import Categories.Object.Initial (Cats o ℓ e) using (Initial; IsInitial)
+
+open Initial
+open IsInitial
+open Functor
+
+-- Unlike for ⊤ being Terminal, Agda can't deduce these, need to be explicit
+Zero-⊥ : Initial
+Zero-⊥ .⊥ = Zero
+Zero-⊥ .⊥-is-initial .! .F₀ ()
+Zero-⊥ .⊥-is-initial .!-unique f = niHelper record
+  { η = λ()
+  ; η⁻¹ = λ()
+  ; commute = λ{ {()} }
+  ; iso = λ()
+  }

src/Categories/Diagram/Empty.agda

@@ -6,10 +6,10 @@ open import Categories.Category.Core using (Category)
 
 module Categories.Diagram.Empty {o ℓ e} (C : Category o ℓ e) (o′ ℓ′ e′ : Level) where
 
-open import Categories.Category.Construction.Empty {o′} {ℓ′} {e′} using (Empty)
+open import Categories.Category.Instance.Zero {o′} {ℓ′} {e′} using (Zero)
 open import Categories.Functor.Core using (Functor)
 
 open Functor
 
-empty : Functor Empty C
+empty : Functor Zero C
 empty .F₀ ()

src/Categories/Object/Initial/Colimit.agda

@@ -5,15 +5,15 @@ open import Categories.Category
 module Categories.Object.Initial.Colimit {o ℓ e} (C : Category o ℓ e) where
 
 open import Categories.Category.Construction.Cocones using (Cocone; Cocone⇒)
-open import Categories.Category.Construction.Empty using (Empty)
+open import Categories.Category.Instance.Zero using (Zero)
 open import Categories.Diagram.Colimit using (Colimit)
 open import Categories.Functor.Core using (Functor)
 open import Categories.Object.Initial C
 
 private
   open module C = Category C
 
-module _ {o′ ℓ′ e′} {F : Functor (Empty {o′} {ℓ′} {e′}) C} where
+module _ {o′ ℓ′ e′} {F : Functor (Zero {o′} {ℓ′} {e′}) C} where
   colimit⇒⊥ : Colimit F → Initial
   colimit⇒⊥ L = record
     { ⊥        = coapex
@@ -32,7 +32,7 @@ module _ {o′ ℓ′ e′} {F : Functor (Empty {o′} {ℓ′} {e′}) C} where
     }
     where open Colimit L
 
-module _ {o′ ℓ′ e′} {F : Functor (Empty {o′} {ℓ′} {e′}) C} where
+module _ {o′ ℓ′ e′} {F : Functor (Zero {o′} {ℓ′} {e′}) C} where
 
   ⊥⇒colimit : Initial → Colimit F
   ⊥⇒colimit t = record

src/Categories/Object/Terminal/Limit.agda

@@ -4,7 +4,7 @@ open import Categories.Category
 
 module Categories.Object.Terminal.Limit {o ℓ e} (C : Category o ℓ e) where
 
-open import Categories.Category.Construction.Empty using (Empty)
+open import Categories.Category.Instance.Zero using (Zero)
 open import Categories.Diagram.Limit
 open import Categories.Functor.Core
 open import Categories.Object.Terminal C
@@ -15,7 +15,7 @@ private
   module C = Category C
   open C
 
-module _ {o′ ℓ′ e′} {F : Functor (Empty {o′} {ℓ′} {e′}) C} where
+module _ {o′ ℓ′ e′} {F : Functor (Zero {o′} {ℓ′} {e′}) C} where
   limit⇒⊤ : Limit F → Terminal
   limit⇒⊤ L = record
     { ⊤        = apex
@@ -34,7 +34,7 @@ module _ {o′ ℓ′ e′} {F : Functor (Empty {o′} {ℓ′} {e′}) C} where
     }
     where open Limit L
 
-module _ {o′ ℓ′ e′} {F : Functor (Empty {o′} {ℓ′} {e′}) C} where
+module _ {o′ ℓ′ e′} {F : Functor (Zero {o′} {ℓ′} {e′}) C} where
   ⊤⇒limit : Terminal → Limit F
   ⊤⇒limit t = record
     { terminal = record