Respects₂-generic ?

[mechvel]

Relation.Binary.Core has _Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _

And I introduce

  Respects₂gen : ∀ {α α= β β= ℓ} {A : Set α} {B : Set β} →
                               (A → B → Set ℓ) → Rel A α= → Rel B β= → Set _  
  Respects₂gen _~_ _~₁_ _~₂_ = ∀ {x x' y y'} → x ~₁ x' → y ~₂ y' → x ~ y → x' ~ y'

Example:

Respects₂gen _∈_ _≈_ _=set_ =    x ≈ x' → ys =set ys' → x ∈ xs → x' ∈ ys'`

expresses that the equality =set on lists (\xs ys -> xs ⊆ ys × ys ⊆ xs) agrees with
the equality _≈_ on elements and with the relation _∈_ betwen elements and lists.

Has Standard library a replacement for Respects₂gen ?
Has it a denotation for (A → B → Set ℓ) ?
(somewhat "Rel-heterogeneous A B" ? ...)

[mechvel]

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:

≈

[mechvel]

How to enter here the underscore symbol?

[fmap]

`_≈_`

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

[MatthewDaggitt]

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 _≈₂_)

[mechvel]

On Sun, 2018-03-18 at 08:06 -0700, MatthewDaggitt wrote: Hmm I can envisage a use case for such a proof. 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?

I like more prefix Respects₂gen or prefix Respects₂-∧. But I would not argue against this _Respects₂_∧_.

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 _≈₂_)

My impression was that _Respects₂_ of Standard is difficult to use. So that I have introduced _Respects2_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _ _Respects2_ _~_ _≈_ = ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ~ y → x' ~ y'

…

-- SM

[gallais]

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.

[mechvel]

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.