From 89598e5a738170648393c3c111c95318ce39263a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sun, 29 Sep 2024 10:21:09 -0500
Subject: Prove associativity for decorated cospan composition

---
 Category/Instance/Cospans.agda | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index a3f8fb0..ccefcf5 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -70,6 +70,7 @@ record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where
     ≅N : C.N ≅ C′.N
 
   open _≅_ ≅N public
+  module ≅N = _≅_ ≅N
 
   field
     from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁
-- 
cgit v1.2.3