Open t-wissmann opened 1 year ago
The definition of Poset in Instance/Poset.v currently is:
Poset
Instance/Poset.v
Definition Poset {C : Category} `{R : relation C} `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P.
I think there are two issues:
C
Type
R
Antisymmetric
Asymmetric
This second issue implies that all inhabitants of Poset are empty, i.e. any element of a poset leads to a contradiction:
Require Import Category.Lib. Require Import Category.Theory.Category. Require Import Category.Instance.Proset. Require Import Coq.Classes.Equivalence. Require Import Coq.Relations.Relation_Definitions. Generalizable All Variables. Set Implicit Arguments. Definition Poset {C : Type} `{R : relation C} `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P. Theorem there_is_no_poset {C : Type} `(P : PreOrder C R) `{Asymmetric C R} : Poset P -> False. Proof. intro x. simpl in *. destruct P as [refl _]. eapply H; unshelve apply (refl x); apply (refl x). Qed.
I assume the definition should be revised as follows:
Definition Poset {C : Type} `{R : relation C} `(P : PreOrder C R) `{Antisymmetric C R} : Category := Proset P.
If there aren't any further subtleties that I missed, I can prepare a PR.
@t-wissmann Thank you for pointing this out! I'd happily accept a PR.
The definition of
Poset
inInstance/Poset.v
currently is:I think there are two issues:
C
should only be aType
and not a category (the morphism structure isn't used anywhere as far as I can see)R
should beAntisymmetric
instead ofAsymmetric
.This second issue implies that all inhabitants of
Poset
are empty, i.e. any element of a poset leads to a contradiction:I assume the definition should be revised as follows:
If there aren't any further subtleties that I missed, I can prepare a PR.