Add dependent congruence of arity 1 and 2 for heterogeneous equality to Prelude

[Russoul]

[gallais]

I'm not sure this needs to be in prelude, the library meant for things you almost can't write any program without.

[Russoul]

Right, I remember now that Edwin emphasized that point of view a few times.

[buzden]

Hmm... Are cong and cong2 needed for almost any program, then?

[Russoul]

"Not being able to write any program without" is rather vague. I am sure there are ways to interpret that for and against adding depCongX based on availability of congX. But I don't have a strong opinion. I don't mind relocating depCong or closing this altogether.

[ohad]

I'm comfortable with moving cong and cong2 out of the prelude and into base.

[stefan-hoeck]

I'm comfortable with moving cong and cong2 out of the prelude and into base.

Please remember that such a change will break every library using these functions. Sure, the fix would be trivial, but we still have to be careful about breaking changes in the Prelude.

[gallais]

In my experience cong is needed as soon as you try to prove anything about any program.

[andrevidela]

In order to keep the name of the namespace consistent and expressive, I propose we place this function in a module Basics.Dependent in `base. How does that sound?

[joelberkeley]

I've been forwarded this thread from #2601

what's the purpose of Basics in Prelude and what would it's role be in base?

[andrevidela]

Basics contains all the combinators on functions that we expect from a functional programming language, in particular it contains both cong and flip https://github.com/idris-lang/Idris2/blob/main/libs/prelude/Prelude/Basics.idr

Importing a dependent version of it seems to remain consistent with Prelude.Basics.

One thing that goes against this naming is that regular users aren't supposed to interact with the Basics namespace, so they almost certainly have no experience importing something from the Basics namespace, which would make importing from Basics.Dependent unintuitive

[andrevidela]

@Russoul @gallais @joelberkeley any feedback or ideas about Basics.Dependent in base?

[joelberkeley]

One thing that goes against this naming is that regular users aren't supposed to interact with the Basics namespace

is this specific to Basics? Or is this just a consequence of being in Prelude?

[andrevidela]

is this specific to Basics? Or is this just a consequence of being in Prelude?

It is a consequence of being in Prelude

[Russoul]

@Russoul @gallais @joelberkeley any feedback or ideas about Basics.Dependent in base?

That works for me! I don't really have a preference.