From fa0282ff6f15af5acb188bae2b492b175a0b8213 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 6 Mar 2024 00:35:06 -0800 Subject: [PATCH] Prove that the identity function is monotonic Signed-off-by: Danila Fedorin --- Lattice.agda | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Lattice.agda b/Lattice.agda index dbe0ade..ae7035f 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -103,6 +103,15 @@ record IsSemilattice {a} (A : Set a) , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄))) ) +module _ {a} {A : Set a} + {_≈_ : A → A → Set a} {_⊔_ : A → A → A} + (lA : IsSemilattice A _≈_ _⊔_) where + + open IsSemilattice lA using (_≼_) + + id-Mono : Monotonic _≼_ _≼_ (λ x → x) + id-Mono a₁≼a₂ = 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}