<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">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 <a href="https://github.com/pthariensflame/lib-adga/blob/master/src/Function/Inverse/Dependent.agda">https://github.com/pthariensflame/lib-adga/blob/master/src/Function/Inverse/Dependent.agda</a>.<div><br></div><div>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?</div><div><br></div><div>If it’s relevant, I’m using Agda 2.3.2.2 from Hackage.</div></body></html>