Data.Functor.Dependent

Functors with type depending on some extra data, the "index"

They are expected to obey the laws
  imap g . imap f = imap (\i => g i . f i)
and
  imap (\i => id {t i}) = id

Definitions

interface DepFunctor : (i : Type) -> ((i -> Type) -> Type) -> Type

Parameters: i, t
Methods:

dmap : ((x : i) -> u x -> v x) -> t u -> t v

Implementations:

DepFunctor i (DPair i)

DepFunctor k (SortedDMap k)

dmap : DepFunctor i t => ((x : i) -> u x -> v x) -> t u -> t v

Visibility: public export