IdrisDoc
: Control.Isomorphism
Index
Control.Isomorphism
MkIso
:
(
to
:
a
->
b
) -> (
from
:
b
->
a
) -> (
toFrom
: (
y
:
b
) ->
to
(
from
y
)
=
y
) -> (
fromTo
: (
x
:
a
) ->
from
(
to
x
)
=
x
) ->
Iso
a
b