diff options
Diffstat (limited to 'Category/Instance/Cospans.agda')
| -rw-r--r-- | Category/Instance/Cospans.agda | 1 |
1 files changed, 1 insertions, 0 deletions
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₁ |