From 27eeead3502f723fc42d61de76332e95b3ecdfdf Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 4 Apr 2023 21:08:31 -0700
Subject: [PATCH] Add typeclasses for (semi)lattices and order

---
 Lattice.agda | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 Lattice.agda

diff --git a/Lattice.agda b/Lattice.agda
new file mode 100644
index 0000000..8012ac3
--- /dev/null
+++ b/Lattice.agda
@@ -0,0 +1,39 @@
+module Lattice where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
+open import Data.Nat using (ℕ; _≤_)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym)
+open import Agda.Primitive using (lsuc)
+
+record Preorder {a} (A : Set a) : Set (lsuc a) where
+    field
+        _≼_ : A → A → Set a
+
+        ≼-refl : Reflexive (_≼_)
+        ≼-trans : Transitive (_≼_)
+        ≼-antisym : Antisymmetric (_≡_) (_≼_)
+
+record Semilattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        _⊔_ : A → A → A
+
+        ⊔-assoc : (x : A) → (y : A) → (z : A) → x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z
+        ⊔-comm : (x : A) → (y : A) → x ⊔ y ≡ y ⊔ x
+        ⊔-idemp : (x : A) → x ⊔ x ≡ x
+
+record Lattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        joinSemilattice : Semilattice A
+        meetSemilattice : Semilattice A
+
+    _⊔_ = Semilattice._⊔_ joinSemilattice
+    _⊓_ = Semilattice._⊔_ meetSemilattice
+
+    field
+        absorb-⊔-⊓ : (x : A) → (y : A) → x ⊔ (x ⊓ y) ≡ x
+        absorb-⊓-⊔ : (x : A) → (y : A) → x ⊓ (x ⊔ y) ≡ x
+
+instance
+    NatPreorder : Preorder ℕ
+    NatPreorder = record { _≼_ = _≤_; ≼-refl = ≤-refl; ≼-trans = ≤-trans; ≼-antisym = ≤-antisym }