diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-09-29 10:21:09 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-09-29 10:21:09 -0500 |
| commit | 89598e5a738170648393c3c111c95318ce39263a (patch) | |
| tree | 69020f7a4f002345bb81a4fff7ef83aa0f15d2c6 /Category/Instance/Cospans.agda | |
| parent | 517c1bd04877885720f7998d71f2062d4a93467a (diff) | |
Prove associativity for decorated cospan composition
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₁ |