Para.idr

The Para Construction

The para construction combines the power of the reader monad and graded monads

given a morphism $C(a,b)$ in a monoidal category $C$, we can build parameterised morphisms $a\times p\to b$ where $p$ is the parameter. When parameterised morphisms compose, the parameter of each morphism is then combined using the monoidal structure.

Given parameterised morphisms $a\times p\to b$ and $b\times q\to c$, their composition is a morphism $a\times (p\otimes q)\to c$

Because the notion of morphism is now graded by parameters, parameterised morphisms do not form a category, but they do form a bicategory.

ParaConstr : forall o. (cat : Category o) -> Monoidal cat -> Bicategory o
ParaConstr
  (MkCategory m i c idl idr ass)
  (MkMonoidal
    (MkFunctor combine combineMap combId combComp)
    _
    (MkNaturalIsomorphism _ phi _ _)
    _
    _
  ) =
  MkBiCat
    (\x, y => Σ o (\mx => combine (mx && x) `m` y) )
    (\x, y => MkCategory
        (one_cell x y)
        (\x => i x.π1) c
        (\_, _, _ => idl _ _ _)
        (\_, _, _ => idr _ _ _)
        (\a, b, c, d, f, g, h => ass _ _ _ _ _ _ _))
    (\_, _, _ => MkFunctor
      (\x => x.π2.π1 *@* x.π1.π1 ##
                    (phi.component (x.π2.π1 && (x.π1.π1 && _)) |@>
                    combineMap _ _ (i x.π2.π1 && x.π1.π2) |@>
                    x.π2.π2))
      (\f, g, h => combineMap _ _ (swap h))
      (\f => combId _)
      (\a, b, c, f, g => combComp _ _ _ _ _)
      )
 
    where
      0 (~@>) : o -> o -> Type
      (~@>) = m
      (*@*) : o -> o -> o
      (*@*) a b = combine (a && b)
 
      (|@>) : {a, b, c : o} -> m a b -> m b c -> m a c
      (|@>) = c
      0 one_cell : (a, b : o) ->
                   Σ o (\mx => mx *@* a ~@> b) ->
                   Σ o (\mx => mx *@* a ~@> b) -> Type
      one_cell a b m1 m2 = m1.π1 ~@> m2.π1

The Para Construction on Types

Because types are monoidal and have products we can build the para construction on types using the above definition.

setPara : Bicategory Type
setPara = ParaConstr Set SetMonoidal