Agda-stdlib: Preorder VS reflexivity + transitivity?

[HuStmpHrrr]

Is there any similar discussions before on this part?

The textbook definition of preorder is a structure with reflexivity and transitivity, but in this library, preorder itself equips with an underlying equivalence relation. However, there are occasions that this equivalence relation is irrelevant, as can be seen here:

https://github.com/HuStmpHrrr/agda-stdlib/blob/master/src/Relation/Binary/Properties/Preorder.agda

The InducedEquivalence does not care about the equivalence relation, and this induced relation is simply induced from the textbook definition of preorder. It's very tempted to define things like these ones:

https://github.com/HuStmpHrrr/agda-stdlib/blob/16e1cc46b62842f703aee535c600444d695d3b77/src/Relation/Binary/InducedStructures.agda

which is minimal of what is actually needed.

Indeed the textbook definition is not entirely isolated, as it can be resolved by setting the underlying equivalence to be propositional equality. What's the recommended way to make this distinction in this library? Or is it worth a distinction?

[WolframKahl]

In the setoid view of the world, which is the view taken by most of the standard library here, reflexivity only makes sense with respect to the equivalence relation of the underlying setoid. The induced equivalence relation of a preorder is in general coarser, and the preorder that has the induced equivalence relation as its setoid equivalence relation is an order (your InducedPoset).

In many cases (but not in all!) we will indeed start from preorders that use propositional equality as the equivalence underlying reflexivity ─ I tend to prefer to make that explicit, but notational support for that may still come in useful.

The InducedEquivalence does not care about the equivalence relation

That is okay, but invIsPreorder does care ─ it re-uses it.

which is minimal of what is actually needed

... in cases where what you have is a Reflexive proof instead of the more general

    -- Reflexivity is expressed in terms of an underlying equality:
    reflexive : _≈_ ⇒ _∼_

Using your InducedStructures with actual Preorders would require adaptation.

As a matter of attitude, I recommend considering the setoids based on propositional equality to be the special case, and design for the general case.

[HuStmpHrrr]

thank you. makes perfect sense.