Data.Container.Additive.Morphism.Definition

Definitions

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

  Forward-backward morphism between additive containers
  It should also encode the constraint that the backward part is a comonoid
  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 Declarations:
infixr operator, level 1
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 .Pos y -> c .Pos 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 .Pos y -> c .Pos x)

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

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

Totality: total
Visibility: public export

.bwd : (f : c =%> d) -> (x : c .Shp) -> d .Pos (f .fwd x) -> c .Pos 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 Declarations:
infixl operator, level 5
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)
                   │    lens     │
      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 Declarations:
infixr operator, level 1
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

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

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

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

Totality: total
Visibility: public export

.bwd : (f : c =&> d) -> (x : c .Shp) -> c .Pos x -> d .Pos (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 Declarations:
infixl operator, level 5
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