Respects₂-generic ? about agda-stdlib HOT 7 OPEN

Strangely, this editor cancels many of underscores that I set in the code.
Let me try to copy-paste the underscore from the first line:

≈

from agda-stdlib.

How to enter here the underscore symbol?

from agda-stdlib.

`_≈_`

https://guides.github.com/features/mastering-markdown/

from agda-stdlib.

Hmm I can envisage a use case for such a type. Not sure about the name Respects₂gen though. My alternative is:

_Respects₂_∧_ : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
                REL A B ℓ₁ → Rel A ℓ₂ → Rel B ℓ₃ → Set _
_∼_ Respects₂ _≈₁_ ∧ _≈₂_ = ∀ {x y u v} → x ∼ u → x ≈₁ y → u ≈₂ v → y ∼ v

Still not entirely happy with it though. Thoughts?

The other question is whether we define it as a product ala _Respects₂_

_Respects₂_∧_ : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
                REL A B ℓ₁ → Rel A ℓ₂ → Rel B ℓ₃ → Set _
_∼_ Respects₂ _≈₁_ ∧ _≈₂_ = (∀ {y} → (_∼ y) Respects _≈₁_) ×
                            (∀ {x} → (x ∼_) Respects _≈₂_)

from agda-stdlib.

from agda-stdlib.

I keep introducing generalisations of the combinators in Relation.Binary.Core, the
latest being P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y so I can sympathise.

I would go even further and suggest:

_⟶_Respects₂_∧_ :
  ∀ {a b c d r s ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
  (R : REL A B r) (S : REL C D s) (_≈₁_ : REL A C ℓ₁) (_≈₂_ : REL B D ℓ₂) → Set _
R ⟶ S Respects₂ _≈₁_ ∧ _≈₂_ = ∀ {a b c d} → a ≈₁ c → b ≈₂ d → R a b → S c d

The others can be defined as specialisations.

The other question is whether we define it as a product ala _Respects₂_

I would say yes because this one is usable even when the respected relations are not
reflexive. However it may be worth defining an ad-hoc record type rather than using
a product, this way we can provide the two-in-one-go as a definition in the record's
module.

from agda-stdlib.

Currently I define and use

 RELRespects :  REL A B ℓ → Rel A ℓ₁ → Rel B ℓ₂ → Set _
 RELRespects _~_ _~₁_ _∼₂_ =
                         ∀ {x x' y y'} → x ~₁ x' → y ∼₂ y' → x ~ y → x' ~ y'

and suggest this for Standard library.

The attempt with _Respects_×_ failed because when it is applied to examples, it overlaps with applying _Respects_,
so that one is forced to apply (_Respects _×_ ~ ~'1 ~2) with ignoring the infix possibility.

from agda-stdlib.