From 3d7c5574124d3384ff942489feaa093618c309b9 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 4 Jan 2026 15:53:23 -0600 Subject: Add category of monoidal preorders --- Category/Instance/Preorders.agda | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'Category/Instance/Preorders.agda') diff --git a/Category/Instance/Preorders.agda b/Category/Instance/Preorders.agda index 7dde3af..6d69eda 100644 --- a/Category/Instance/Preorders.agda +++ b/Category/Instance/Preorders.agda @@ -24,27 +24,27 @@ module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : Preorder c₁ ℓ₁ e ≗-isEquivalence : IsEquivalence _≗_ ≗-isEquivalence = record - { refl = Eq.refl B - ; sym = λ f≈g → Eq.sym B f≈g - ; trans = λ f≈g g≈h → Eq.trans B f≈g g≈h - } + { refl = Eq.refl B + ; sym = λ f≈g → Eq.sym B f≈g + ; trans = λ f≈g g≈h → Eq.trans B f≈g g≈h + } module ≗ = IsEquivalence ≗-isEquivalence -- The category of preorders and monotone maps -Preorders : ∀ c ℓ e → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ) +Preorders : (c ℓ e : Level) → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ) Preorders c ℓ e = record - { Obj = Preorder c ℓ e - ; _⇒_ = PreorderHomomorphism - ; _≈_ = _≗_ - ; id = λ {A} → Id.preorderHomomorphism A - ; _∘_ = λ f g → Comp.preorderHomomorphism g f - ; assoc = λ {_ _ _ D} → Eq.refl D - ; sym-assoc = λ {_ _ _ D} → Eq.refl D - ; identityˡ = λ {_ B} → Eq.refl B - ; identityʳ = λ {_ B} → Eq.refl B - ; identity² = λ {A} → Eq.refl A - ; equiv = ≗-isEquivalence - ; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i) - } + { Obj = Preorder c ℓ e + ; _⇒_ = PreorderHomomorphism + ; _≈_ = _≗_ + ; id = λ {A} → Id.preorderHomomorphism A + ; _∘_ = λ f g → Comp.preorderHomomorphism g f + ; assoc = λ {_ _ _ D} → Eq.refl D + ; sym-assoc = λ {_ _ _ D} → Eq.refl D + ; identityˡ = λ {_ B} → Eq.refl B + ; identityʳ = λ {_ B} → Eq.refl B + ; identity² = λ {A} → Eq.refl A + ; equiv = ≗-isEquivalence + ; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i) + } -- cgit v1.2.3