Data.Container.Additive.Morphism.Definition

Definitions

record (=%+>) : AddCont -> AddCont -> Type

  Forward-backward morphism between additive containers
  Analogous to `=%>`, but with an added `+` in syntax to denote additivity
  It should also encode the constraint that the backward part is a
  commutative monoid homomorphism. That is currently left out.
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
                   │    lens     │
      c.Pos x   ◄──┤             ├◄── d.Pos y
                   └─────────────┘

Totality: total
Visibility: public export
Constructor: 

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

Projection: 

.ULens : c =%+> d -> UC c =%> UC d

Fixity Declaration: infixr operator, level 1

.ULens : c =%+> d -> UC c =%> UC d

Totality: total
Visibility: public export

ULens : c =%+> d -> UC c =%> UC d

Totality: total
Visibility: public export

(!%+) : ((x : c .Shp) -> (y : d .Shp ** d .PosSet y -> c .PosSet x)) -> c =%+> d

  Analogous to `!%` for ordinary containers, allows us to construct the 
  lens directly

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

(%!+) : c =%+> d -> (x : c .Shp) -> (y : d .Shp ** d .PosSet y -> c .PosSet x)

Totality: total
Visibility: public export

.fwd : c =%+> d -> c .Shp -> d .Shp

Totality: total
Visibility: public export

.bwd : (f : c =%+> d) -> (x : c .Shp) -> d .PosSet (f .fwd x) -> c .PosSet x

Totality: total
Visibility: public export

compDepLens : c =%+> d -> d =%+> e -> c =%+> e

Totality: total
Visibility: public export

(%+>>) : c =%+> d -> d =%+> e -> c =%+> e

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

id : c =%+> c

Totality: total
Visibility: public export

lensInputs : c =%+> d -> AddCont

  Pairing of all possible combinations of inputs to a particular lens
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             ├──►
                   │    lens     │
                ◄──┤             ├◄── d.Pos (lens.fwd x)
                   └─────────────┘

Totality: total
Visibility: public export

record (=&+>) : AddCont -> AddCont -> Type

  Forward-forward morphism between additive containers
  It should also encode the constraint that the second component of the
  chart is a commutative monoid homomorphism. That is currently left out
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
                   │    chart    │
      c.Pos x   ──►┤             ├──► d.Pos y
                   └─────────────┘

Totality: total
Visibility: public export
Constructor: 

(!&) : UC c =&> UC d -> c =&+> d

Projection: 

.UChart : c =&+> d -> UC c =&> UC d

Fixity Declaration: infixr operator, level 1

.UChart : c =&+> d -> UC c =&> UC d

Totality: total
Visibility: public export

UChart : c =&+> d -> UC c =&> UC d

Totality: total
Visibility: public export

(!&+) : ((x : c .Shp) -> (y : d .Shp ** c .PosSet x -> d .PosSet y)) -> c =&+> d

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

(&!+) : c =&+> d -> (x : c .Shp) -> (y : d .Shp ** c .PosSet x -> d .PosSet y)

Totality: total
Visibility: public export

.fwd : c =&+> d -> c .Shp -> d .Shp

Totality: total
Visibility: public export

.bwd : (f : c =&+> d) -> (x : c .Shp) -> c .PosSet x -> d .PosSet (f .fwd x)

Totality: total
Visibility: public export

compDepChart : c =&+> d -> d =&+> e -> c =&+> e

Totality: total
Visibility: public export

(&+>>) : c =&+> d -> d =&+> e -> c =&+> e

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

id : c =&+> c

Totality: total
Visibility: public export

chartInputs : (0 _ : c =&+> d) -> AddCont

  Unlike with lenses, the set of all inputs to a chart is simpler, it is 
  just the input container.

Totality: total
Visibility: public export

valuedIn : AddCont -> ComMonoid -> AddCont

  The dual of an additive container at some monoid `y`:
  same shapes, positions become homomorphisms into `y`
  On underlying containers this recoves `valuedIn`

Totality: total
Visibility: public export

dual : AddCont -> AddCont

  `dualTo` at the free object on 1

Totality: total
Visibility: public export

dualiseChart : c =&+> d -> valuedIn c y =%+> valuedIn d y

  Charts dualise to lenses: forward mode becomes reverse mode.

Totality: total
Visibility: public export