Begin defining category of cospans

1 files changed, 16 insertions, 0 deletions

diff --git a/Category/Cocomplete/Bundle.agda b/Category/Cocomplete/Bundle.agda
new file mode 100644
index 0000000..3ab3cac
--- /dev/null
+++ b/Category/Cocomplete/Bundle.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --without-K --safe #-}
+module Category.Cocomplete.Bundle where
+
+open import Level
+
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Category.Core using (Category)
+
+
+record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
+  field
+    U     : Category o ℓ e
+    finCo : FinitelyCocomplete U
+
+  open Category U public
+  open FinitelyCocomplete finCo public