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

Prove that the identity function is monotonic

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

9
Lattice.agda
View File

@ -103,6 +103,15 @@ 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} {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} module _ {a b} {A : Set a} {B : Set b}
{_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}
{_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B} {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}