diff options
Diffstat (limited to 'Category/Cocomplete/Bundle.agda')
| -rw-r--r-- | Category/Cocomplete/Bundle.agda | 16 |
1 files changed, 0 insertions, 16 deletions
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 |