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.

Totality: total
Visibility: public export
Constructor: 

(!%) : UC c1 =%> UC c2 -> c1 =%> c2

Projection: 

.ULens : c1 =%> c2 -> UC c1 =%> UC c2

Fixity Declarations:
infixr operator, level 1
infixr operator, level 1

.ULens : c1 =%> c2 -> UC c1 =%> UC c2

Visibility: public export

ULens : c1 =%> c2 -> UC c1 =%> UC c2

Visibility: public export

(!%+) : ((x : c1 .Shp) -> (y : c2 .Shp ** c2 .Pos y -> c1 .Pos x)) -> c1 =%> c2

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

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

(%!) : c1 =%> c2 -> (x : c1 .Shp) -> (y : c2 .Shp ** c2 .Pos y -> c1 .Pos x)

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

.fwd : c1 =%> c2 -> c1 .Shp -> c2 .Shp

Visibility: public export

.bwd : (f : c1 =%> c2) -> (x : c1 .Shp) -> c2 .Pos (f .fwd x) -> c1 .Pos x

Visibility: public export

compDepLens : c1 =%> c2 -> c2 =%> c3 -> c1 =%> c3

Visibility: public export

(%>>) : c1 =%> c2 -> c2 =%> c3 -> c1 =%> c3

Visibility: public export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5

id : c =%> c

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)
                   └─────────────┘

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

Totality: total
Visibility: public export
Constructor: 

(!&) : UC c1 =&> UC c2 -> c1 =&> c2

Projection: 

.UChart : c1 =&> c2 -> UC c1 =&> UC c2

Fixity Declarations:
infixr operator, level 1
infixr operator, level 1

.UChart : c1 =&> c2 -> UC c1 =&> UC c2

Visibility: public export

UChart : c1 =&> c2 -> UC c1 =&> UC c2

Visibility: public export

(&!) : c1 =&> c2 -> (x : c1 .Shp) -> (y : c2 .Shp ** c1 .Pos x -> c2 .Pos y)

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

.fwd : c1 =&> c2 -> c1 .Shp -> c2 .Shp

Visibility: public export

.bwd : (f : c1 =&> c2) -> (x : c1 .Shp) -> c1 .Pos x -> c2 .Pos (f .fwd x)

Visibility: public export

compDepChart : c1 =&> c2 -> c2 =&> c3 -> c1 =&> c3

Visibility: public export

(&>>) : c1 =&> c2 -> c2 =&> c3 -> c1 =&> c3

Visibility: public export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5

id : c =&> c

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.

Visibility: public export