Data.Container.Base.Endofunctor.Definition

Reexports

Definitions

(<!>) : (Type -> Type) -> Cont -> Cont

  If `f` is a monad, then `f <!> -` is a comonad, and vice versa

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

(<!>) : (f : (Type -> Type)) -> Functor f => c =%> d -> (f <!> c) =%> (f <!> d)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

(!!) : Cont -> Cont

  Comonad of the adjunction between Cont and Cont_Mon
  BANG. List on positions, always has a monoid structure

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

(!*) : Cont -> Cont

  Comonad of the adjunction between Cont and AddCont
  Bag on positions, always has a commutative monoid structure

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

(!!) : c =%> d -> (!!) c =%> (!!) d

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

(!*) : c =%> d -> (!*) c =%> (!*) d

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

pureBw : Monad m => (m <!> c) =%> c

  Turn a banged container into a container
  Requires pure on the backward pass
  At `m = Bag` this is the counit of `UC -| !*`, i.e. `addContTransposeInv id`

Totality: total
Visibility: public export

joinBw : Monad m => (m <!> c) =%> (m <!> (m <!> c))

Totality: total
Visibility: public export

ListAll : Cont -> Cont

Totality: total
Visibility: public export

ListAny : Cont -> Cont

Totality: total
Visibility: public export

BagAll : Cont -> Cont

Totality: total
Visibility: public export

unitBag : c =%> BagAll c

Totality: total
Visibility: public export

bww : (f : c =%> d) -> (cs : List (c .Shp)) -> All (d .Pos) (f .fwd <$> cs) -> All (c .Pos) cs

Totality: total
Visibility: public export

List : c =%> d -> ListAll c =%> ListAll d

Totality: total
Visibility: public export

Pointed : Cont -> Cont

  A pointed container additionally in its shape contains the data of also one
  distinguished position
  Unlike with `Deriv`, decidability is not needed

Totality: total
Visibility: public export