From 236c92a5ef525744c8fcafd4f2cd6ec193cf32de Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 5 Jan 2025 19:36:42 -0800 Subject: [PATCH] Add definitions about monotonicity to Lattice Signed-off-by: Danila Fedorin --- Lattice.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Lattice.agda b/Lattice.agda index d8a75ce..2fe2660 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -21,6 +21,18 @@ module _ {a b} {A : Set a} {B : Set b} Monotonic : (A → B) → Set (a ⊔ℓ b) Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂ + Monotonicˡ : ∀ {c} {C : Set c} → (A → C → B) → Set (a ⊔ℓ b ⊔ℓ c) + Monotonicˡ f = ∀ c → Monotonic (λ a → f a c) + + Monotonicʳ : ∀ {c} {C : Set c} → (C → A → B) → Set (a ⊔ℓ b ⊔ℓ c) + Monotonicʳ f = ∀ a → Monotonic (f a) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} + (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) (_≼₃_ : C → C → Set c) where + + Monotonic₂ : (A → B → C) → Set (a ⊔ℓ b ⊔ℓ c) + Monotonic₂ f = Monotonicˡ _≼₁_ _≼₃_ f × Monotonicʳ _≼₂_ _≼₃_ f + record IsSemilattice {a} (A : Set a) (_≈_ : A → A → Set a) (_⊔_ : A → A → A) : Set a where