search

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
750 stars 69 forks source link

Can you explain uhom? #2

Closed MarisaKirisame closed 7 years ago

MarisaKirisame commented 7 years ago

So here is some code in Category.v Class Category := { ob : Type; uhom := Type : Type; hom : ob → ob → uhom where "a ~> b" := (hom a b); ...

what will happend if hom is ob -> ob -> Type instead, why wont universe polymorphism work?

jwiegley commented 7 years ago

Initially I had exactly that, but I ran into Universe polymorphism issues. It's possible these have been fixed in the 8.5 or 8.6 releases, so I would recommend giving it a try.

MarisaKirisame commented 7 years ago

👍 Will report back if I had successfully formalize major stuff without that.