From 8a832a39547c21a0cde9cd3671f0368cd35c26c0 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 19 Sep 2024 12:34:28 -0500
Subject: Add decorated cospans

---
 Category/Cocomplete/Bundle.agda | 16 ----------------
 1 file changed, 16 deletions(-)
 delete mode 100644 Category/Cocomplete/Bundle.agda

(limited to 'Category/Cocomplete/Bundle.agda')

diff --git a/Category/Cocomplete/Bundle.agda b/Category/Cocomplete/Bundle.agda
deleted file mode 100644
index 3ab3cac..0000000
--- a/Category/Cocomplete/Bundle.agda
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# 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