[Agda] Ill-typed with construction

[Jacques Carette]

The page 
https://agda.readthedocs.io/en/latest/language/with-abstraction.html is 
extremely informative (thanks!), but the subsection 
https://agda.readthedocs.io/en/latest/language/with-abstraction.html#ill-typed-with-abstractions 
is a bit problematic in that it leaves off the most important part: how 
to fix it!

This is motivated by a real breakage (still the categories library).  
Try as I might, I simply cannot hand-write the correct "with" 
incantation to fix the one that used to work pre-2.5, and now is broken 
[1].  The example is very much like the one in the documentation linked 
to above, just "more so" in that there are many more type-level 
dependencies.

If someone could hand-write the correct helper function that fixes the 
documentation, hopefully that would be a big enough hint that I can 
figure this out myself.

Jacques

[1] last line of 
https://github.com/copumpkin/categories/blob/master/Categories/NaturalIsomorphism.agda 
for those who are curious.