From 69670cde145b18f5aa2a685f0dff8076e75542da Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 5 Nov 2024 22:00:06 -0600
Subject: Add trivial and graph decoration functors

---
 Category/Instance/Nat/FinitelyCocomplete.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 Category/Instance/Nat/FinitelyCocomplete.agda

(limited to 'Category/Instance/Nat/FinitelyCocomplete.agda')

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
+        }
+    }
+
-- 
cgit v1.2.3