Poset and various lattice induced categories (#649)

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)

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)

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 _ _)

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

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 _≤_