[Discussion]: Moving setoid, ≡-setoid, and flip away from Function.Equality

[Saransh-cpp]

Related to #759

Now that agda-stdlib has a Function.Indexed directory, I think it would be nice to migrate setoid, ≡-setoid, and flip to the new hierarchy.

Along with these, I am unsure if other functions in Function.Equality must also be migrated somewhere. The issue mentions - "Missing an indexed function variant. Should go in a new hierarchy Function.Dependent.(Structures/Bundles)" - but I'm not sure if I understand that very well. Should the operators and functions not involving IndexedSetoid have a new indexed version of themselves in a different module, or should the indexed functions be moved to Function.Dependent.(Structures/Bundles)?

Moreover, should I start by moving _⇨_, Π, _⟶_, setoid, and ≡-setoid to Function.Indexed.Relation.Binary.Equality, given that all of them have IndexedSetoid involved within their definitions?

Thanks!

[MatthewDaggitt]

The remaining unported functions in Function.Equality are setoid, _⇨_, ≡-setoid, flip and →-to-⟶. Once again, they're slightly weird constructs so I think I'm going to omit them, and see if we get any complaints.

[JacquesCarette]

The first two (setoid, _⇨_) ,were needed, so there's now PRs for them.