DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add definitions about monotonicity to Lattice

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-01-05 19:36:42 -08:00
parent ca375976b7
commit 236c92a5ef
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Lattice.agda
View File

@ -21,6 +21,18 @@ module _ {a b} {A : Set a} {B : Set b}
Monotonic : (A → B) → Set (a ⊔ℓ b) Monotonic : (A → B) → Set (a ⊔ℓ b)
Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂ 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) record IsSemilattice {a} (A : Set a)
(_≈_ : A → A → Set a) (_≈_ : A → A → Set a)
(_⊔_ : A → A → A) : Set a where (_⊔_ : A → A → A) : Set a where