From 164fc3636fc98a54b156d1eaf1dde4ce57ba6930 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 3 Mar 2024 17:23:57 -0800 Subject: [PATCH] Prove that constant functions are monotonic Signed-off-by: Danila Fedorin --- Lattice.agda | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Lattice.agda b/Lattice.agda index 2feb2f5..dbe0ade 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -103,6 +103,17 @@ record IsSemilattice {a} (A : Set a) , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄))) ) +module _ {a b} {A : Set a} {B : Set b} + {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} + {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B} + (lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where + + open IsSemilattice lA using () renaming (_≼_ to _≼₁_) + open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp) + + const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x) + const-Mono x _ = ⊔₂-idemp x + record IsLattice {a} (A : Set a) (_≈_ : A → A → Set a) (_⊔_ : A → A → A)