Update category of cospans

2 files changed, 96 insertions, 103 deletions

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 ⊗