Include proof of bijection in ⇓W⇑ class
Created by: joaopizani
From @joaopizani on June 8, 2014 11:22
Currently the ⇓W⇑
typeclass claims to "store" an isomorphism in the form of a pair of functions (⇓
and ⇑
). We should have therefore a proof that it actually constitutes an isomorphism, and this proof should be in ⇓W⇑
as well.
Copied from original issue: joaopizani/piware#15
Imported comments:
By joaopizani on 2015-04-04 16:17:55 UTC
Not exactly an isomorphism, as we are not requiring it to "preserve" any operation. We just want the ⇓W⇑
functions to be bijective and inverses of each other, really.
By joaopizani on 2015-04-04 16:17:55 UTC
Proving Iso in ⇓W⇑-×
turned out to be a bit harder than expected, delaying it for a while now...