Add decorated cospans

6 files changed, 116 insertions, 20 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
diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
new file mode 100644
index 0000000..af40895
--- /dev/null
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+module Category.Cocomplete.Finitely.Bundle where
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+
+
+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
+
+  open FinitelyCocompleteSymmetricMonoidal finCo using (+-monoidal; +-symmetric)
+
+  symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
+  symmetricMonoidalCategory = record
+      { U = U
+      ; monoidal = +-monoidal
+      ; symmetric = +-symmetric
+      }
diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
new file mode 100644
index 0000000..26813eb
--- /dev/null
+++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+
+module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where
+
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+
+
+module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete 𝒞) where
+
+  open FinitelyCocomplete finCo using (cocartesian)
+  open CocartesianMonoidal cocartesian using (+-monoidal) public
+  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) public
diff --git a/Cospan.agda b/Category/Instance/Cospans.agda
index 3c5296d..a3f8fb0 100644
--- a/Cospan.agda
+++ b/Category/Instance/Cospans.agda
@@ -1,11 +1,11 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category using (Category)
-open import Category.Cocomplete.Bundle using (FinitelyCocompleteCategory)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
 open import Function using (flip)
 open import Level using (_⊔_)
 
-module Cospan {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
+module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
 
 open FinitelyCocompleteCategory 𝒞
 
@@ -38,8 +38,8 @@ record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
 
   field
     {N} : Obj
-    f₁    : A ⇒ N
-    f₂    : B ⇒ N
+    f₁  : A ⇒ N
+    f₂  : B ⇒ N
 
 compose : Cospan A B → Cospan B C → Cospan A C
 compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ }
diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
new file mode 100644
index 0000000..fa4d903
--- /dev/null
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Setoids.SymmetricMonoidal {ℓ} where
+
+open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Monoidal.Instance.Setoids
+    using (Setoids-Cartesian; Setoids-Cocartesian)
+    renaming (Setoids-Monoidal to ×-monoidal)
+open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids ℓ ℓ) Setoids-Cartesian
+    using ()
+    renaming (symmetric to ×-symmetric)
+open import Level using (suc)
+open import Categories.Category.Cocartesian (Setoids ℓ ℓ)
+    using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open CocartesianMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-monoidal)
+open CocartesianSymmetricMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-symmetric)
+
+
+Setoids-× : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ
+Setoids-× = record
+    { U = Setoids ℓ ℓ
+    ; monoidal = ×-monoidal
+    ; symmetric = ×-symmetric
+    }
+
+Setoids-+ : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ
+Setoids-+ = record
+    { U = Setoids ℓ ℓ
+    ; monoidal = +-monoidal
+    ; symmetric = +-symmetric
+    }
diff --git a/Cospan/Decorated.agda b/Cospan/Decorated.agda
new file mode 100644
index 0000000..5178435
--- /dev/null
+++ b/Cospan/Decorated.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Categories.Functor.Monoidal.Symmetric using (module Strong)
+open Strong using (SymmetricMonoidalFunctor)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
+
+open FinitelyCocompleteCategory using () renaming (symmetricMonoidalCategory to smc)
+
+module Cospan.Decorated
+    {o ℓ e}
+    (C : FinitelyCocompleteCategory o ℓ e)
+    (F : SymmetricMonoidalFunctor (smc C) (Setoids-× {ℓ}))
+  where
+
+open FinitelyCocompleteCategory C
+
+open import Category.Instance.Cospans C using (Cospan)
+open import Level using (_⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+
+open Setoid using () renaming (Carrier to ∣_∣)
+
+
+record DecoratedCospan (A B : Obj) : Set (o ⊔ ℓ) where
+
+  open SymmetricMonoidalFunctor F using (F₀)
+
+  field
+    cospan : Cospan A B
+
+  open Cospan cospan public
+
+  field
+    decoration : ∣ F₀ N ∣