From cb2efa506d9ecec48aad72deb10acb6ffba45970 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 8 Dec 2025 15:30:53 -0600
Subject: Update category of cospans

---
 Functor/Instance/Decorate.agda | 29 +++++++++++++----------------
 1 file changed, 13 insertions(+), 16 deletions(-)

(limited to 'Functor/Instance/Decorate.agda')

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₁ ¡ ∘ ε) ∘ ρ⇐         ∎
-
-- 
cgit v1.2.3