Problems with Isos

Isos

class Profunctor (p : Type -> Type -> Type) where

  dimap : (a -> b) -> (c -> d) -> p b c -> p a d
  dimap f g = lmap f . rmap g

  lmap : (a -> b) -> p b c -> p a c
  lmap = flip dimap id

  rmap : (a -> b) -> p c a -> p c b
  rmap = dimap id

Iso : Profunctor p => Type -> Type -> Type -> Type -> Type
Iso {p} s t a b = p a b -> p s t

specialize : Profunctor q => ({p : _} -> Profunctor p => p a b -> p s t) -> q a b -> q s t
specialize f x = f x

record Forgotten r a b where
  constructor Forget
  runForget : a -> r

forwards : Profunctor p => Iso {p} s t a b -> s -> a
forwards {a} {b} {s} {t} i = runForget . fi $ Forget id where
  fi : Forgotten a a b -> Forgotten a s t
  fi = specialize i
  
record Tagged a b where
  constructor Tag
  runTagged : b

backwards : Profunctor p => Iso {p} s t a b -> b -> t
backwards {a} {b} {s} {t} i = runTagged . bi . Tag where
  bi : Tagged a b -> Tagged s t
  bi = specialize i

from : Profunctor p => Iso {p} s t a b -> Iso {p} b a t s
from i = dimap (backwards i) (forwards i)