New package: order theory

[nmvdw]

What do people think of adding a new package called 'OrderTheory' whose contents are as follows:

• The Lattice folder (https://github.com/UniMath/UniMath/tree/master/UniMath/Algebra/Lattice)
• The DCPOs folder (https://github.com/UniMath/UniMath/tree/master/UniMath/Combinatorics/DCPOs)
• The Posets folder (https://github.com/UniMath/UniMath/tree/master/UniMath/Combinatorics/Posets)

I think that this way, the filers are ordered more logically.

[benediktahrens]

Good with me!

[rmatthes]

For me, this proposal implies that the work leading to Pataraia's fixed-point theorem (monotone endofunctions on a pointed DCPO have a fixed point - no continuity needed) in https://github.com/UniMath/UniMath/blob/master/UniMath/Algebra/FixedPointTheorems.v is declared as obsolete - since it will not belong to the package. Currently, I do not see Pataraia's theorem. Is it maybe hidden through more abstraction?

[rmatthes]

A side question: is that theorem really an original result of Pataraia, or is it rather his proof that brought it into the realm of univalent mathematics? The book by Davey and Priestley (2nd ed.) discusses the statement as "CPO Fixpoint Theorem II". Then they say that previous proofs were known that relied on Zorn's lemma and that Pataraia's proof is "elegant". But that other previous proofs avoided the axiom of choice by using what they call "CPO Fixpoint Theorem III" on increasing self-maps on pointed DCPOs.

[nmvdw]

For me, this proposal implies that the work leading to Pataraia's fixed-point theorem (monotone endofunctions on a pointed DCPO have a fixed point - no continuity needed) in https://github.com/UniMath/UniMath/blob/master/UniMath/Algebra/FixedPointTheorems.v is declared as obsolete - since it will not belong to the package. Currently, I do not see Pataraia's theorem. Is it maybe hidden through more abstraction?

Good point. That file should be moved as well to that folder.

[rmatthes]

And what about the prerequisites for that file?

[m-lindgren]

I like this idea. I would also be in favor of moving the definitions of po (we should give this a more descriptive name IMO), Poset etc, and their associated functions out of Foundations and MoreFoundations into this new package.

[nmvdw]

And what about the prerequisites for that file?

See #1726 for a concrete suggestion on this.

[benediktahrens]

@nmvdw : is this issue solved?

[m-lindgren]

Related: #1067.

[nmvdw]

@nmvdw : is this issue solved?

Not fully yet. There is still some material that needs to be moved to OrderTheory (partial orders, well-founded sets).

[arnoudvanderleer]

@nmvdw If I understand this correctly, there are exactly two (parts of) files that still need to be moved?

[nmvdw]

Yes. The easiest change is to move https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/WellOrderedSets.v and https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/OrderedSets.v, and a more complicated change would be to move the stuff on posets.

[arnoudvanderleer]

The posets are more complicated because they are scattered through multiple files, or because their file has more references pointing to it?

[nmvdw]

I think both.

[arnoudvanderleer]

I think I'll also move Subposets.v.
Would it also be good to move StructureIdentity.v?