What's the 'right' notion of equality between functions?

[jamesmckinna]

We have the pointwise PropositionalEquality definition _≗_ (moved in #2335 )

_≗_ {A = A} {B = B} f g = ∀ x → f x ≡ g x

and the Function definition _≈_ (since #2240 and its antecedent issues back to #1467 )

_≈_ : (f g : Func From To) → Set (a₁ ⊔ b₂)
f ≈ g = {x : From.Carrier} → f ⟨$⟩ x To.≈ g ⟨$⟩ x

and... we are (once again!) inconsistent as to implicit/explicit quantification.

@JacquesCarette has argued for the implicit version; @Taneb 's recent topic thread on Zulip suggests that this is not always the right choice.

Maybe there's room for both, but it doesn't feel quite right to me... or else, the distinction should be documented.

[JacquesCarette]

I agree that it feels inconsistent. Normally, I'd go for implicit when practice shows that it can often be inferred - but it turns out that practice is very mixed on that front! In those cases, I think going explicit is the better choice.