Data.Container.Additive.Morphism.Instances

(source)

Definitions

toState : c .Shp -> Scalar =%> c

Visibility: public export

fromState : Scalar =%> c -> c .Shp

Visibility: public export

toCostate : ((x : c .Shp) -> c .Pos x) -> c =%> Scalar

Visibility: public export

fromCostate : c =%> Scalar -> (x : c .Shp) -> c .Pos x

Visibility: public export

pushDown : AddCont -> AddCont

Visibility: public export

pushIntoContinuationList : (d >< p) =%> l -> p =%> (pushDown d >@ List l)

Visibility: public export

pushIntoContinuation : IsFlat l => Num (l .Shp) => (d >< p) =%> l -> p =%> (pushDown d >@ l)

Visibility: public export

constantOne : InterfaceOnPositions c Num => c =%> Scalar

Visibility: public export

leftUnit : (Scalar >< c) =%> c

Visibility: public export

rightUnit : (c >< Scalar) =%> c

Visibility: public export

leftUnitInv : c =%> (Scalar >< c)

Visibility: public export

rightUnitInv : c =%> (c >< Scalar)

Visibility: public export

assocL : ((a >< b) >< c) =%> (a >< (b >< c))

Visibility: public export

assocR : (a >< (b >< c)) =%> ((a >< b) >< c)

Visibility: public export

swap : (a >< b) =%> (b >< a)

Visibility: public export

leftUnit : (Scalar >@ c) =%> c

Visibility: public export

rightUnit : (c >@ Scalar) =%> c

Visibility: public export

leftUnitInv : c =%> (Scalar >@ c)

Visibility: public export

rightUnitInv : c =%> (c >@ Scalar)

  Right unit inverse: c =%> c >@ I

Visibility: public export

elim : (c >+< c) =%> c

Visibility: public export

duoidal : ((c >@ d) >< (e >@ f)) =%> ((c >< e) >@ (d >< f))

Visibility: public export

coprodDistrOverTensor : ((a >+< b) >< (p >< q)) =%> ((a >< p) >+< (b >< q))

Visibility: public export

rebracketcomptensor : ((e >@ y) >< y) =%> (e >@ (y >< y))

  Not an isomorphism, arising from duoidal structure between >@ and ><

Visibility: public export

distribute : (c >< e) =%> s -> (c >< (e >@ g)) =%> (s >@ g)

Visibility: public export

extractEffect : (d >< (e >@ f)) =%> (e >@ (d >< f))

Visibility: public export

swapMiddle : ((c1 >< c2) >< (c3 >< c4)) =%> ((c1 >< c3) >< (c2 >< c4))

Visibility: public export

Copy : c =%> (c >< c)

Visibility: public export

PairMaps : c =%> d -> c =%> e -> c =%> (d >< e)

Visibility: public export

Delete : c =%> Scalar

Visibility: public export

ProjLeft : (c >< d) =%> c

  Note that this doesn't exist for ordinary containers!

Visibility: public export

ProjRight : (c >< d) =%> d

Visibility: public export

Sum : {auto {conArg:18691} : Num a} -> (Const a >< Const a) =%> Const a

Visibility: public export

bwSumList : ComMonoid l => (xs : List l) -> l -> All (const l) xs

Visibility: public export

SumList : {auto {conArg:18791} : ComMonoid l} -> List (Const l) =%> Const l

Visibility: public export

Negate : {auto {conArg:18823} : Num a} -> Neg a => Const a =%> Const a

Visibility: public export

Zero : {auto {conArg:18863} : Num a} -> c =%> Const a

Visibility: public export

Mul : {auto {conArg:18896} : Num a} -> (Const a >< Const a) =%> Const a

Visibility: public export

SquaredDifference : {auto {conArg:18957} : Num a} -> Neg a => (Const a >< Const a) =%> Const a

  Mean squared error

Visibility: public export

selectShape : All .Shp cs -> Fin k -> Any .Shp cs

  Select a shape from All to produce an Any at the given index
  Same as `index i (allAnies shapes)` but reduces better

Visibility: public export

extractPos : (i : Fin n) -> AnyShpPos (selectShape shapes i) -> (index i xs) .Pos (index i shapes)

  Extract the position from an AnyPos at a given index

Visibility: public export

record FCoAlgCont : (Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor:

MkFCoAlgCont : (carrier : Cont) -> ((a : carrier .Shp) -> f (carrier .Pos a) -> carrier .Pos a) -> FCoAlgCont f

Projections:

.carrier : FCoAlgCont f -> Cont
.coalg : ({rec:0} : FCoAlgCont f) -> (a : (carrier {rec:0}) .Shp) -> f ((carrier {rec:0}) .Pos a) -> (carrier {rec:0}) .Pos a

.carrier : FCoAlgCont f -> Cont

Visibility: public export

carrier : FCoAlgCont f -> Cont

Visibility: public export

.coalg : ({rec:0} : FCoAlgCont f) -> (a : (carrier {rec:0}) .Shp) -> f ((carrier {rec:0}) .Pos a) -> (carrier {rec:0}) .Pos a

Visibility: public export

coalg : ({rec:0} : FCoAlgCont f) -> (a : (carrier {rec:0}) .Shp) -> f ((carrier {rec:0}) .Pos a) -> (carrier {rec:0}) .Pos a

Visibility: public export

coAlgMorphism : FCoAlgCont f -> FCoAlgCont f -> Type

Visibility: public export