Add isMonotone Definition for Poset

[jmougeot]

I propose adding the following definition to represent monotone (order-preserving) functions between posets:

isMonotone : (P : Poset o ℓ e) → (Q : Poset o' ℓ' e') → (f : Poset.Carrier P → Poset.Carrier Q) → Set (o ⊔ ℓ ⊔ e ⊔ ℓ' ⊔ e')
isMonotone P Q f = IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f

• Provides a clear and reusable definition for monotone functions between posets.
• Enhances readability and aligns with existing structures like IsOrderHomomorphism.

Feedback on the definition, naming, and module placement is welcome.

[jamesmckinna]

See #2580 .
We have tended, historically, and only so far, built up layers of conceptual organisation in Algebra and Relation.Binary hierarchies, in order of generality/abstraction

• properties of 'bare' relations (perhaps wrt ambient IsEquivalence relation)
• properties of such relative to a given Algebra carrier structure (instantiating that relation)
• reified as a property of a given Structure
• and finally in terms of the associated Bundle.

For Homomorphisms, there is a further twist, namely as far as is possible, to parametrise not on the associated full Bundles, but rather only on their underlying Raw versions, in order to uncouple the definitions from depending on the ambient axiomatisations of the IsX structures at hand. Cf. the fact that Algebra.Definitions makes far fewer distinctions than Algebra.Properties precisely because so much of the underlying mechanics are shared between eg Magma/Semigroup/Monoid/Group (and Quasigroup/Loop) wrt the undelying binary 'multiplication', without having to invoke the specifics of its particular properties within any give structure.

Here, IIUC, this proposal inverts that order by going Bundle-first (unless I am missing something, are all the other parts already present), and I think that that is... perhaps a mistake, when a more fine-grained approach would be better/more flexible/more maintainable.

There may be something more categorical to say about 'fullness' of various subcategories (and faithfulness of forgetful functors) here, but I think that would obscure the picture...

[JacquesCarette]

I guess the most basic isMonotone should probably depend on 2 carriers and 4 relations (and a function), which is the bare minimum needed by IsOrderHomomorphism. I guess there is no obvious item for the second point, there is something missing for layer 3, and the above would be for layer 4.

[TOTBWF]

There are definitely some organizational reasons to prefer homomorphisms between raw structures, but this does not play out well in practice IME. The reasons for this are a bit subtle though. Suppose we had a definition of monotonicity like

record RawPreorder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _≲_        : Rel Carrier ℓ₂  -- The relation.

record IsRawPreorderHomomorphism
  (P : RawPreorder c ℓ₁ ℓ₂) (Q : RawPreorder c′ ℓ₁′ ℓ₂′)
  (f : RawPreorder.Carrier P → RawPreorder.Carrier Q)
  : Set _
  field
    -- Whatever you want here, doesn't really matter.

Now, suppose that you have a theorem about preorder homomorphisms that requires P and Q to be preorders, which is the typical use-case. If you use raw preorder homomorphisms, you will never be able to make P and Q implicit: agda can infer which raw preorders you are talking about from the record telescope of IsRawPreorderHomomorphism, but deducing the actual Preorders will basically never be possible.

[jamesmckinna]

Hmmm... not sure what your point is here @TOTBWF ? That wrt a given category, that Hom should be able to infer its arguments (qua bundles)? Fine if I could stipulate that eg Preorder homomorphisms should be understood as governed by Poset... but that's not how things are organised here? What am I missing?

As for not being able to supply arguments to lemmas as implicitly as one would maximally prefer... that's a compromise made throughout the library, with a default heuristic of more, rather than less, explicit. At least IIUC.

[TOTBWF]

Sorry, should have been more clear! In general, one should aim to be able to infer bundles/structures from their morphisms. Deviating from this leads to yellow when you try to compose two morphisms.

As for Poset/Preorder, this is a holdover from the 1Lab code that this was ported from. We found our order theory hierarchy atop Posets, which is the natural choice in univalent foundations. This probably isn't the right choice for the stdlib.

[jamesmckinna]

It may be that we need (?) to follow stdlib in defining IsXHomomorphism on Raw bundles but also having to add Bundle-specific Hom definitions (and their Biased versions, when less Structure is actually needed?) for the sake of the heuristic 'compose should be able to infer its arguments, within a given category'? At least, IIUC your point, @TOTBWF ?