agda
Very dependent map
Closes #833 .
The names, of course, are up for debate! (And, now that I think of it, I should probably add a property or two of them in this same PR).
Re: naming Is it possible to reconcile the name choices for this PR, and the general principles in #278 ?
I guess this would push towards naming the first one simply map? Except that Data.Product.Base already has such a thing, and it is much less dependent.
My feeling is that #278 deals with the case of "normally dependent" naming -- here the functions really are absurdly dependent. So they seem like they'd need their own, new column. Interestingly, the various type families in dep-map are left implicit, and Agda seems happy enough with that. Having said that, I tried to apply dep-map to non-dependent cases, and it all became a giant yellow party.
In other words, we don't need the results of @gallais 's #278 experiment to know that we can't make these very-dependent version the 'default' with the most basic name.
Thanks - these are all great suggestions. (The h i actually come from me cutting and pasting from elsewhere in stdlib, but I'll accept the blame for not relabeling). Will implement as soon as I have a moment.
I think we're there now! Would you be happy to merge @MatthewDaggitt ?