Add trivial and graph decoration functorsmain

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
+        }
+    }
+