Data.Functor.Indexed

Functors able to read some separate data, the "index".

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

The abbreviation "Ind" could be taken to stand for "Indexed", but
also for "Independent", to contrast it with the "Dependent"
versions elsewhere in the library.

Definitions

interface IndFunctor : Type -> (Type -> Type) -> Type

Parameters: i, f
Constraints: Functor f
Methods:

imap : (i -> x -> y) -> f x -> f y

Implementations:

IndFunctor k (Pair k)

IndFunctor () Maybe

IndFunctor Nat List

IndFunctor (Fin k) (Vect k)

Functor m => IndFunctor a (Kleisli m a)

imap : IndFunctor i f => (i -> x -> y) -> f x -> f y

Visibility: public export

(<|$>) : IndFunctor i f => (i -> x -> y) -> f x -> f y

Visibility: export
Fixity Declaration: infixr operator, level 4