Add category of finitely-cocomplete categories

- Objects are categories with all finite colimits
- Morphisms are functors preserving finite colimits (i.e. right exact)

1 files changed, 14 insertions, 5 deletions

diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
index af40895..74f434f 100644
--- a/Category/Cocomplete/Finitely/Bundle.agda
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -1,12 +1,12 @@
 {-# OPTIONS --without-K --safe #-}
 module Category.Cocomplete.Finitely.Bundle where
 
-open import Level
+open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
 open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-
+open import Level using (_⊔_; suc)
 
 record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
 
@@ -17,11 +17,20 @@ record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
   open Category U public
   open FinitelyCocomplete finCo public
 
-  open FinitelyCocompleteSymmetricMonoidal finCo using (+-monoidal; +-symmetric)
+  open FinitelyCocompleteSymmetricMonoidal finCo
+    using ()
+    renaming (+-monoidal to monoidal; +-symmetric to symmetric)
+    public
 
   symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
   symmetricMonoidalCategory = record
       { U = U
-      ; monoidal = +-monoidal
-      ; symmetric = +-symmetric
+      ; monoidal = monoidal
+      ; symmetric = symmetric
+      }
+
+  cocartesianCategory : CocartesianCategory o ℓ e
+  cocartesianCategory = record
+      { U = U
+      ; cocartesian = cocartesian
       }