Skip to content

Commit

Permalink
Fix Definition of Instance/Poset.v
Browse files Browse the repository at this point in the history
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
  • Loading branch information
t-wissmann committed Dec 21, 2023
1 parent 41ab38d commit e2bcc89
Showing 1 changed file with 14 additions and 3 deletions.
17 changes: 14 additions & 3 deletions Instance/Poset.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.

0 comments on commit e2bcc89

Please sign in to comment.