Data.Container.Additive.Morphism.Instances

(source)

Definitions

pushIntoContinuation : (d >*< p) =%+> l -> p =%+> (Nap (d .Shp) >-+@ l)

Totality: total
Visibility: public export

terminal : c =%+> UnitCont

Totality: total
Visibility: public export

leftUnit : (UnitCont >*< c) =%+> c

Totality: total
Visibility: public export

rightUnit : (c >*< UnitCont) =%+> c

Totality: total
Visibility: public export

leftUnitInv : c =%+> (UnitCont >*< c)

Totality: total
Visibility: public export

rightUnitInv : c =%+> (c >*< UnitCont)

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

copy : c =%+> (c >*< c)

  These do not exist for ordinary containers!
  Here we need `c` not to be erased since we're using its monoid structure

Totality: total
Visibility: public export

pairMaps : c =%+> d -> c =%+> e -> c =%+> (d >*< e)

Totality: total
Visibility: public export

materialiseCont : Materialise (c .Shp) => InterfaceOnPositions c Materialise => c =%+> c

  Materialises both the forward pass and the backward pass

Totality: total
Visibility: public export

constPair : {auto {conArg:12852} : ComMonoid s} -> {auto {conArg:12855} : ComMonoid t} -> Const (s, t) =%+> (Const s >*< Const t)

  Generally used for pairing up parameters

Totality: total
Visibility: public export

constFinite : {ps : Fin n -> Type} -> (ms : ((i : Fin n) -> ComMonoid (ps i))) -> Const ((Product (\i => Const (ps i))) .Shp) =%+> Product (\i => Const (ps i))

  The n-ary `constPair`

Totality: total
Visibility: public export

projFinite : (i : Fin n) -> Product f =%+> f i

  Projection out of an iterated product; backward is the coprojection

Totality: total
Visibility: public export

projLeft : (c >*< d) =%+> c

Totality: total
Visibility: public export

projRight : (c >*< d) =%+> d

Totality: total
Visibility: public export

Maybe : c =%+> d -> Maybe c =%+> Maybe d

  The action of the `Maybe` functor on lenses

Totality: total
Visibility: public export

fanOut : ((i : ix) -> c =%+> f i) -> c =%+> Section f

Totality: total
Visibility: public export

mapSection : ((i : ix) -> a i =%+> b i) -> Section a =%+> Section b

  The action of `Section` on a family of lenses

Totality: total
Visibility: public export

sectionStrength : (Section g >*< p) =%+> Section (\i => g i >*< p)

Totality: total
Visibility: public export

generators : (s : ((i : Fin n) -> (f i) .Shp)) -> (Product f) .PosSet (tabulateShp s) -> List (i : Fin n ** (f i) .PosSet (s i))

Totality: total
Visibility: public export

evalAll : Section f =%+> Product f

  Evaluate a section over `Fin n` at every index

Totality: total
Visibility: public export

copair : ((i : ix) -> c i =%+> d) -> AddContDPair c =%+> d

  The universal map out of a dependent pair

Totality: total
Visibility: public export

evalSection : (Section a >*< AddContDPair p) =%+> AddContDPair (\i => a i >*< p i)

  Evaluate a section at the index an indexed value carries and pair it with
  that value

Totality: total
Visibility: public export

graph : Section f =%+> (Nap x >-+@ AddContDPair f)

  The graph of a section, implemented through effects

Totality: total
Visibility: public export

matchIndex : DecEq a => (AddContDPair b >*< AddContDPair l) =%+> Maybe (AddContDPair (\i => b i >*< l i))

  A lens from two dependent pairs into one. When they agree
  on the index they're paired, when they don't we return failure

Totality: total
Visibility: public export

unitor : c =%+> (Scalar >-+@ c)

  Backwards pass is ComMon-homomorphism on the nose

Totality: total
Visibility: public export

unitorInv : (Scalar >-+@ c) =%+> c

  Backwards map is a ComMon-homomorphism only through the quotient

Totality: total
Visibility: public export

multiplicator : (m >-+@ (n >-+@ c)) =%+> ((m >@ n) >-+@ c)

Totality: total
Visibility: public export

multiplicatorInv : ((m >@ n) >-+@ c) =%+> (m >-+@ (n >-+@ c))

Totality: total
Visibility: public export

actionToFree : (e >-+@ Scalar) =%+> (!*) e

  Read each position as the generator it is, with multiplicity one

Totality: total
Visibility: public export

freeToAction : (!*) e =%+> (e >-+@ Scalar)

  Expand each generator into as many copies as its multiplicity says.

Totality: total
Visibility: public export

adjR : UC c =%> m -> c =%+> (m >-+@ Scalar)

  Hom-set isomorphism of the adjunction, which is the general purpose
  `addContTranspose` read through the isomorphism above

Totality: total
Visibility: public export

adjL : c =%+> (m >-+@ Scalar) -> UC c =%> m

  Inverse of the hom-set isomorphism of the adjunction

Totality: total
Visibility: public export

epsilon : UC Scalar =%> Scalar

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

associator : ((a >+@ b) >+@ c) =%+> (a >+@ (b >+@ c))

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

duoidal : ((m >-+@ d) >*< (n >-+@ g)) =%+> ((m >< n) >-+@ (d >*< g))

  Lax interchange between the categorical product `>*<` on AddCont and the
  action `>-+@` of `(Cont, ><)` on it. Not an isomorphism.

Totality: total
Visibility: public export

distribute : (c .Shp -> e =%> s) -> (c >*< (e >-+@ g)) =%+> (s >-+@ g)

  Specific distributive law we need

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

State : AddCont -> Type

  State here differers for the one in `Cont`, because `Scalar` is different
  
        ┌─────────────┐
        │             ├──► (x : c.Shp)
        │    State    │
        │             ├◄── c.Pos x
        └─────────────┘

Totality: total
Visibility: public export

toState : c .Shp -> State c

Totality: total
Visibility: public export

Costate : AddCont -> Type

  Costate here differs from the one in `Cont`, because `Scalar` is different
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             │
                   │   Costate   │
      c.Pos x   ◄──┤             │
                   └─────────────┘

Totality: total
Visibility: public export

toCostate : ((x : c .Shp) -> c .PosSet x) -> Costate c

Totality: total
Visibility: public export

constantOne : InterfaceOnPositions c Num => Costate c

Totality: total
Visibility: public export

Delete : Costate c

Totality: total
Visibility: public export

sum : {auto {conArg:14935} : Num a} -> (Const a >*< Const a) =%+> Const a

Totality: total
Visibility: public export

bwSumBag : (xs : List l) -> l -> All (const l) xs

Totality: total
Visibility: public export

sumBag : {auto {conArg:15023} : ComMonoid l} -> BagAll (Const l) =%+> Const l

Totality: total
Visibility: public export

negate : {auto {conArg:15065} : Num a} -> Neg a => Const a =%+> Const a

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

zero : {auto {conArg:15103} : Num a} -> c =%+> Const a

Totality: total
Visibility: public export

mul : {auto {conArg:15135} : Num a} -> (Const a >*< Const a) =%+> Const a

Totality: total
Visibility: public export

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

  Mean squared error

Totality: total
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

Totality: total
Visibility: public export

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

  Extract the position from an AnyPos at a given index

Totality: total
Visibility: public export