Data.Container.Base.Morphism.Definition

Definitions

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

  Dependent lenses
  Forward-backward container morphisms

Totality: total
Visibility: public export
Constructor: 

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

Fixity Declaration: infixr operator, level 1

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

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

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

  See fwd of `DChart`

Visibility: public export

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

Visibility: public export

compDepLens : a =%> b -> b =%> c -> a =%> c

  Composition of dependent lenses

Visibility: public export

(%>>) : a =%> b -> b =%> c -> a =%> c

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

id : a =%> a

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

Visibility: public export

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

  Dependent charts
  Forward-forward container morphisms

Totality: total
Visibility: public export
Constructor: 

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

Fixity Declaration: infixr operator, level 1

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

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

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

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

Visibility: public export

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

Visibility: public export

compDepChart : a =&> b -> b =&> c -> a =&> c

Visibility: public export

(&>>) : a =&> b -> b =&> c -> a =&> c

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

id : a =&> a

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 : c1 .Shp) -> (y : c2 .Shp ** Iso (c1 .Pos x) (c2 .Pos y))) -> c1 =:> c2

Fixity Declaration: infixr operator, level 1

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

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

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

  Every cartesian morphism is a dependent lens

Visibility: public export

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

  Every cartesian morphism is a dependent chart

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`?

Visibility: public export

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

  Chart -> DLens
  Tangent bundle to Contanget bundle, effectively

Visibility: public export