[Agda] Isomorphisms, equational reasoning, and level changes

[Conal Elliott]

I’m trying to do “equational” reasoning on types where the equivalence is a
flavor of isomorphism (_↔_ from Function.Bundles, specializing Inverse from
that module). The types of begin_ in Relation.Binary.PropositionalEquality
 and sym in IsEquivalence, however, appear to disallow changing type during
the chain of reasoning; i.e., for proving A ~ B they require that A and B have
the same type. For many equivalence relations, this restriction is fine,
but isomorphisms often relate types having different levels, which is the
problem I’m encountering. Is there a known workaround?

Thanks, - Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201206/50948339/attachment.html>