From 3c62ac510f286f228c9993fe6c37abdcad9e1fb2 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 8 Dec 2025 16:09:19 -0600
Subject: Update category of cospans monoidal structure

---
 Category/Monoidal/Instance/Cospans.agda | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'Category/Monoidal/Instance/Cospans.agda')

diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda
index 228ddea..a1648db 100644
--- a/Category/Monoidal/Instance/Cospans.agda
+++ b/Category/Monoidal/Instance/Cospans.agda
@@ -18,8 +18,9 @@ open import Categories.Category.Monoidal.Core using (Monoidal)
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Properties using ([_]-resp-≅)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
-open import Category.Instance.Cospans 𝒞 using (Cospans; Cospan)
-open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC)
+open import Category.Instance.Cospans 𝒞 using (Cospans)
+open import Category.Diagram.Cospan using (Cospan; cospan)
+open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC)
 open import Category.Monoidal.Instance.Cospans.Lift {o} {ℓ} {e} using (module Square)
 open import Data.Product.Base using (_,_)
 open import Functor.Instance.Cospan.Stack 𝒞 using (⊗)
@@ -61,7 +62,6 @@ CospansMonoidal = record
     ; pentagon = pentagon
     }
   where
-    module ⊗ = Functor ⊗
     module Cospans = Category Cospans
     module Unitorˡ = Square ⊥+--id
     module Unitorʳ = Square -+⊥-id
@@ -83,16 +83,15 @@ CospansMonoidal = record
 CospansBraided : Braided CospansMonoidal
 CospansBraided = record
     { braiding = niHelper record
-        { η = λ { (X , Y) → Braiding.FX≅GX′.from {X , Y} }
-        ; η⁻¹ = λ { (Y , X) → Braiding.FX≅GX′.to {Y , X} }
-        ; commute = λ { {X , Y} {X′ , Y′} (f , g) → Braiding.from (record { f₁ = f₁ f , f₁ g ; f₂ = f₂ f , f₂ g }) }
-        ; iso = λ { (X , Y) → Braiding.FX≅GX′.iso {X , Y} }
+        { η = λ (X , Y) → Braiding.FX≅GX′.from {X , Y}
+        ; η⁻¹ = λ (Y , X) → Braiding.FX≅GX′.to {Y , X}
+        ; commute = λ (cospan f₁ f₂ , cospan g₁ g₂) → Braiding.from (cospan (f₁ , g₁) (f₂ , g₂))
+        ; iso = λ (X , Y) → Braiding.FX≅GX′.iso {X , Y}
         }
     ; hexagon₁ = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym homomorphism ○ sym homomorphism ○ L-resp-≈ hex₁ ○ homomorphism ○ refl⟩∘⟨ homomorphism
     ; hexagon₂ = sym L-resp-⊗ ⟩∘⟨refl ⟩∘⟨ sym L-resp-⊗ ○ sym homomorphism ⟩∘⟨refl ○ sym homomorphism ○ L-resp-≈ hex₂ ○ homomorphism ○ homomorphism ⟩∘⟨refl
     }
   where
-    open Cospan
     module Cospans = Category Cospans
     open Cospans.Equiv
     open Cospans.HomReasoning
-- 
cgit v1.2.3