From dbe587eb007d512735f58887ce7c22d951db02ca Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Wed, 23 Jul 2025 19:35:50 +0530
Subject: [PATCH] Define the category of posets

---
 Cubical/Categories/Instances/Posets.agda      | 25 +++++++++++++++++++
 .../Relation/Binary/Order/Poset/Mappings.agda |  4 +--
 2 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 Cubical/Categories/Instances/Posets.agda

diff --git a/Cubical/Categories/Instances/Posets.agda b/Cubical/Categories/Instances/Posets.agda
new file mode 100644
index 0000000000..ce483065d5
--- /dev/null
+++ b/Cubical/Categories/Instances/Posets.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.Posets where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function as Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Poset.Mappings
+
+open import Cubical.Categories.Category
+
+open Category hiding (_∘_)
+
+PosetsCategory : ∀ ℓ ℓ' → Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-max ℓ ℓ')
+PosetsCategory ℓ ℓ' .ob = Poset ℓ ℓ'
+PosetsCategory ℓ ℓ' .Hom[_,_] P Q = Σ[ f ∈ (⟨ P ⟩ → ⟨ Q ⟩) ] IsIsotone (str P) f (str Q)
+PosetsCategory ℓ ℓ' .id = idfun _ , isisotone λ _ _ → idfun _
+PosetsCategory ℓ ℓ' ._⋆_ (f , fMon) (g , gMon) = g ∘ f , IsIsotone-∘ _ _ _ _ _ fMon gMon
+PosetsCategory ℓ ℓ' .⋆IdL _ = refl
+PosetsCategory ℓ ℓ' .⋆IdR _ = refl
+PosetsCategory ℓ ℓ' .⋆Assoc _ _ _ = refl
+PosetsCategory ℓ ℓ' .isSetHom {x = P} {y = Q} = isSetΣSndProp (isSet→ Q.is-set) λ _ → isPropIsIsotone _ _ _
+  where module Q = PosetStr (str Q)
diff --git a/Cubical/Relation/Binary/Order/Poset/Mappings.agda b/Cubical/Relation/Binary/Order/Poset/Mappings.agda
index 161f366072..e159ce1377 100644
--- a/Cubical/Relation/Binary/Order/Poset/Mappings.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Mappings.agda
@@ -38,6 +38,7 @@ record IsIsotone {A : Type ℓ₀} {B : Type ℓ₁}
   (M : PosetStr ℓ₀' A) (f : A → B) (N : PosetStr ℓ₁' B)
   : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
   where
+  constructor isisotone
   -- Shorter qualified names
   private
     module M = PosetStr M
@@ -67,8 +68,7 @@ record IsAntitone {A : Type ℓ₀} {B : Type ℓ₁}
   (M : PosetStr ℓ₀' A) (f : A → B) (N : PosetStr ℓ₁' B)
   : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
   where
-  constructor
-    isantitone
+  constructor isantitone
   -- Shorter qualified names
   private
     module M = PosetStr M