From 8ec259bb32b4339b27560f5ea13afa81b9b8febc Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 7 Jan 2026 10:12:13 -0600 Subject: Differentiate lax and strong monoidal monotones --- Category/Instance/Preorders.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Category/Instance/Preorders.agda') 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 -- cgit v1.2.3