diff --git a/src/Categories/Category/Construction/Empty.agda b/src/Categories/Category/Construction/Empty.agda
deleted file mode 100644
index 88aa2d8c8..000000000
--- a/src/Categories/Category/Construction/Empty.agda
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Categories.Category.Construction.Empty {o ℓ e}  where
-
-open import Level
-open import Categories.Category.Core
-open import Data.Empty.Polymorphic
-
-open Category
-
--- A level-polymorphic empty category
-Empty : Category o ℓ e
-Empty .Obj = ⊥
diff --git a/src/Categories/Category/Instance/EmptySet.agda b/src/Categories/Category/Instance/EmptySet.agda
index 3ce361023..b9292df36 100644
--- a/src/Categories/Category/Instance/EmptySet.agda
+++ b/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,15 +18,17 @@ 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
@@ -36,7 +36,7 @@ module _ {c ℓ : Level} where
     { ⊥            = EmptySetoid
     ; ⊥-is-initial = record
       { !        = record
-        { to = λ { () }
+        { to = λ ()
         ; cong  = λ { {()} }
         }
       ; !-unique = λ { _ {()} }
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda
index c2618ece3..b4f21707c 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda
+++ b/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})
         }
diff --git a/src/Categories/Category/Instance/Zero.agda b/src/Categories/Category/Instance/Zero.agda
index 0d754b6a4..839e1450e 100644
--- a/src/Categories/Category/Instance/Zero.agda
+++ b/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
diff --git a/src/Categories/Category/Instance/Zero/Core.agda b/src/Categories/Category/Instance/Zero/Core.agda
new file mode 100644
index 000000000..10ebb6d70
--- /dev/null
+++ b/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 = ⊥
diff --git a/src/Categories/Category/Instance/Zero/Properties.agda b/src/Categories/Category/Instance/Zero/Properties.agda
new file mode 100644
index 000000000..5873df3a2
--- /dev/null
+++ b/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 = λ()
+  }
diff --git a/src/Categories/Diagram/Empty.agda b/src/Categories/Diagram/Empty.agda
index 568512043..d51ddcf60 100644
--- a/src/Categories/Diagram/Empty.agda
+++ b/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₀ ()
diff --git a/src/Categories/Object/Initial/Colimit.agda b/src/Categories/Object/Initial/Colimit.agda
index ec9e91923..6678459fb 100644
--- a/src/Categories/Object/Initial/Colimit.agda
+++ b/src/Categories/Object/Initial/Colimit.agda
@@ -5,7 +5,7 @@ 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
@@ -13,7 +13,7 @@ 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
diff --git a/src/Categories/Object/Terminal/Limit.agda b/src/Categories/Object/Terminal/Limit.agda
index 7932a3f9e..d3336bd47 100644
--- a/src/Categories/Object/Terminal/Limit.agda
+++ b/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