Migrate _↔̇_ to the new Function hierarchy

[Saransh-cpp]

Xref #759

The issue currently does not mention a module where _↔̇_ should be moved to, but given that _↔_ was moved from Function.Inverse to Function.Bundles._, I have moved _↔̇_ in a similar fashion as well.

Edit: Oops, GitHub is automatically converting _↔̇_ with no backticks to ↔̇

[Taneb]

I'm not familiar with _↔̇_. This isn't really relevant to reviewing this PR but could someone explain to me what it's meant to represent and be used for?

[Saransh-cpp]

I couldn't figure out its usage too 🙂

[MatthewDaggitt]

Hmm so it looks like it's lifting the Inverse relation to indexed sets. I guess therefore it should really go in a new module Function.Indexed.Bundles. It'll be a bit lonely in there but eventually the module might get fleshed out.

Any chance you can move it there @Saransh-cpp ? If you were keen then you could add the equivalents of the other arrows below there too?

agda-stdlib/src/Function/Bundles.agda

Line 315 in cfa2504

infix 3 _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_

I think we should probably rename the arrow though to follow the naming conventions of the other indexed types as well as making it extendable, as I doubt the other arrow types have dotted variants. We should follow the convention below and use a subscript i instead:

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

Line 31 in cfa2504

infix 4 _≈ᵢ_ _≈_

therefore the name would change from _↔̇_ to _↔ᵢ_

[MatthewDaggitt]

Also very minor point, but could you avoid using unicode characters in branch names? It messes with some Github systems as well as being very difficult to type outside emacs 👍

[Saransh-cpp]

Woops, renaming the branch closed the PR, did not know that.

Thank you for the detailed comment! I'll add equivalents of the other arrows in the file too and rename the existing one to a better name.