Data.Container.Base.Fix.Definition

Definitions

data KleeneShp : Cont -> Type

  Kleene star, aka. the free monad monad on containers
  Is the least fixpoint in the category of containers of
  Kleene c = Scalar >+< (c >@ Kleene c)
  Since Idris doesn't support codata, we can also use this for greatest fixpoint
  by using corecursive shapes and marking them as partial

Totality: total
Visibility: public export
Constructors:

Done : KleeneShp c

More : Ext c (KleeneShp c) -> KleeneShp c

data KleenePos : KleeneShp c -> Type

Totality: total
Visibility: public export
Constructors:

DonePos : KleenePos Done

MorePos : (cp : c .Pos cs) -> KleenePos (f cp) -> KleenePos (More (cs <| f))

Kleene : Cont -> Cont

Totality: total
Visibility: public export

KleeneShp : c =%> d -> KleeneShp c -> KleeneShp d

Totality: total
Visibility: public export

KleenePos : (f : c =%> d) -> (ks : KleeneShp c) -> KleenePos (KleeneShp f ks) -> KleenePos ks

Totality: total
Visibility: public export

Kleene : c =%> d -> Kleene c =%> Kleene d

  Action on morphisms

Totality: total
Visibility: public export