
  0 | ||| Functors with type depending on some extra data, the "index"
  1 | |||
  2 | ||| They are expected to obey the laws
  3 | |||   imap g . imap f = imap (\i => g i . f i)
  4 | ||| and
  5 | |||   imap (\i => id {t i}) = id
  6 | module Data.Functor.Dependent
  7 | 
  8 | import Data.SortedMap.Dependent
  9 | 
 10 | 
 11 | public export
 12 | interface DepFunctor (0 i : Type) (0 t : (i -> Type) -> Type) | t where
 13 |   dmap : {0 u : i -> Type} -> {0 v : i -> Type} -> ((x : i) -> u x -> v x) -> t u -> t v
 14 | 
 15 | export
 16 | {0 i : Type} -> DepFunctor i (DPair i) where
 17 |   dmap f (x ** y) = (x ** f x y)
 18 | 
 19 | %inline
 20 | impl : {0 u,v : i -> Type} -> ((x : i) -> u x -> v x) -> {x : i} -> u x -> v x
 21 | impl f {x} = f x
 22 | 
 23 | DepFunctor k (SortedDMap k) where
 24 |   dmap f = Dependent.map $ impl f
 25 |