Cartesian.idr

Cartesian Container Morphisms

Cartesian container morphisms come from Abbott (do they?) where the name was given by the fact that the something something cartesian morphisms pullbacks.

In the programming practice, this means that the backward map of lenses is an isomorphism rather than a one-way morphism. All the naming conventions for cartesian morphisms will make use of a # symbol, as a symbol reminiscent of a the geometrical representation of the cartesian plane. While there is no direct relation between the two, I thought it would make for a helpful mnemonic.

record (=#>) (0 a, b : Container) where
  constructor MkCartDepLens
  -- `c` for cartesian forward map
  cfwd : a.req -> b.req
  -- `c` for cartesian backward map
  cbwd : (x : a.req) -> b.res (cfwd x) ≅ a.res x

Next, we should also make sure that our definition of cartesian container forms a category, for this we define identity and composition.

(|#>) : {0 a, b, c : Container} -> a =#> b -> b =#> c -> a =#> c
(|#>) m1 m2 =
  let f1 : a.req -> b.req
      f1 = m1.cfwd
      b1 : (x : a.req) -> b.res (f1 x) ≅ a.res x
      b1 = m1.cbwd
      f2 : b.req -> c.req
      f2 = m2.cfwd
      b2 : (x : b.req) -> c.res (f2 x) ≅ b.res x
      b2 = m2.cbwd
  in MkCartDepLens (f2 . f1)
    (\x => transIso (b2 (f1 x)) (b1 x))

identity : (0 v : Container) -> v =#> v
identity v = MkCartDepLens id (\x => Iso.identity (v.res x))