Isomorphism between MaybeT Identity a and Maybe a in Idris

IsoMaybe.idr

module IsoMaybe

import Control.Isomorphism

data MaybeT : (m : Type -> Type) -> Type -> Type where
  MaybeTC : { m : Type -> Type } -> m (Maybe a) -> MaybeT m a

data Identity : Type -> Type where
  IdentityC : a -> Identity a

unIdentity : Identity a -> a
unIdentity (IdentityC a) = a

isoMaybeTIdentityMaybe : Iso (MaybeT Identity a) (Maybe a)
isoMaybeTIdentityMaybe = MkIso to from toFrom fromTo where
  to : MaybeT Identity a -> Maybe a
  to (MaybeTC x) = unIdentity x

  from : Maybe a -> MaybeT Identity a
  from m = MaybeTC (IdentityC m)

  toFrom : (b : Maybe a) -> to (from b) = b
  toFrom b = Refl

  fromTo : (b : MaybeT Identity a) -> from (to b) = b
  fromTo b = let (MaybeTC (IdentityC y)) = b
             in Refl