Merge pull request #457 from agda/indexed-coproduct

Add indexed coproducts

Author: JacquesCarette

src/Categories/Object/Coproduct/Indexed.agda

@@ -0,0 +1,37 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+module Categories.Object.Coproduct.Indexed {o ℓ e} (C : Category o ℓ e) where
+
+open import Level
+
+open import Categories.Morphism.Reasoning.Core C
+
+open Category C
+open Equiv
+
+record IndexedCoproductOf {i} {I : Set i} (P : I → Obj) : Set (i ⊔ o ⊔ e ⊔ ℓ) where
+  field
+    X : Obj
+
+    ι : ∀ i → P i ⇒ X
+    [_] : ∀ {Y} → (∀ i → P i ⇒ Y) → X ⇒ Y
+
+    commute : ∀ {Y} (f : ∀ i → P i ⇒ Y) → ∀ i → [ f ] ∘ ι i ≈ f i
+    unique : ∀ {Y} (h : X ⇒ Y) (f : ∀ i → P i ⇒ Y) → (∀ i → h ∘ ι i ≈ f i) → [ f ] ≈ h
+
+  η : ∀ {Y} (h : X ⇒ Y) → [ (λ i → h ∘ ι i) ] ≈ h
+  η h = unique _ _ λ _ → refl
+
+  ∘[] : ∀ {Y Z} (f : ∀ i → P i ⇒ Y) (g : Y ⇒ Z) → g ∘ [ f ] ≈ [ (λ i → g ∘ f i) ]
+  ∘[] f g = sym (unique _ _ λ i → pullʳ (commute _ _))
+
+  []-cong : ∀ {Y} (f g : ∀ i → P i ⇒ Y) → (∀ i → f i ≈ g i) → [ f ] ≈ [ g ]
+  []-cong f g eq = unique _ _ λ i → trans (commute _ _) (sym (eq i))
+
+  unique′ : ∀ {Y} (h h′ : X ⇒ Y) → (∀ i → h′ ∘ ι i ≈ h ∘ ι i) → h′ ≈ h
+  unique′ h h′ f = trans (sym (unique _ _ f)) (η _)
+
+AllCoproductsOf : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
+AllCoproductsOf i = ∀ {I : Set i} (P : I → Obj) → IndexedCoproductOf P

src/Categories/Object/Duality.agda

@@ -15,6 +15,8 @@ open import Categories.Object.Terminal op
 open import Categories.Object.Initial C
 open import Categories.Object.Product op
 open import Categories.Object.Coproduct C
+open import Categories.Object.Product.Indexed op
+open import Categories.Object.Coproduct.Indexed C
 
 open import Categories.Object.Zero
 
@@ -80,6 +82,26 @@ coProduct⇒Coproduct A×B = record
   where
   module A×B = Product A×B
 
+IndexedCoproductOf⇒coIndexedProductOf : ∀ {i} {I : Set i} {P : I → Obj} → IndexedCoproductOf P → IndexedProductOf P
+IndexedCoproductOf⇒coIndexedProductOf ΣP = record
+  { X = ΣP.X
+  ; π = ΣP.ι
+  ; ⟨_⟩ = ΣP.[_]
+  ; commute = ΣP.commute
+  ; unique = ΣP.unique
+  }
+  where module ΣP = IndexedCoproductOf ΣP
+
+coIndexedProductOf⇒IndexedCoproductOf : ∀ {i} {I : Set i} {P : I → Obj} → IndexedProductOf P → IndexedCoproductOf P
+coIndexedProductOf⇒IndexedCoproductOf ΠP = record
+  { X = ΠP.X
+  ; ι = ΠP.π
+  ; [_] = ΠP.⟨_⟩
+  ; commute = ΠP.commute
+  ; unique = ΠP.unique
+  }
+  where module ΠP = IndexedProductOf ΠP
+
 -- Zero objects are autodual
 IsZero⇒coIsZero : IsZero C Z → IsZero op Z
 IsZero⇒coIsZero is-zero = record