aboutsummaryrefslogtreecommitdiff
path: root/Category/Instance/Preorders.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Category/Instance/Preorders.agda')
-rw-r--r--Category/Instance/Preorders.agda2
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