Max S. New

I think if we want a "most general" version of a universal property, a good one to pick in my experience is "representable profunctor", i.e. a profunctor C^o x D...

> I think I still need the ad hoc variant for individual instances: One of the nice things about representables is that they subsume these cases as well. I.e., a...

And I agree with Felix's plan. More concretely, we can define representable profunctor in some module and prove some "Yoneda facts": 1. It determines a functor up to unique natural...

@anuyts You can show that for a fixed profunctor R : C^o x D -> Set that the following are equivalent: 1. A functor F : C -> D and...

More broken links here: https://lalrpop.github.io/lalrpop/tutorial/index.html The link to sub-section 001 is https://lalrpop.github.io/lalrpop/tutorial/tutorial/001_adding_lalrpop.html and should be https://lalrpop.github.io/lalrpop/tutorial/001_adding_lalrpop.html etc

Why wouldn't the definition from category theory be general enough?

Sure I can review

Sounds hard