jonsterling / coq-domains Goto Github PK

https://planetmath.org/IdealCompletionOfAPoset (as per Andrej Bauer's suggestion)

HierarchyBuilder causes a lot of noisy elpi-related warnings. I wonder if we can (or should) silence these...

• define lift of a set
• prove it is a dcpo
• prove the universal property

This is done already by De Jong and Escardo in Agda: https://github.com/tomdjong/TypeTopology/blob/master/source/DcpoLimits.lagda. I'd like to have that in this library too.

There is a remarkable idea from Moegelberg that Lars Birkedal pointed out to me. Recall that it not the case that EM(Lift) = Kleisli(Lift) in the constructive setting (see #24); the problem is roughly that you cannot "un-point" / unlift a pointed domain. But an approach proposed by op. cit. is to replace Cpo by co-EM(!) where ! is the comonad on EM(Lift) corresponding to Lift; then we have a new monad Lift' : co-EM(!) -> co-EM(!), and we may consider the Kleisli category for this monad as a replacement for pCpo.

Marcelo Fiore has been explaining his work on Abstract Domain Theory to me, and I think it would be nice to formalize some of it, especially over an arbitrary Grothendieck topos. One good step is to formalize a generalized notion of omega-cpo. The recipe seems to be the following:

1. Start with a lifting monad L on some category. For example, consider the lifting monad on posets.
2. Let \omega be the initial L-algebra. In SET with (+1), this is the natural numbers but in general, but it is natural to consider the topos's partial map classifier, and in that case you get something that looks like the natural numbers but also has some spooky stuff in there.
3. There is an algebraic structure of a "formally \omega-complete object" that one can define on top of your original category, explained in this paper.

If you start with posets and the set theoretic partial map classifier, you get exactly the theory of \omega-cpos. If you replace posets with sets, you get something kind of degenerate. But what is useful to me about this is that you can generate the "correct" theory of \omega-cpos for an arbitrary topos in this way. It would be excellent to work out the details in Coq.

mathcomp-analysis currently has infrastructure for surjective functions on sets at math-comp/analysis@master/theories/functions.v. There's an initiative (registration-free mirror here) to generalize this machinery and move it to mathcomp proper, which we could potentially reuse.

The lift is producing only flat domains... This is the lift of a set, but not of a domain. In particular, the unit is not even monotone.

It is totally crazy how I am creating merge conflicts with every commit LOL.

I conjecture that for any dcpo D, the relation <=_D is equivalent to the image of [Σ, D] -> [2,D].

Developing this properties of this category, including its algebraic compactness (which remains conjectural in a constructive setting as far as I am concerned, but seems plausible) will be important for connecting this work to Axiomatic Domain Theory and thence to Synthetic Domain Theory.

Just to remember, unlike in classical domain theory, here we will not expect the Kleisli category of the lift monad to be equivalent to the Eilenberg-Mac Lane category.

We have one definition that applies only to dcpos, and another more general and relaxed definition that also applies to arbitrary posets. I think we should switch to the latter globally, but I'm open to ideas.