diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-09-19 12:34:28 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-09-19 12:34:28 -0500 |
| commit | 8a832a39547c21a0cde9cd3671f0368cd35c26c0 (patch) | |
| tree | 82710a665db81d84c5e592c586211304a3fa6d2c /Category/Cocomplete/Bundle.agda | |
| parent | dc3b799d6f9cdd4fb0b2b32f323b7128ccc14a80 (diff) | |
Add decorated cospans
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 |