HasEquiv in Type?

Stream: lean4

[Jason Gross]

Is there a reason that HasEquiv in the standard library uses Prop rather than Sort _? I'd like to be able to use ≈ with relations that live in Type...

[Mario Carneiro]

Do we have universe out-params? That seems like a prerequisite for this to work

[Jason Gross]

I think it already works. That is to say, I've had no trouble with

class HasArr (α : Sort u1) where
  Arr : α → α → Sort u2

infix:70 " ~> " => HasArr.Arr

[Leonardo de Moura]

Pushed this change: https://github.com/leanprover/lean4/commit/c54a7c8ccc75e0a664560b53d26987b0a7bb861b

@Mario Carneiro We have modified the typeclass resolution procedure a few weeks ago. All universes are out-param by default now like in Lean 3.

[Jason Gross]

Thanks!