IdrisDoc: Control.Isomorphism

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