Data.Container.Base.Morphism.Definition

Definitions

data (=%>) : Cont -> Cont -> Type

  Dependent lenses
  Forward-backward container morphisms
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
                   │    lens     │
      c.Pos x   ◄──┤             ├◄── d.Pos y
                   └─────────────┘

Totality: total
Visibility: public export
Constructor: 

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

Fixity Declaration: infixr operator, level 1

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

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

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

  See fwd of `DChart`

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

  Composition of dependent lenses

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 -> Cont

  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

data (=&>) : Cont -> Cont -> Type

  Dependent charts
  Forward-forward container morphisms
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
                   │    lens     │
      c.Pos x   ──►┤             ├──► d.Pos y
                   └─────────────┘

Totality: total
Visibility: public export
Constructor: 

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

Fixity Declaration: infixr operator, level 1

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

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

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

  For some reason, this has to be a lambda for
  `Autodiff.Core.Forward.MkDiff` to reduce correctly

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 Declaration: infixl operator, level 5

id : c =&> c

Totality: total
Visibility: public export

data (=:>) : Cont -> Cont -> Type

  Cartesian morphisms
  Morphisms whose function on positions is an isomorphism
  There is a sense in which these are "linear" morphisms of containers

Totality: total
Visibility: public export
Constructor: 

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

Fixity Declaration: infixr operator, level 1

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

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

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

  Every cartesian morphism is a dependent lens

Totality: total
Visibility: public export

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

  Every cartesian morphism is a dependent chart

Totality: total
Visibility: public export

reduceVia : ((s' : d .Shp) -> d .Pos s') -> c =%> d -> (s : c .Shp) -> c .Pos s

Totality: total
Visibility: public export

valuedIn : Cont -> Type -> Cont

  Similar to the extension of a container. Following some ideas in
  Diegetic open games (https://arxiv.org/abs/2206.12338)
  Is this recovered via container composition when `r` is a some container?
  Probably something like `c >@ (Const Unit r) = valuedIn c r`?

Totality: total
Visibility: public export

chartToLens : c1 =&> c2 -> valuedIn c1 r =%> valuedIn c2 r

  Chart -> DLens
  Tangent bundle to Contanget bundle, effectively

Totality: total
Visibility: public export