diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 10:12:13 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 10:12:13 -0600 |
| commit | 8ec259bb32b4339b27560f5ea13afa81b9b8febc (patch) | |
| tree | f8b860c07c3da42f7ad078413700c347adbfd9d5 /Category/Instance/Preorders.agda | |
| parent | aecb9a5862a9082909c902307974e7ca85463bb9 (diff) | |
Differentiate lax and strong monoidal monotones
Diffstat (limited to 'Category/Instance/Preorders.agda')
| -rw-r--r-- | Category/Instance/Preorders.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Category/Instance/Preorders.agda b/Category/Instance/Preorders.agda index 6d69eda..1a663ac 100644 --- a/Category/Instance/Preorders.agda +++ b/Category/Instance/Preorders.agda @@ -31,7 +31,7 @@ module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : Preorder c₁ ℓ₁ e module ≗ = IsEquivalence ≗-isEquivalence --- The category of preorders and monotone maps +-- The category of preorders and preorder homomorphisms Preorders : (c ℓ e : Level) → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ) Preorders c ℓ e = record |