From 8d3d3b53cfab2540ed006e768af1e41ea3d35750 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 3 Feb 2025 10:11:47 -0600 Subject: Add category of finitely-cocomplete categories - Objects are categories with all finite colimits - Morphisms are functors preserving finite colimits (i.e. right exact) --- Category/Instance/One/Properties.agda | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 Category/Instance/One/Properties.agda (limited to 'Category/Instance/One/Properties.agda') diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda new file mode 100644 index 0000000..1452669 --- /dev/null +++ b/Category/Instance/One/Properties.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Category.Instance.One.Properties {o ℓ e : Level} where + +open import Categories.Category.Core using (Category) +open import Categories.Category.Instance.One using () renaming (One to One′) + +One : Category o ℓ e +One = One′ + +open import Categories.Category.Cocartesian One using (Cocartesian) +open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete) +open import Categories.Object.Initial One using (Initial) +open import Categories.Category.Cocartesian One using (BinaryCoproducts) + + +One-Initial : Initial +One-Initial = _ + +One-BinaryCoproducts : BinaryCoproducts +One-BinaryCoproducts = _ + +One-Cocartesian : Cocartesian +One-Cocartesian = record + { initial = One-Initial + ; coproducts = One-BinaryCoproducts + } + +One-FinitelyCocomplete : FinitelyCocomplete +One-FinitelyCocomplete = record + { cocartesian = One-Cocartesian + ; coequalizer = _ + } -- cgit v1.2.3