From e293371f59d1d8d2786cde5ef29182499d560d42 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 11 Jun 2024 11:22:59 -0500
Subject: Begin defining category of cospans

---
 Category/Cocomplete/Bundle.agda | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 Category/Cocomplete/Bundle.agda

(limited to 'Category/Cocomplete')

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
-- 
cgit v1.2.3