From ad3fe42d244d8f19b8b95d20e5f66acd1a1b39b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Fri, 26 Nov 2021 08:40:08 +0100
Subject: [PATCH] Poset and various lattice induced categories (#649)

---
 Cubical/Categories/Instances/DistLattice.agda | 14 ++++++++++
 Cubical/Categories/Instances/Lattice.agda     | 14 ++++++++++
 Cubical/Categories/Instances/Poset.agda       | 28 +++++++++++++++++++
 Cubical/Categories/Instances/Semilattice.agda | 18 ++++++++++++
 Cubical/Relation/Binary/Poset.agda            |  2 +-
 5 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 Cubical/Categories/Instances/DistLattice.agda
 create mode 100644 Cubical/Categories/Instances/Lattice.agda
 create mode 100644 Cubical/Categories/Instances/Poset.agda
 create mode 100644 Cubical/Categories/Instances/Semilattice.agda

diff --git a/Cubical/Categories/Instances/DistLattice.agda b/Cubical/Categories/Instances/DistLattice.agda
new file mode 100644
index 0000000000..b78c38afb5
--- /dev/null
+++ b/Cubical/Categories/Instances/DistLattice.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.DistLattice where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.DistLattice
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Instances.Lattice
+
+open Category
+
+DistLatticeCategory : ∀ {ℓ} (L : DistLattice ℓ) → Category ℓ ℓ
+DistLatticeCategory L = LatticeCategory (DistLattice→Lattice L)
diff --git a/Cubical/Categories/Instances/Lattice.agda b/Cubical/Categories/Instances/Lattice.agda
new file mode 100644
index 0000000000..f254b34f25
--- /dev/null
+++ b/Cubical/Categories/Instances/Lattice.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.Lattice where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.Lattice
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Instances.Semilattice
+
+open Category
+
+LatticeCategory : ∀ {ℓ} (L : Lattice ℓ) → Category ℓ ℓ
+LatticeCategory L = SemilatticeCategory (Lattice→MeetSemilattice L)
diff --git a/Cubical/Categories/Instances/Poset.agda b/Cubical/Categories/Instances/Poset.agda
new file mode 100644
index 0000000000..720326e9b8
--- /dev/null
+++ b/Cubical/Categories/Instances/Poset.agda
@@ -0,0 +1,28 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.Poset where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Poset
+
+open import Cubical.Categories.Category
+
+open Category
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ (P : Poset ℓ ℓ') where
+
+  open PosetStr (snd P)
+
+  PosetCategory : Category ℓ ℓ'
+  ob PosetCategory           = fst P
+  Hom[_,_] PosetCategory     = _≤_
+  id PosetCategory           = is-refl _
+  _⋆_ PosetCategory          = is-trans _ _ _
+  ⋆IdL PosetCategory _       = is-prop-valued _ _ _ _
+  ⋆IdR PosetCategory _       = is-prop-valued _ _ _ _
+  ⋆Assoc PosetCategory _ _ _ = is-prop-valued _ _ _ _
+  isSetHom PosetCategory     = isProp→isSet (is-prop-valued _ _)
diff --git a/Cubical/Categories/Instances/Semilattice.agda b/Cubical/Categories/Instances/Semilattice.agda
new file mode 100644
index 0000000000..86cdd6418a
--- /dev/null
+++ b/Cubical/Categories/Instances/Semilattice.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.Semilattice where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.Semilattice
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Instances.Poset
+
+open Category
+
+module _ {ℓ} (L : Semilattice ℓ) where
+
+  open MeetSemilattice L
+
+  SemilatticeCategory : Category ℓ ℓ
+  SemilatticeCategory = PosetCategory IndPoset
diff --git a/Cubical/Relation/Binary/Poset.agda b/Cubical/Relation/Binary/Poset.agda
index c2ac279196..57d7560484 100644
--- a/Cubical/Relation/Binary/Poset.agda
+++ b/Cubical/Relation/Binary/Poset.agda
@@ -49,7 +49,7 @@ record PosetStr (ℓ' : Level) (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')
   constructor posetstr
 
   field
-    _≤_         : A → A → Type ℓ'
+    _≤_     : A → A → Type ℓ'
     isPoset : IsPoset _≤_
 
   infixl 7 _≤_