Mistakes in the definition of Poset

[t-wissmann]

The definition of Poset in Instance/Poset.v currently is:

Definition Poset {C : Category} `{R : relation C}
           `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P.

I think there are two issues:

1. C should only be a Type and not a category (the morphism structure isn't used anywhere as far as I can see)
2. The relation R should be Antisymmetric instead of 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.

[jwiegley]

@t-wissmann Thank you for pointing this out! I'd happily accept a PR.