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.

[MatthewDaggitt]

I definitely vote for explicit in this case. I often run into places where it can't be inferred.

[JacquesCarette]

If we make it "normal style" to use _ (i.e. space-underscore) when it can be, then explicit is pretty light-weight.

[jamesmckinna]

So... do we break the change introduced in #2240 (ahead of v2.1?) and standardise on explicit quantification? I propose that we do!

Adding this to the v2.1 milestone so we can agree/reject this proposal before v2.1-rc2... and so that someone can file a PR to implement it... pre-emptively #2429

[JacquesCarette]

Since this is indeed 'intra' v2.1, I think this is the way to go.

[jamesmckinna]

Closed by #2429

[jamesmckinna]

Reopening to reconsider #2381 (and possibly others?), which had previously followed Function.Relation.Binary.Equality.Setoid in having implicit quantification... and also are 'intra'v2.1 PR(s)

Some detective work required to track them all (maybe it is just this one?) down, but in the meantime, this is perhaps a wider library design issue that we should discuss... UPDATED or else regard our agreement on explicit quantification as being library-design/style-guide worthy as a design principle?

UPDATED: I think #2381 may in fact be the only outstanding inconsistency, now addressed in #2433 .

Downstream [DRY] issue: refactor all of these additions (and eg Function.Indexed.Relation.Binary.Equality) to use suitable versions of Relation.Binary.Indexed.Homogeneous.Core.Lift?

UPDATED Closing now in favour of #2434