diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 16:15:11 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 16:15:11 -0600 |
| commit | 3386254cb6f5fc36c5cb18b7240edde3210a376c (patch) | |
| tree | cfe3eb553afab97c12634e62931f9fa1d378397b /Category/Instance/MonoidalPreorders.agda | |
| parent | 3d7c5574124d3384ff942489feaa093618c309b9 (diff) | |
Add category of symmetric monoidal preorders
Diffstat (limited to 'Category/Instance/MonoidalPreorders.agda')
| -rw-r--r-- | Category/Instance/MonoidalPreorders.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Category/Instance/MonoidalPreorders.agda b/Category/Instance/MonoidalPreorders.agda index 6bdeb3f..6f8ffe0 100644 --- a/Category/Instance/MonoidalPreorders.agda +++ b/Category/Instance/MonoidalPreorders.agda @@ -71,5 +71,5 @@ MonoidalPreorders c ℓ e = categoryHelper record ; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i) } where - open MonoidalMonotone using (F; cong) - open MonoidalPreorder using (U; refl; module Eq) + open MonoidalMonotone using (cong) + open MonoidalPreorder using (refl; module Eq) |