subrelation on more than one type

Stream: Is there code for X?

[Paul Rowe]

I'm looking for something along the lines of the following:

def subrelation' {α β : Type*} (r : α → β → Prop) (s : α → β → Prop) :=
λ a b, r a b → s a b

All I'm finding is subrelation which requires the types to be the same. This seems too basic to be missing. Is it an instance of a more general thing I'm not finding? Perhaps something like a relation on an indexed family of types?

[Yaël Dillies]

This is just ≤. r ≤ s means ∀ a, r a ≤ s a which means ∀ a b, r a b ≤ s a b which means ∀ a b, r a b → s a b.

[Paul Rowe]

Where is this partial_order instance defined?

[Yaël Dillies]

It's a special case of docs#pi.has_le applied twice. For the outer application, set ι to be α and α to be λ _, β → Prop.

[Paul Rowe]

Oh I see. Got it. Thanks!

[Eric Wieser]

Another spelling is (r ⇒ s) id id (docs#relator.lift_fun), but that's rather cryptic

[Paul Rowe]

Oh, nice. I agree it's rather cryptic, but the double application of pi.has_le is a certain kind of cryptic too. In the end, just knowing that ≤ would work was sufficient. I'm just always curious to dig a little deeper to see the definition.