Data.Indexed.Independent

We can treat any dependent functor as an independent functor by
using constant index

Definitions

record Independent : ((k -> Type) -> Type) -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

Indep : t (const v) -> Independent t v

Projection: 

.dep : Independent t v -> t (const v)

Hints:

(DepFilterable i t, DepFoldable i t) => Filterable (Independent t)

DepFoldable i t => Foldable (Independent t)

DepFunctor i t => Functor (Independent t)

(DepFilterable i t, DepFoldable i t) => IndFilterable i (Independent t)

(DepFoldable i t, DepFunctor i t) => IndFoldable i (Independent t)

DepFunctor i t => IndFunctor i (Independent t)

(DepTraversable i t, (DepFunctor i t, DepFoldable i t)) => IndTraversable i (Independent t)

(DepTraversable i t, DepFunctor i t) => Traversable (Independent t)

DepWitherable i t => Witherable (Independent t)

.dep : Independent t v -> t (const v)

Visibility: public export

dep : Independent t v -> t (const v)

Visibility: public export