[Agda] Isomorphisms, equational reasoning, and level changes

[Matthew Daggitt]

Hi Conal,
I think the existing specialised reasoning combinators in Function.Related
<https://github.com/agda/agda-stdlib/blob/eb338fd27861f8c9db1359fda6e0ad24df555ae0/src/Function/Related.agda#L309>
for
the old function hierarchy infrastructure do what you want. See
Data.List.Relation.Unary.Any.Properties
<https://github.com/agda/agda-stdlib/blob/eb338fd27861f8c9db1359fda6e0ad24df555ae0/src/Data/List/Relation/Unary/Any/Properties.agda#L678>
for an example of how these can be used. Unfortunately this has not yet
been ported across to the new function hierarchy...

I haven't thought deeply about how the standard reasoning combinators could
be made to work with this level of generality. Let me know if you come up
with something!
Cheers,
Matthew

On Mon, Dec 7, 2020 at 1:42 PM Conal Elliott <conal at conal.net> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201208/c7f85e06/attachment.html>