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

Prove that constant functions are monotonic

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-03 17:23:57 -08:00
parent c932210d37
commit 164fc3636f
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Lattice.agda
View File

@ -103,6 +103,17 @@ record IsSemilattice {a} (A : Set a)
, λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈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) record IsLattice {a} (A : Set a)
(_≈_ : A → A → Set a) (_≈_ : A → A → Set a)
(_⊔_ : A → A → A) (_⊔_ : A → A → A)