leanprover-community
feat(order/omega-cpo): cpos form a cartesian closed category
Could you fix the line lengths? (And perhaps switch some of the multiline bys to begin ... end?)
My understanding is that your doing this for the sake of an application to the semantics of programming langauges, right?
I've never really thought much about the various categories of blah-orders. On the one hand I'm tempted to worry about how much of this file generalises already to categories of weaker order structures. On the other hand I don't know the answers offhand, and so if there's an intended application at this level of specificity I guess I'm game to just judge this PR on whether it sensibly used the CCC API.
That's exactly right. I'm sure it can be generalized but I really don't know where I'd begin. I propose we start with this particular case and generalize when that becomes useful.
My understanding is that your doing this for the sake of an application to the semantics of programming langauges, right?
I've never really thought much about the various categories of blah-orders. On the one hand I'm tempted to worry about how much of this file generalises already to categories of weaker order structures. On the other hand I don't know the answers offhand, and so if there's an intended application at this level of specificity I guess I'm game to just judge this PR on whether it sensibly used the CCC API.
I've been thinking about this a little recently - it turns out the categories of blah-complete partial orders (for sensible values of blah) are all monadic over PartialOrder, so in particular are all complete, and the forgetful functor creates limits. I couldn't find any generalisation for which categories are CCC but I haven't thought a great deal about this.
As for this PR, I think it's a good idea to have completeness of wCPO (which is not hard to show directly rather than going via monadicity), instead of doing terminal and binary products specifically. The CCC stuff looks reasonable to me although I'm surprised it's necessary to have all the prod lemmas repeated rather than letting the existing ones do the work
@b-mehta I'd like to know more about using completeness instead of binary products and terminal objects. How do you state completeness?
@b-mehta I'd like to know more about using completeness instead of binary products and terminal objects. How do you state completeness?
@cipher1024 I put together a rough idea of what I meant in a separate branch so as to not clog up this one: mathlib/cpo-complete. It's a little less nice than I expected (I don't know the concrete category API that well), but you'll need some more limits than just products for LCCC anyway.
@b-mehta Who should we ask to look at how we're using the concrete category API?
This looks pretty good to me. I made a few minor changes while reading @b-mehta's branch, but nothing substantial.
I looked a bit at what would be required to port this to today’s mathlib. I don't have anything presentable yet, but I did create https://github.com/leanprover-community/mathlib/pull/13833 which may be useful :-)
