From e2bcc89d5509a36ea48253ded9333b30d63298c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Thu, 21 Dec 2023 17:16:11 +0100
Subject: [PATCH] Fix Definition of Instance/Poset.v
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fix a couple of problems in the definition of Poset Category, amounting
to the following changes:

* C should be a Type of the objects (not: a Category)
* A Poset is Antisymmetric (not: Asymmetric)
* Since Antisymmetric in Coq is parametric in an equivalence relation,
  we just fix this equivalence to be propositional equality.
* Add (ℕ,≤) as an example
---
 Instance/Poset.v | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/Instance/Poset.v b/Instance/Poset.v
index e5d26a0a..72e118a6 100644
--- a/Instance/Poset.v
+++ b/Instance/Poset.v
@@ -8,7 +8,7 @@ Require Import Coq.Relations.Relation_Definitions.
 Generalizable All Variables.
 
 (* Any partially-ordered set forms a category (directly from its preorder,
-   since it simply adds asymmetry). See also [Pos], the category of
+   since it simply adds antisymmetry). See also [Pos], the category of
    partially-ordered sets (where the sets are the objects, and morphisms are
    monotonic mappings.
 
@@ -23,5 +23,16 @@ Generalizable All Variables.
    set is equivalent to a poset. Finally, every subcategory of a poset is
    isomorphism-closed." *)
 
-Definition Poset {C : Category} `{R : relation C}
-           `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P.
+Lemma eq_equiv {C : Type} : @Equivalence C eq.
+Proof.
+  split; auto. intros x y z; apply eq_trans.
+Qed.
+
+Definition Poset {C : Type} `{R : relation C}
+           `(P : PreOrder C R) `{@Antisymmetric C eq eq_equiv R} : Category := Proset P.
+
+Section Examples.
+Definition LessThanEqualTo_Category : Category :=
+  @Poset nat PeanoNat.Nat.le PeanoNat.Nat.le_preorder
+    (partial_order_antisym PeanoNat.Nat.le_partialorder).
+End Examples.