diff options
Diffstat (limited to 'Category/Instance/Nat/FinitelyCocomplete.agda')
| -rw-r--r-- | Category/Instance/Nat/FinitelyCocomplete.agda | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/Category/Instance/Nat/FinitelyCocomplete.agda b/Category/Instance/Nat/FinitelyCocomplete.agda new file mode 100644 index 0000000..d5a9ec0 --- /dev/null +++ b/Category/Instance/Nat/FinitelyCocomplete.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Instance.Nat.FinitelyCocomplete where + +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian) +open import Level using (0ℓ) +open import Nat.Properties using (Coeq) + +Nat-FinitelyCocomplete : FinitelyCocompleteCategory 0ℓ 0ℓ 0ℓ +Nat-FinitelyCocomplete = record + { U = Nat + ; finCo = record + { cocartesian = Nat-Cocartesian + ; coequalizer = Coeq + } + } + |