fact: Definition Poset {C : Category} `{R : relation C} `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P.
imports: Category.Lib Category.Theory.Category Category.Instance.Proset Coq.Classes.Equivalence Coq.Relations.Relation_Definitions