Define Biproducts

src/Categories/Object/Biproduct.agda

@@ -0,0 +1,80 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+-- Biproducts, a-la Karvonen.
+--
+-- This definition has advantages over more traditional ones,
+-- namely that that we don't require either enrichment in CMon/Ab, or Zero Objects.
+--
+-- See https://arxiv.org/abs/1801.06488
+module Categories.Object.Biproduct {o ℓ e} (𝒞 : Category o ℓ e) where
+
+open import Level
+
+open import Categories.Object.Coproduct 𝒞
+open import Categories.Object.Product 𝒞
+
+open import Categories.Morphism 𝒞
+
+open Category 𝒞
+open HomReasoning
+
+private
+  variable
+    A B C D : Obj
+    f g h : A ⇒ B
+
+record IsBiproduct {A B A⊕B : Obj} (π₁ : A⊕B ⇒ A) (π₂ : A⊕B ⇒ B) (i₁ : A ⇒ A⊕B) (i₂ : B ⇒ A⊕B) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    isCoproduct : IsCoproduct i₁ i₂
+    isProduct : IsProduct π₁ π₂
+
+    π₁∘i₁≈id : π₁ ∘ i₁ ≈ id
+    π₂∘i₂≈id : π₂ ∘ i₂ ≈ id
+    permute  : i₁ ∘ π₁ ∘ i₂ ∘ π₂ ≈ i₂ ∘ π₂ ∘ i₁ ∘ π₁
+
+  open IsCoproduct isCoproduct public renaming (unique to []-unique)
+  open IsProduct isProduct public renaming (unique to ⟨⟩-unique)
+
+record Biproduct (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    A⊕B : Obj
+
+    π₁    : A⊕B ⇒ A
+    π₂    : A⊕B ⇒ B
+
+    i₁    : A ⇒ A⊕B
+    i₂    : B ⇒ A⊕B
+
+    isBiproduct : IsBiproduct π₁ π₂ i₁ i₂
+
+  open IsBiproduct isBiproduct public
+
+IsBiproduct⇒Biproduct : {π₁ : C ⇒ A} {π₂ : C ⇒ B} {i₁ : A ⇒ C} {i₂ : B ⇒ C}  → IsBiproduct π₁ π₂ i₁ i₂ → Biproduct A B
+IsBiproduct⇒Biproduct isBiproduct = record
+  { isBiproduct = isBiproduct
+  }
+
+Biproduct⇒IsBiproduct : (b : Biproduct A B) → IsBiproduct (Biproduct.π₁ b) (Biproduct.π₂ b) (Biproduct.i₁ b) (Biproduct.i₂ b)
+Biproduct⇒IsBiproduct biproduct = Biproduct.isBiproduct biproduct
+
+Biproduct⇒Product : Biproduct A B → Product A B
+Biproduct⇒Product b = record
+  { ⟨_,_⟩ = ⟨_,_⟩
+  ; project₁ = project₁
+  ; project₂ = project₂
+  ; unique = ⟨⟩-unique
+  }
+  where
+    open Biproduct b
+
+Biproduct⇒Coproduct : Biproduct A B → Coproduct A B
+Biproduct⇒Coproduct b = record
+  { [_,_] = [_,_]
+  ; inject₁ = inject₁
+  ; inject₂ = inject₂
+  ; unique = []-unique
+  }
+  where
+    open Biproduct b

src/Categories/Object/Coproduct.agda

@@ -43,3 +43,30 @@ record Coproduct (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
   ∘-distribˡ-[] : ∀ {f : A ⇒ C} {g : B ⇒ C} {q : C ⇒ D} → q ∘ [ f , g ] ≈ [ q ∘ f , q ∘ g ]
   ∘-distribˡ-[] = ⟺ $ unique (pullʳ inject₁) (pullʳ inject₂)
 
+record IsCoproduct {A B A+B : Obj} (i₁ : A ⇒ A+B) (i₂ : B ⇒ A+B) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    [_,_] : A ⇒ C → B ⇒ C → A+B ⇒ C
+
+    inject₁ : [ f , g ] ∘ i₁ ≈ f
+    inject₂ : [ f , g ] ∘ i₂ ≈ g
+    unique   : h ∘ i₁ ≈ f → h ∘ i₂ ≈ g → [ f , g ] ≈ h
+
+Coproduct⇒IsCoproduct : (c : Coproduct A B) → IsCoproduct (Coproduct.i₁ c) (Coproduct.i₂ c)
+Coproduct⇒IsCoproduct c = record
+  { [_,_] = [_,_]
+  ; inject₁ = inject₁
+  ; inject₂ = inject₂
+  ; unique = unique
+  }
+  where
+    open Coproduct c
+
+IsCoproduct⇒Coproduct : ∀ {C} {i₁ : A ⇒ C} {i₂ : B ⇒ C} → IsCoproduct i₁ i₂ → Coproduct A B
+IsCoproduct⇒Coproduct c = record
+  { [_,_] = [_,_]
+  ; inject₁ = inject₁
+  ; inject₂ = inject₂
+  ; unique = unique
+  }
+  where
+    open IsCoproduct c