Data.Indexed.FixedDep

We can regard any functor as dependently indexed, with specified
fixed index.

Definitions

record FixDepIndex : i -> (Type -> Type) -> (i -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

WithDepIndex : f (a x) -> FixDepIndex x f a

Projection: 

.unIndex : FixDepIndex x f a -> f (a x)

Hints:

Filterable f => DepFilterable i (FixDepIndex x f)

Foldable f => DepFoldable i (FixDepIndex x f)

Functor f => DepFunctor i (FixDepIndex x f)

Traversable f => DepTraversable i (FixDepIndex x f)

Witherable f => DepWitherable i (FixDepIndex x f)

.unIndex : FixDepIndex x f a -> f (a x)

Visibility: public export

unIndex : FixDepIndex x f a -> f (a x)

Visibility: public export