Modular Formulation of Preorders, Posets, HeytAlg, etc

[GenericMonkey]

Issue raised in the first pass of creating a Hyperdoctrine. In order to modularly be able to scale the definition of a hyperdoctrine to other target categories we should refactor the construction with:

• Preorder as the basic category (can be stolen from other repo)
• A general subcategory construction for Posets, Heyting Algebras, w/ one adjoint, w/ 2 adjoints, etc).

[maxsnew]

Additionally shouldn't a lot of this go under Cubical.Preorders instead of Cubical.Categories ?

[GenericMonkey]

Reopening this after our discussion about how to redesign the order theory stuff.

Recapping for convienence. Currently we have:

• a non-upstream file Cubical.Relation.Binary.Preorder that is basically a copy of the upstream library's Cubical.Relation.Binary.Poset, removing the is-antisym field.
• a file defining MonFun between two Preorders
• a file defining the thin notion of adjoint, i.e. adjoints for monotone functions.
• IsPreorder has an isSet requirement on the underlying type.
• PREORDER is defined as a category with objects being Preorders and morphisms being MonFuns
• POSET is defined using FullSubcategory and IsPoset (which has a lot of redundant info due to `Preorder already having a lot of the information)
• POSETADJ, POSETADJL POSETADJR defined using our homebrewed Displayed Category/Displayed Poset

We've chatted a bit about reformatting this hierarchy, so I'm reopening this issue to track. A couple ideas I remember us chatting about:

• [x] Stop using IsPoset as defined in the upstream Relation.Binary.Poset.
• [x] Define an isUnivalent record for the Preorder type, and use this instead.
• [x] Propagate and rebuild the subcategories described above using the new library Displayed Categories
• [ ] Define meets, joins, heyting implication in a similar modular way so we can continue making these subcategories modularly

I removed the isSet requirement in IsPreorder and defined isUnivalent by basically copying the record from the Cubical.Categories.Category definition, and was able to prove the analogous PathToOrderEquiv and isSet proofs. A few issues this brought up:

• If we are going to redefine PREORDER, we now need a Σ[ P ∈ Preorder ] isSet (P .fst) as our objects.
• However, now it seems like for POSET, since we get isSet for free from our Preorder being univalent, we don't necessarily want it to be subcategory of Σ[ P ∈ Preorder ] isSet (P .fst) but just Preorders (which aren't a category). Should we make POSET a primitive category with objects Σ[ P ∈ Preorder ] isUnivalent P? or is the Subcategory formulation more useful?
• Since we are basically reusing proofs about Categories (and will end up doing the same thing for meets, joins, heyting implication down the line), is it worth defining Preorders as thin categories? or are the degenerate notions of these concepts still useful to have independently?
• Cubical.Binary.Relation already has a different notion of isUnivalent: an equality between R a a' and a ≡ a'. So a Preorder isUnivalent if the OrderEquiv relation isUnivalent. Unfortunately this leads to some naming clashes that we'll need to fix as well.

[maxsnew]

Some thoughts:

Should we make POSET a primitive category with objects Σ[ P ∈ Preorder ] isUnivalent P? Yes I think so

Since we are basically reusing proofs about Categories (and will end up doing the same thing for meets, joins, heyting implication down the line), is it worth defining Preorders as thin categories? or are the degenerate notions of these concepts still useful to have independently? I don't think we should define Preorders to be thin categories, but we should prove that they are Iso and similarly monotone functions are iso to functors etc and try to reuse the work on universal properties in categories as much as possible.

[maxsnew]

I've completely changed my mind about this now that I have more experience. We should just define a preorder/poset to be a category/univalent category that hasPropHoms.