Should the index argument `I` be implicit or explicit for indexed relations?

[MatthewDaggitt]

See the discussion #1511 (comment). I'd welcome any feedback from anyone else who has used it?

agda-stdlib/src/Relation/Binary/Indexed/Homogeneous/Core.agda

Line 32 in 358ad8b

IREL A B ℓ = ∀ {i} → REL (A i) (B i) ℓ

[MatthewDaggitt]

@jamesmckinna "This is something intimately linked to eta-expanding of functions and therefore is an upstream issue"