jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
757 stars 70 forks source link

Fix Definition of Instance/Poset.v #136

Closed t-wissmann closed 8 months ago

t-wissmann commented 11 months ago

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

t-wissmann commented 11 months ago

The new type of @Poset is:

@Poset
     : ∀ (C : Type) (R : relation C), PreOrder R → Antisymmetric C eq R → Category
t-wissmann commented 11 months ago

With this PR I'd like to fix the issues in the current definition. Still, since antisymmetry isn't used at all in the definition of Poset, I wonder what the benefit of the definition is, anway.

t-wissmann commented 8 months ago

Thanks!