From 7093fb4fa137b63ae7f2b8a00269ef63da9d70ee Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Fri, 17 Jul 2026 17:16:37 -0700
Subject: Add categories with all binary biproducts

---
 Morphism/Zero.agda | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 Morphism/Zero.agda

(limited to 'Morphism')

diff --git a/Morphism/Zero.agda b/Morphism/Zero.agda
new file mode 100644
index 0000000..01e0953
--- /dev/null
+++ b/Morphism/Zero.agda
@@ -0,0 +1,13 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Level using (Level; _⊔_)
+
+module Morphism.Zero {o ℓ e : Level} (𝒞 : Category o ℓ e) where
+
+open Category 𝒞
+
+record IsZero⇒ {A B : Obj} (z : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    constant : {C : Obj} (f g : C ⇒ A) → z ∘ f ≈ z ∘ g
+    coconstant : {C : Obj} (f g : B ⇒ C) → f ∘ z ≈ g ∘ z
-- 
cgit v1.2.3