Update category of cospans

10 files changed, 275 insertions, 246 deletions

diff --git a/Category/Diagram/Cospan.agda b/Category/Diagram/Cospan.agda
new file mode 100644
index 0000000..b988651
--- /dev/null
+++ b/Category/Diagram/Cospan.agda
@@ -0,0 +1,117 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Level using (Level; _⊔_)
+
+module Category.Diagram.Cospan {o ℓ e : Level} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
+
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Relation.Binary using (IsEquivalence)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+
+open 𝒞 hiding (i₁; i₂; _≈_)
+open ⇒-Reasoning U using (switch-fromtoˡ; glueTrianglesˡ)
+open Morphism U using (_≅_; module ≅)
+
+record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
+
+  constructor cospan
+
+  field
+    {N} : Obj
+    f₁  : A ⇒ N
+    f₂  : B ⇒ N
+
+private
+  variable
+    A B C D : Obj
+
+record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
+
+  module C = Cospan C
+  module D = Cospan D
+
+  field
+    ≅N : C.N ≅ D.N
+
+  open _≅_ ≅N public
+  module ≅N = _≅_ ≅N
+
+  field
+    from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
+    from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
+
+infix 4 _≈_
+
+private
+  variable
+    f g h : Cospan A B
+
+≈-refl : f ≈ f
+≈-refl {f = cospan f₁ f₂} = record
+    { ≅N = ≅.refl
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
+    }
+  where abstract
+    from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁
+    from∘f₁≈f₁ = identityˡ
+    from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂
+    from∘f₂≈f₂ = identityˡ
+
+≈-sym : f ≈ g → g ≈ f
+≈-sym f≈g = record
+    { ≅N = ≅.sym ≅N
+    ; from∘f₁≈f₁ = a
+    ; from∘f₂≈f₂ = b
+    }
+  where abstract
+    open _≈_ f≈g
+    a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁
+    a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁)
+    b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂
+    b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂)
+
+≈-trans : f ≈ g → g ≈ h → f ≈ h
+≈-trans f≈g g≈h = record
+    { ≅N = ≅.trans f≈g.≅N g≈h.≅N
+    ; from∘f₁≈f₁ = a
+    ; from∘f₂≈f₂ = b
+    }
+  where abstract
+    module f≈g = _≈_ f≈g
+    module g≈h = _≈_ g≈h
+    a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁
+    a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁
+    b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂
+    b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂
+
+≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
+≈-equiv = record
+    { refl = ≈-refl
+    ; sym = ≈-sym
+    ; trans = ≈-trans
+    }
+
+compose : Cospan A B → Cospan B C → Cospan A C
+compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
+  where
+    open pushout g h
+
+identity : Cospan A A
+identity = cospan id id
+
+compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
+compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
+  where
+    module P₁ = pushout f₂ g₁
+    module P₂ = pushout g₂ h₁
+    module P₃ = pushout P₁.i₂ P₂.i₁
+
+_⊗_ :  Cospan A B → Cospan C D → Cospan (A + C) (B + D)
+_⊗_ (cospan f₁ f₂) (cospan g₁ g₂) = cospan (f₁ +₁ g₁) (f₂ +₁ g₂)
+
+infixr 10 _⊗_
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index ae6d359..d17a58d 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -13,12 +13,10 @@ open Category U hiding (_≈_)
 
 open import Categories.Diagram.Pushout U using (Pushout)
 open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso)
-open import Relation.Binary using (IsEquivalence)
 open import Categories.Morphism U using (_≅_; module ≅)
 open import Categories.Morphism.Reasoning U
   using
     ( switch-fromtoˡ
-    ; glueTrianglesˡ
     ; pullˡ ; pullʳ
     ; cancelˡ
     )
@@ -30,99 +28,16 @@ open import Category.Diagram.Pushout U 
     ; extend-i₁-iso ; extend-i₂-iso
     )
 
-record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
-
-  constructor cospan
-
-  field
-    {N} : Obj
-    f₁  : A ⇒ N
-    f₂  : B ⇒ N
+open import Category.Diagram.Cospan 𝒞 using (Cospan; compose; compose-3; identity; _≈_; cospan; ≈-trans; ≈-sym; ≈-equiv)
 
 private
   variable
     A B C D : Obj
 
-compose : Cospan A B → Cospan B C → Cospan A C
-compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
-  where
-    open pushout g h
-
-identity : Cospan A A
-identity = cospan id id
-
-compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
-compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
-  where
-    module P₁ = pushout f₂ g₁
-    module P₂ = pushout g₂ h₁
-    module P₃ = pushout P₁.i₂ P₂.i₁
-
-record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
-
-  module C = Cospan C
-  module D = Cospan D
-
-  field
-    ≅N : C.N ≅ D.N
-
-  open _≅_ ≅N public
-  module ≅N = _≅_ ≅N
-
-  field
-    from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
-    from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
-
 private
   variable
     f g h : Cospan A B
 
-≈-refl : f ≈ f
-≈-refl {f = cospan f₁ f₂} = record
-    { ≅N = ≅.refl
-    ; from∘f₁≈f₁ = from∘f₁≈f₁
-    ; from∘f₂≈f₂ = from∘f₂≈f₂
-    }
-  where abstract
-    from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁
-    from∘f₁≈f₁ = identityˡ
-    from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂
-    from∘f₂≈f₂ = identityˡ
-
-≈-sym : f ≈ g → g ≈ f
-≈-sym f≈g = record
-    { ≅N = ≅.sym ≅N
-    ; from∘f₁≈f₁ = a
-    ; from∘f₂≈f₂ = b
-    }
-  where abstract
-    open _≈_ f≈g
-    a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁
-    a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁)
-    b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂
-    b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂)
-
-≈-trans : f ≈ g → g ≈ h → f ≈ h
-≈-trans f≈g g≈h = record
-    { ≅N = ≅.trans f≈g.≅N g≈h.≅N
-    ; from∘f₁≈f₁ = a
-    ; from∘f₂≈f₂ = b
-    }
-  where abstract
-    module f≈g = _≈_ f≈g
-    module g≈h = _≈_ g≈h
-    a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁
-    a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁
-    b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂
-    b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂
-
-≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
-≈-equiv = record
-    { refl = ≈-refl
-    ; sym = ≈-sym
-    ; trans = ≈-trans
-    }
-
 compose-idˡ : compose f identity ≈ f
 compose-idˡ {f = cospan {N} f₁ f₂} = record
     { ≅N = ≅P
diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda
index 7e63f81..b527265 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -20,6 +20,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟
 
 import Categories.Category.Monoidal.Utilities as ⊗-Util
 import Category.Instance.Cospans 𝒞 as Cospans
+import Category.Diagram.Cospan 𝒞 as Cospan
 
 open import Categories.Category using (Category; _[_∘_])
 open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
@@ -52,7 +53,7 @@ private
 
 compose : DecoratedCospan A B → DecoratedCospan B C → DecoratedCospan A C
 compose c₁ c₂ = record
-    { cospan = Cospans.compose C₁.cospan C₂.cospan
+    { cospan = Cospan.compose C₁.cospan C₂.cospan
     ; decoration = F₁ [ i₁ , i₂ ] ∘ φ ∘ s⊗t
     }
   where
@@ -69,7 +70,7 @@ compose c₁ c₂ = record
 
 identity : DecoratedCospan A A
 identity = record
-    { cospan = Cospans.identity
+    { cospan = Cospan.identity
     ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ]
     }
 
@@ -80,9 +81,9 @@ record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where
     module C₂ = DecoratedCospan C₂
 
   field
-    cospans-≈ : C₁.cospan Cospans.≈ C₂.cospan
+    cospans-≈ : C₁.cospan Cospan.≈ C₂.cospan
 
-  open Cospans._≈_ cospans-≈ public
+  open Cospan._≈_ cospans-≈ public
   open Morphism 𝒟.U using (_≅_)
 
   field
@@ -107,13 +108,13 @@ module _ where
 
     ≈-refl : f ≈ f
     ≈-refl = record
-        { cospans-≈ = Cospans.≈-refl
+        { cospans-≈ = Cospan.≈-refl
         ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ
         }
 
     ≈-sym : f ≈ g → g ≈ f
     ≈-sym f≈g = record
-        { cospans-≈ = Cospans.≈-sym cospans-≈
+        { cospans-≈ = Cospan.≈-sym cospans-≈
         ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco)
         }
       where
@@ -121,7 +122,7 @@ module _ where
 
     ≈-trans : f ≈ g → g ≈ h → f ≈ h
     ≈-trans f≈g g≈h = record
-        { cospans-≈ = Cospans.≈-trans f≈g.cospans-≈ g≈h.cospans-≈
+        { cospans-≈ = Cospan.≈-trans f≈g.cospans-≈ g≈h.cospans-≈
         ; same-deco =
               homomorphism ⟩∘⟨refl ○
               glueTrianglesˡ 𝒟.U g≈h.same-deco f≈g.same-deco
@@ -613,7 +614,7 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re
     module C₂ = DecoratedCospan c₂
     module C₂′ = DecoratedCospan c₂′
     ≅C₂∘C₁ = Cospans.compose-equiv ≅C₂.cospans-≈ ≅C₁.cospans-≈
-    module ≅C₂∘C₁ = Cospans._≈_ ≅C₂∘C₁
+    module ≅C₂∘C₁ = Cospan._≈_ ≅C₂∘C₁
     P = 𝒞.pushout C₁.f₂ C₂.f₁
     P′ = 𝒞.pushout C₁′.f₂ C₂′.f₁
     module P = Pushout P
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda
index 2766df2..9bee58e 100644
--- a/Category/Instance/FinitelyCocompletes.agda
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -1,29 +1,31 @@
 {-# OPTIONS --without-K --safe #-}
-open import Level using (Level)
+
+open import Level using (Level; suc; _⊔_)
+
 module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where
 
+import Category.Instance.One.Properties as OneProps
+
 open import Categories.Category using (_[_,_])
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Helper using (categoryHelper)
-open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
 open import Categories.Category.Core using (Category)
+open import Categories.Category.Helper using (categoryHelper)
 open import Categories.Category.Instance.Cats using (Cats)
 open import Categories.Category.Instance.One using (One; One-⊤)
+open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
 open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat)
 open import Categories.Diagram.Coequalizer using (IsCoequalizer)
 open import Categories.Functor using (Functor) renaming (id to idF)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
 open import Categories.Object.Coproduct using (IsCoproduct)
 open import Categories.Object.Initial using (IsInitial)
 open import Categories.Object.Product.Core using (Product)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
 open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×)
-open import Category.Instance.One.Properties using (One-FinitelyCocomplete)
 open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′)
-open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
 open import Function.Base using (id; flip)
-open import Level using (Level; suc; _⊔_)
+open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
 
 FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
 FinitelyCocompletes = categoryHelper record
@@ -48,7 +50,7 @@ FinitelyCocompletes = categoryHelper record
 One-FCC : FinitelyCocompleteCategory o ℓ e
 One-FCC = record
     { U = One
-    ; finCo = One-FinitelyCocomplete
+    ; finCo = OneProps.finitelyCocomplete
     }
 
 _×_
@@ -62,7 +64,6 @@ _×_ 𝒞 𝒟 = record
   where
     module 𝒞 = FinitelyCocompleteCategory 𝒞
     module 𝒟 = FinitelyCocompleteCategory 𝒟
-{-# INJECTIVE_FOR_INFERENCE _×_ #-}
 
 module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
 
diff --git a/Cospan/Decorated.agda b/Cospan/Decorated.agda
index 498a869..b5d6f07 100644
--- a/Cospan/Decorated.agda
+++ b/Cospan/Decorated.agda
@@ -17,7 +17,7 @@ module Cospan.Decorated
 module C = FinitelyCocompleteCategory C
 module D = SymmetricMonoidalCategory D
 
-open import Category.Instance.Cospans C using (Cospan)
+open import Category.Diagram.Cospan C using (Cospan)
 open import Level using (_⊔_)
 
 
diff --git a/Functor/Instance/Cospan/Embed.agda b/Functor/Instance/Cospan/Embed.agda
index 77f0361..6dbc04a 100644
--- a/Functor/Instance/Cospan/Embed.agda
+++ b/Functor/Instance/Cospan/Embed.agda
@@ -1,4 +1,5 @@
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
 
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
 
@@ -14,9 +15,10 @@ open import Categories.Category using (_[_,_]; _[_∘_]; _[_≈_])
 open import Categories.Category.Core using (Category)
 open import Categories.Functor.Core using (Functor)
 open import Category.Instance.Cospans 𝒞 using (Cospans)
+open import Category.Diagram.Cospan 𝒞 using (cospan)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
-open import Functor.Instance.Cospan.Stack using (⊗)
+open import Functor.Instance.Cospan.Stack 𝒞 using (⊗)
 
 module 𝒞 = FinitelyCocompleteCategory 𝒞
 module Cospans = Category Cospans
@@ -28,24 +30,26 @@ open Morphism U using (module ≅; _≅_)
 open PushoutProperties U using (up-to-iso)
 open Pushout′ U using (pushout-id-g; pushout-f-id)
 
-L₁ : {A B : 𝒞.Obj} → U [ A , B ] → Cospans [ A , B ]
-L₁ f = record
-    { f₁ = f
-    ; f₂ = 𝒞.id
-    }
+private
+  variable
+    A B C : 𝒞.Obj
+    W X Y Z : 𝒞.Obj
+
+L₁ : U [ A , B ] → Cospans [ A , B ]
+L₁ f = cospan f 𝒞.id
 
-L-identity : {A : 𝒞.Obj} → L₁ 𝒞.id ≈ Cospans.id {A}
+L-identity : L₁ 𝒞.id ≈ Cospans.id {A}
 L-identity = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = 𝒞.identity²
-    ; from∘f₂≈f₂′ = 𝒞.identity²
+    ; from∘f₁≈f₁ = 𝒞.identity²
+    ; from∘f₂≈f₂ = 𝒞.identity²
     }
 
-L-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ]
+L-homomorphism : {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ]
 L-homomorphism {X} {Y} {Z} {f} {g} = record
     { ≅N = up-to-iso P′ P
-    ; from∘f₁≈f₁′ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute})
-    ; from∘f₂≈f₂′ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ
+    ; from∘f₁≈f₁ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute})
+    ; from∘f₂≈f₂ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ
     }
   where
     open ⇒-Reasoning U
@@ -57,11 +61,11 @@ L-homomorphism {X} {Y} {Z} {f} {g} = record
     module P = Pushout P
     module P′ = Pushout P′
 
-L-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ]
+L-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ]
 L-resp-≈ {A} {B} {f} {g} f≈g = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = 𝒞.identityˡ ○ f≈g
-    ; from∘f₂≈f₂′ = 𝒞.identity²
+    ; from∘f₁≈f₁ = 𝒞.identityˡ ○ f≈g
+    ; from∘f₂≈f₂ = 𝒞.identity²
     }
   where
     open 𝒞.HomReasoning
@@ -75,24 +79,21 @@ L = record
     ; F-resp-≈ = L-resp-≈
     }
 
-R₁ : {A B : 𝒞.Obj} → U [ B , A ] → Cospans [ A , B ]
-R₁ g = record
-    { f₁ = 𝒞.id
-    ; f₂ = g
-    }
+R₁ : U [ B , A ] → Cospans [ A , B ]
+R₁ g = cospan 𝒞.id g
 
-R-identity : {A : 𝒞.Obj} → R₁ 𝒞.id ≈ Cospans.id {A}
+R-identity : R₁ 𝒞.id ≈ Cospans.id {A}
 R-identity = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = 𝒞.identity²
-    ; from∘f₂≈f₂′ = 𝒞.identity²
+    ; from∘f₁≈f₁ = 𝒞.identity²
+    ; from∘f₂≈f₂ = 𝒞.identity²
     }
 
-R-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ]
-R-homomorphism {X} {Y} {Z} {f} {g} = record
+R-homomorphism : {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ]
+R-homomorphism {f} {g} = record
     { ≅N = up-to-iso P′ P
-    ; from∘f₁≈f₁′ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ
-    ; from∘f₂≈f₂′ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute})
+    ; from∘f₁≈f₁ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ
+    ; from∘f₂≈f₂ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute})
     }
   where
     open ⇒-Reasoning U
@@ -104,11 +105,11 @@ R-homomorphism {X} {Y} {Z} {f} {g} = record
     module P = Pushout P
     module P′ = Pushout P′
 
-R-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ]
-R-resp-≈ {A} {B} {f} {g} f≈g = record
+R-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ]
+R-resp-≈ {f} {g} f≈g = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = 𝒞.identity²
-    ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ f≈g
+    ; from∘f₁≈f₁ = 𝒞.identity²
+    ; from∘f₂≈f₂ = 𝒞.identityˡ ○ f≈g
     }
   where
     open 𝒞.HomReasoning
@@ -122,17 +123,11 @@ R = record
     ; F-resp-≈ = R-resp-≈
     }
 
-B₁ : {A B C : 𝒞.Obj} → U [ A , C ] → U [ B , C ] → Cospans [ A , B ]
-B₁ f g = record
-    { f₁ = f
-    ; f₂ = g
-    }
-
-B∘L : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ B₁ g h ∘ L₁ f ] ≈ B₁ (U [ g ∘ f ]) h
-B∘L {W} {X} {Y} {Z} {f} {g} {h} = record
+B∘L : {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ cospan g h ∘ L₁ f ] ≈ cospan (U [ g ∘ f ]) h
+B∘L {f} {g} {h} = record
     { ≅N = up-to-iso P P′
-    ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute})
-    ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ
+    ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute})
+    ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ
     }
   where
     open ⇒-Reasoning U
@@ -144,11 +139,11 @@ B∘L {W} {X} {Y} {Z} {f} {g} {h} = record
     module P = Pushout P
     module P′ = Pushout P′
 
-R∘B : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ B₁ f g ] ≈ B₁ f (U [ g ∘ h ])
-R∘B {W} {X} {Y} {Z} {f} {g} {h} = record
+R∘B : {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ cospan f g ] ≈ cospan f (U [ g ∘ h ])
+R∘B {f} {g} {h} = record
     { ≅N = up-to-iso P P′
-    ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ
-    ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute})
+    ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ
+    ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute})
     }
   where
     open ⇒-Reasoning U
@@ -164,20 +159,18 @@ module _ where
 
   open _≅_
 
-  ≅-L-R : ∀ {X Y : 𝒞.Obj} (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y)
-  ≅-L-R {X} {Y} X≅Y = record
+  ≅-L-R : (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y)
+  ≅-L-R X≅Y = record
       { ≅N = X≅Y
-      ; from∘f₁≈f₁′ = isoʳ X≅Y
-      ; from∘f₂≈f₂′ = 𝒞.identityʳ
+      ; from∘f₁≈f₁ = isoʳ X≅Y
+      ; from∘f₂≈f₂ = 𝒞.identityʳ
       }
 
-module ⊗ = Functor (⊗ 𝒞)
-
-L-resp-⊗ : {X Y X′ Y′ : 𝒞.Obj} {a : U [ X , X′ ]} {b : U [ Y , Y′ ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b)
-L-resp-⊗ {X} {Y} {X′} {Y′} {a} {b} = record
+L-resp-⊗ : {a : U [ W , X ]} {b : U [ Y , Z ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b)
+L-resp-⊗ {a} {b} = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = 𝒞.identityˡ
-    ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ)
+    ; from∘f₁≈f₁ = 𝒞.identityˡ
+    ; from∘f₂≈f₂ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ)
     }
   where
     open 𝒞.HomReasoning
diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda
index 03cca1f..b72219b 100644
--- a/Functor/Instance/Cospan/Stack.agda
+++ b/Functor/Instance/Cospan/Stack.agda
@@ -9,9 +9,11 @@ import Categories.Diagram.Pushout.Properties as PushoutProperties
 import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning as ⇒-Reasoning
 
-open import Categories.Category.Core using (Category)
+open import Categories.Category using (Category)
+open import Categories.Functor using (Functor)
 open import Categories.Functor.Bifunctor using (Bifunctor)
-open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same; id-Cospan; compose)
+open import Category.Instance.Cospans 𝒞 using (Cospans)
+open import Category.Diagram.Cospan 𝒞 as Cospan using (Cospan; identity; compose; _⊗_)
 open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using () renaming (_×_ to _×′_)
 open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC)
 open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂)
@@ -32,27 +34,19 @@ open DiagramPushout U×U using () renaming (Pushout to Pushout′)
 
 open import Categories.Category.Monoidal.Utilities monoidal using (_⊗ᵢ_)
 
-together :  {A A′ B B′ : Obj} → Cospan A B → Cospan A′ B′ → Cospan (A + A′) (B + B′)
-together A⇒B A⇒B′ = record
-    { f₁ = f₁ A⇒B +₁ f₁ A⇒B′
-    ; f₂ = f₂ A⇒B +₁ f₂ A⇒B′
-    }
-  where
-    open Cospan
-
-id⊗id≈id : {A B : Obj} → Same (together (id-Cospan {A}) (id-Cospan {B})) (id-Cospan {A + B})
+id⊗id≈id : {A B : Obj} → identity {A} ⊗ identity {B} Cospan.≈ identity {A + B}
 id⊗id≈id {A} {B} = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = from∘f≈f′
-    ; from∘f₂≈f₂′ = from∘f≈f′
+    ; from∘f₁≈f₁ = from∘f≈f
+    ; from∘f₂≈f₂ = from∘f≈f
     }
   where
     open Morphism U using (module ≅)
     open HomReasoning
     open 𝒞 using (+-η; []-cong₂)
     open coproduct {A} {B} using (i₁; i₂)
-    from∘f≈f′ : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id
-    from∘f≈f′ = begin
+    from∘f≈f : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id
+    from∘f≈f = begin
         id ∘ [ i₁ ∘ id , i₂ ∘ id ]  ≈⟨ identityˡ ⟩
         [ i₁ ∘ id , i₂ ∘ id ]       ≈⟨ []-cong₂ identityʳ identityʳ ⟩
         [ i₁ , i₂ ]                 ≈⟨ +-η ⟩
@@ -64,14 +58,14 @@ homomorphism
     → (B⇒C : Cospan B C)
     → (A⇒B′ : Cospan A′ B′)
     → (B⇒C′ : Cospan B′ C′)
-    → Same (together (compose A⇒B B⇒C) (compose A⇒B′ B⇒C′)) (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′) )
+    → compose A⇒B B⇒C ⊗ compose A⇒B′ B⇒C′ Cospan.≈ compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′)
 homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record
     { ≅N = ≅N
-    ; from∘f₁≈f₁′ = from∘f₁≈f₁′
-    ; from∘f₂≈f₂′ = from∘f₂≈f₂′
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
-    open Cospan
+    open Cospan.Cospan
     open Pushout
     open HomReasoning
     open ⇒-Reasoning U
@@ -89,56 +83,62 @@ homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record
     P₃′ = IsPushout⇒Pushout (-+-.F-resp-pushout P₁×P₂.isPushout)
     ≅N : Q P₃′ ≅ Q P₃
     ≅N = up-to-iso P₃′ P₃
-    from∘f₁≈f₁′ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′))
-    from∘f₁≈f₁′ = begin
+    from∘f₁≈f₁ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′))
+    from∘f₁≈f₁ = begin
         from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′))  ≈⟨ Equiv.refl ⟩
         from ≅N ∘ ((i₁ P₁ ∘ f₁ A⇒B) +₁ (i₁ P₂ ∘ f₁ A⇒B′))           ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨
         from ≅N ∘ (i₁ P₁ +₁ i₁ P₂) ∘ (f₁ A⇒B +₁ f₁ A⇒B′)            ≈⟨ Equiv.refl ⟩
-        from ≅N ∘ i₁ P₃′ ∘ f₁ (together A⇒B A⇒B′)                   ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩
-        i₁ P₃ ∘ f₁ (together A⇒B A⇒B′)                              ∎
-    from∘f₂≈f₂′ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′))
-    from∘f₂≈f₂′ = begin
+        from ≅N ∘ i₁ P₃′ ∘ f₁ (A⇒B ⊗ A⇒B′)                          ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩
+        i₁ P₃ ∘ f₁ (A⇒B ⊗ A⇒B′)                                     ∎
+    from∘f₂≈f₂ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′))
+    from∘f₂≈f₂ = begin
         from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′))  ≈⟨ Equiv.refl ⟩
         from ≅N ∘ ((i₂ P₁ ∘ f₂ B⇒C) +₁ (i₂ P₂ ∘ f₂ B⇒C′))           ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨
         from ≅N ∘ (i₂ P₁ +₁ i₂ P₂) ∘ (f₂ B⇒C +₁ f₂ B⇒C′)            ≈⟨ Equiv.refl ⟩
-        from ≅N ∘ i₂ P₃′ ∘ f₂ (together B⇒C B⇒C′)                   ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩
-        i₂ P₃ ∘ f₂ (together B⇒C B⇒C′)                              ∎
+        from ≅N ∘ i₂ P₃′ ∘ f₂ (B⇒C ⊗ B⇒C′)                          ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩
+        i₂ P₃ ∘ f₂ (B⇒C ⊗ B⇒C′)                                     ∎
 
 ⊗-resp-≈
     : {A A′ B B′ : Obj}
       {f f′ : Cospan A B}
       {g g′ : Cospan A′ B′}
-    → Same f f′
-    → Same g g′
-    → Same (together f g) (together f′ g′)
+    → f Cospan.≈ f′
+    → g Cospan.≈ g′
+    → f ⊗ g Cospan.≈ f′ ⊗ g′
 ⊗-resp-≈ {_} {_} {_} {_} {f} {f′} {g} {g′} ≈f ≈g = record
     { ≅N = ≈f.≅N ⊗ᵢ ≈g.≅N
-    ; from∘f₁≈f₁′ = from∘f₁≈f₁′
-    ; from∘f₂≈f₂′ = from∘f₂≈f₂′
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open 𝒞 using (-+-)
-    module ≈f = Same ≈f
-    module ≈g = Same ≈g
+    module ≈f = Cospan._≈_ ≈f
+    module ≈g = Cospan._≈_ ≈g
     open HomReasoning
-    open Cospan
+    open Cospan.Cospan
     open 𝒞 using (+₁-cong₂; +₁∘+₁)
-    from∘f₁≈f₁′ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′
-    from∘f₁≈f₁′ = begin 
+    from∘f₁≈f₁ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′
+    from∘f₁≈f₁ = begin 
         (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈⟨ +₁∘+₁ ⟩
-        (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g)  ≈⟨ +₁-cong₂ (≈f.from∘f₁≈f₁′) (≈g.from∘f₁≈f₁′) ⟩
+        (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g)  ≈⟨ +₁-cong₂ ≈f.from∘f₁≈f₁ ≈g.from∘f₁≈f₁ ⟩
         f₁ f′ +₁ f₁ g′                        ∎
-    from∘f₂≈f₂′ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′
-    from∘f₂≈f₂′ = begin 
+    from∘f₂≈f₂ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′
+    from∘f₂≈f₂ = begin 
         (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈⟨ +₁∘+₁ ⟩
-        (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g)  ≈⟨ +₁-cong₂ (≈f.from∘f₂≈f₂′) (≈g.from∘f₂≈f₂′) ⟩
+        (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g)  ≈⟨ +₁-cong₂ ≈f.from∘f₂≈f₂ ≈g.from∘f₂≈f₂ ⟩
         f₂ f′ +₁ f₂ g′                        ∎
 
+private
+  ⊗′ : Bifunctor Cospans Cospans Cospans
+  ⊗′ = record
+      { F₀ = λ (A , A′) → A + A′
+      ; F₁ = λ (f , g) → f ⊗ g
+      ; identity = λ { {x , y} → id⊗id≈id {x} {y} }
+      ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ }
+      ; F-resp-≈ = λ (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g
+      }
+
 ⊗ : Bifunctor Cospans Cospans Cospans
-⊗ = record
-    { F₀ = λ { (A , A′) → A + A′ }
-    ; F₁ = λ { (f , g) → together f g }
-    ; identity = λ { {x , y} → id⊗id≈id {x} {y} }
-    ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ }
-    ; F-resp-≈ = λ { (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g }
-    }
+⊗ = ⊗′
+
+module ⊗ = Functor ⊗
diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda
index 30cec87..fedddba 100644
--- a/Functor/Instance/Decorate.agda
+++ b/Functor/Instance/Decorate.agda
@@ -1,4 +1,5 @@
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
 
 open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
 open import Categories.Functor.Monoidal.Symmetric using (module Lax)
@@ -19,6 +20,7 @@ module Functor.Instance.Decorate
 import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
 import Categories.Diagram.Pushout as DiagramPushout
 import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Category.Diagram.Cospan 𝒞 as Cospan
 
 open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
 open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
@@ -27,10 +29,10 @@ open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Categories.Functor.Core using (Functor)
 open import Categories.Functor.Properties using ([_]-resp-≅)
 open import Function.Base using () renaming (id to idf)
-open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same)
+open import Category.Instance.Cospans 𝒞 using (Cospans)
 open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans)
-open import Functor.Instance.Cospan.Stack using (⊗)
-open import Functor.Instance.DecoratedCospan.Stack using () renaming (⊗ to ⊗′)
+open import Functor.Instance.Cospan.Stack 𝒞 using (module ⊗)
+open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using () renaming (module ⊗ to ⊗′)
 
 module 𝒞 = FinitelyCocompleteCategory 𝒞
 module 𝒟 = SymmetricMonoidalCategory 𝒟
@@ -67,14 +69,14 @@ identity = record
     open ⇒-Reasoning 𝒟.U
 
 homomorphism : DecoratedCospans [ decorate (Cospans [ g ∘ f ]) ≈ DecoratedCospans [ decorate g ∘ decorate f ] ]
-homomorphism {B} {C} {g} {A} {f} = record
+homomorphism {g} {f} = record
     { cospans-≈ = Cospans.Equiv.refl
     ; same-deco = same-deco
     }
   where
 
-    open Cospan f using (N; f₂)
-    open Cospan g using () renaming (N to M; f₁ to g₁)
+    open Cospan.Cospan f using (N; f₂)
+    open Cospan.Cospan g using () renaming (N to M; f₁ to g₁)
 
     open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-)
     open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
@@ -99,7 +101,7 @@ homomorphism {B} {C} {g} {A} {f} = record
         F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩
         F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐                  ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨
         F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐            ≈⟨ pushˡ F.homomorphism ⟩
-        F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐           ≈⟨ push-center (sym F.homomorphism) ⟩
+        F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐           ≈⟨ push-center F.homomorphism ⟩
         F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨
         F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩
         F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐             ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , ¡)) ⟨
@@ -126,19 +128,15 @@ Decorate = record
     ; F-resp-≈ = F-resp-≈
     }
 
-module ⊗ = Functor (⊗ 𝒞)
-module ⊗′ = Functor (⊗′ 𝒞 F)
-open 𝒞 using (_+₁_)
-
 Decorate-resp-⊗ : DecoratedCospans [ decorate (⊗.₁ (f , g)) ≈ ⊗′.₁ (decorate f , decorate g) ]
-Decorate-resp-⊗ {f = f} {g = g} = record
-    { cospans-≈ = Cospans.Equiv.refl
+Decorate-resp-⊗ {f} {g} = record
+    { cospans-≈ = Cospan.≈-refl
     ; same-deco = same-deco
     }
   where
 
-    open Cospan f using (N)
-    open Cospan g using () renaming (N to M)
+    open Cospan.Cospan f using (N)
+    open Cospan.Cospan g using () renaming (N to M)
 
     open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-)
     open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
@@ -165,4 +163,3 @@ Decorate-resp-⊗ {f = f} {g = g} = record
         F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐             ≈⟨ extendʳ (φ-commute (¡ , ¡)) ⟨
         φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐            ≈⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩
         φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐         ∎
-
diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda
index 4595a8f..77b16fa 100644
--- a/Functor/Instance/DecoratedCospan/Embed.agda
+++ b/Functor/Instance/DecoratedCospan/Embed.agda
@@ -19,6 +19,7 @@ import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
 import Categories.Diagram.Pushout.Properties as PushoutProperties
 import Categories.Morphism.Reasoning as ⇒-Reasoning
 import Category.Diagram.Pushout as Pushout′
+import Category.Diagram.Cospan as Cospan
 import Functor.Instance.Cospan.Embed 𝒞 as Embed
 
 open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
@@ -34,9 +35,9 @@ import Categories.Morphism as Morphism
 open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
 open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Categories.Functor using (Functor; _∘F_)
-open import Data.Product.Base using (_,_)
-open import Function.Base using () renaming (id to idf)
-open import Functor.Instance.DecoratedCospan.Stack using (⊗)
+open import Data.Product using (_,_)
+open import Function using () renaming (id to idf)
+open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗)
 
 module 𝒞 = FinitelyCocompleteCategory 𝒞
 module 𝒟 = SymmetricMonoidalCategory 𝒟
@@ -62,7 +63,7 @@ R = Decorate ∘F Embed.R
 
 B₁ : 𝒞.U [ A , C ] → 𝒞.U [ B , C ] → 𝒟.U [ 𝒟.unit , F.F₀ C ] → DecoratedCospans [ A , B ]
 B₁ f g s = record
-    { cospan = Embed.B₁ f g
+    { cospan = Cospan.cospan f g
     ; decoration = s
     }
 
@@ -265,7 +266,6 @@ module _ where
     where
       module Decorate = Functor Decorate
 
-  module ⊗ = Functor (⊗ 𝒞 F)
   open 𝒞 using (_+₁_)
 
   L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ]
diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda
index 5c3c232..381ee06 100644
--- a/Functor/Instance/DecoratedCospan/Stack.agda
+++ b/Functor/Instance/DecoratedCospan/Stack.agda
@@ -19,6 +19,7 @@ import Categories.Diagram.Pushout as DiagramPushout
 import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning as ⇒-Reasoning
 import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+
 import Functor.Instance.Cospan.Stack 𝒞 as Stack
 
 open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
@@ -26,13 +27,16 @@ open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Monoidal.Utilities using (module Shorthands)
 open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
 open import Categories.Category.Monoidal.Braided.Properties using (braiding-coherence-inv)
+open import Categories.Functor using (Functor)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Properties using ([_]-resp-≅)
 open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
 open import Categories.Object.Initial using (Initial)
 open import Categories.Object.Duality using (Coproduct⇒coProduct)
-open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; Same to Same′)
-open import Category.Instance.Cospans 𝒞 using (Same; compose)
+open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; _≈_ to _≈_′)
+
+import Category.Diagram.Cospan 𝒞 as Cospan
+
 open import Cospan.Decorated 𝒞 F using (DecoratedCospan)
 open import Data.Product.Base using (_,_)
 
@@ -52,10 +56,9 @@ private
   variable
     A A′ B B′ C C′ : Obj
 
-
 together : Cospans [ A , B ] → Cospans [ A′ , B′ ] → Cospans [ A + A′ , B + B′ ]
 together A⇒B A⇒B′ = record
-    { cospan = Stack.together A⇒B.cospan A⇒B′.cospan
+    { cospan = A⇒B.cospan Cospan.⊗ A⇒B′.cospan
     ; decoration = ⊗-homo.η (A⇒B.N , A⇒B′.N) ∘ A⇒B.decoration ⊗₁ A⇒B′.decoration ∘ unitorʳ.to
     }
   where
@@ -108,9 +111,9 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
 
     module _ where
       open DecoratedCospan using (cospan)
-      cospans-≈ : Same (Stack.together _ _) (compose (Stack.together _ _) (Stack.together _ _))
+      cospans-≈ : _ Cospan.⊗ _ Cospan.≈ Cospan.compose (_ Cospan.⊗ _) (_ Cospan.⊗ _)
       cospans-≈ = Stack.homomorphism (f .cospan) (g .cospan) (f′ .cospan) (g′ .cospan)
-      open Same cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public
+      open Cospan._≈_ cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public
 
     module DecorationNames where
       open DecoratedCospan f using (N) renaming (decoration to s) public
@@ -185,7 +188,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
         ≅∘[]+[]≈μ∘μ+μ = begin
             ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′                                                  ≈⟨ refl⟩∘⟨ μ∘+ ⟩⊗⟨ μ∘+ ⟩
             ≅ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′)                                              ≈⟨ refl⟩∘⟨ introˡ +-η ⟩
-            ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′)                               ≈⟨ push-center (sym μ∘+) ⟩
+            ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′)                               ≈⟨ push-center μ∘+ ⟩
             ≅ ∘ μ ∘ (ι₁ +₁ ι₂) ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′)                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ⊗-distrib-over-∘ ⟩
             ≅ ∘ μ ∘ (ι₁ ∘ μ ∘ i₁ +₁ i₂) +₁ (ι₂ ∘ μ ∘ i₁′ +₁ i₂′)                                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ μ-natural) ⟩⊗⟨ (extendʳ μ-natural) ⟩
             ≅ ∘ μ ∘ (μ ∘ ι₁ +₁ ι₁ ∘ i₁ +₁ i₂) +₁ (μ ∘ ι₂ +₁ ι₂ ∘ i₁′ +₁ i₂′)                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩⊗⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩
@@ -221,7 +224,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
            α⇐ ∘ w +₁ (x +₁ _ ∘ α⇒ ∘ _) ∘ α⇒                                 ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ assoc-commute-from ⟩∘⟨refl ⟨
            α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y) +₁ z ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒          ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pushˡ split₁ʳ) ⟩∘⟨refl ⟨
            α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y ∘ +-swap) +₁ z ∘ α⇐) ∘ α⇒                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ σ.⇒.sym-commute _ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩
-           α⇐ ∘ w +₁ (α⇒ ∘ (+-swap ∘ y +₁ x) +₁ z ∘ α⇐) ∘ α⇒                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center (sym split₁ˡ) ⟩∘⟨refl ⟩
+           α⇐ ∘ w +₁ (α⇒ ∘ (+-swap ∘ y +₁ x) +₁ z ∘ α⇐) ∘ α⇒                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center split₁ˡ ⟩∘⟨refl ⟩
            α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ (y +₁ x) +₁ z ∘ α⇐) ∘ α⇒          ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ assoc-commute-to) ⟩∘⟨refl ⟨
            α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐ ∘ y +₁ (x +₁ z))   ∘ α⇒        ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc²εβ ⟩∘⟨refl ⟩
            α⇐ ∘ w +₁ ((α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ y +₁ (x +₁ z)) ∘ α⇒        ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
@@ -231,7 +234,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
 
         μ∘μ+μ∘swap-inner : {X : Obj} → μ {X} ∘ μ +₁ μ ∘ swap-inner ≈ μ ∘ μ +₁ μ {X}
         μ∘μ+μ∘swap-inner = begin
-          μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒                           ≈⟨ push-center (sym serialize₁₂) ⟩
+          μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒                           ≈⟨ push-center serialize₁₂ ⟩
           μ ∘ μ +₁ id ∘ id +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
           μ ∘ μ +₁ id ∘ (id +₁ id) +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-to ⟨
           μ ∘ μ +₁ id ∘ α⇐ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒        ≈⟨ pullˡ μ-assoc ⟩
@@ -243,7 +246,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
           μ ∘ id +₁ (μ ∘ μ +₁ id ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒                                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pull-center (sym split₁ˡ) ⟩∘⟨refl ⟩
           μ ∘ id +₁ (μ ∘ (μ ∘ +-swap) +₁ id ∘ α⇐) ∘ α⇒                                    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ μ∘σ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩
           μ ∘ id +₁ (μ ∘ μ +₁ id ∘ α⇐) ∘ α⇒                                               ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (sym-assoc ○ flip-iso associator (μ-assoc ○ sym-assoc))  ⟩∘⟨refl ⟩
-          μ ∘ id +₁ (μ ∘ id +₁ μ) ∘ α⇒                                                    ≈⟨ push-center (sym split₂ʳ) ⟩
+          μ ∘ id +₁ (μ ∘ id +₁ μ) ∘ α⇒                                                    ≈⟨ push-center split₂ʳ ⟩
           μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ) ∘ α⇒                                              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟨
           μ ∘ id +₁ μ ∘ α⇒ ∘ (id +₁ id) +₁ μ                                              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl  ⟩
           μ ∘ id +₁ μ ∘ α⇒ ∘ id +₁ μ                                                      ≈⟨ refl⟩∘⟨ sym-assoc ⟩
@@ -370,13 +373,13 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
     }
   where
 
-    open Same′ using (cospans-≈)
+    open _≈_′ using (cospans-≈)
 
     module SameNames where
-      open Same′ ≈f using () renaming (same-deco to ≅∘s≈t) public
-      open Same′ ≈g using () renaming (same-deco to ≅∘s≈t′) public
-      open Same (≈f .cospans-≈) using (module ≅N) public
-      open Same (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public
+      open _≈_′ ≈f using () renaming (same-deco to ≅∘s≈t) public
+      open _≈_′ ≈g using () renaming (same-deco to ≅∘s≈t′) public
+      open Cospan._≈_ (≈f .cospans-≈) using (module ≅N) public
+      open Cospan._≈_ (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public
 
     open SameNames
 
@@ -417,9 +420,11 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
 
 ⊗ : Bifunctor Cospans Cospans Cospans
 ⊗ = record
-    { F₀ = λ { (A , A′) → A + A′ }
-    ; F₁ = λ { (f , g) → together f g }
+    { F₀ = λ (A , A′) → A + A′
+    ; F₁ = λ (f , g) → together f g
     ; identity = λ { {x , y} → id⊗id≈id {x} {y} }
     ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ }
-    ; F-resp-≈ = λ { (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g }
+    ; F-resp-≈ = λ (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g
     }
+
+module ⊗ = Functor ⊗