[Agda] dependent inverse transitivity

[Alexander Altman]

I have been working on a form of dependent inverses within my lightly-modified version of the Agda standard library (based on version 0.7, if it matters).  The file in question is at https://github.com/pthariensflame/lib-adga/blob/master/src/Function/Inverse/Dependent.agda.

I am having trouble defining transitivity for them; that is, I would to close all the holes at the end of the file, but I seem to be blocked every step of the way.  In particular, Agda will not accept the various naïve congruence proofs I’ve tried when building `to`, `from`, `to-index` and `from-index`.  The problem seems to be that I need to transport parts of some of the intermediate types along the various proofs of the form `cong (Inverse.to-index _) _`, but I can’t figure out how to do so.  Can anyone help?

If it’s relevant, I’m using Agda 2.3.2.2 from Hackage.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140131/5066b77b/attachment.html