From monoid to monoidal tricategory

MonoidalTricategory.idr

infixr 5 +++
infixr 5 ***

-- A list over a type
-- data List : Type -> Type where 
--   Nil : List a 
--   (::) : a -> List a -> List a 

Graph : Type -> Type 
Graph obj = obj -> obj -> Type 

-- A list of edges composed in parallel
data Parallel : Graph (List obj) where
  -- Empty list of edges
  None : Parallel [] []
  -- Add a single edge to the list 
  (:::) : {g : Graph obj} -> g a b -> Parallel as bs -> Parallel (a::as) (b::bs)
  -- Compose two lists of edges together
  (***) : Parallel as1 bs1 -> Parallel as2 bs2 -> Parallel (as1 ++ as2) (bs1 ++ bs2)

namespace Cat 
  -- A category over a graph, ie a list of sequentially composed edges
  public export
  data Path : Graph obj where
    -- Identity 
    Id : {a : obj} -> Path a a
    -- Sequentially add an edge to the path
    (::) : {g : Graph obj} -> {a, b, c : obj} -> g b c -> Path a b -> Path a c
    -- Sequential composition of two paths 
    (+++) : {a, b, c : obj} -> Path b c -> Path a b -> Path a c
    -- We can't define parallel composition yet, we need a bit more structure

namespace Monoidal 
  -- Monoidal category over a graph between lists of objects 
  data MonCat : Graph (List obj) where 
    -- These rules stay the same
    Id : {as : List obj} -> MonCat as as
    (::) : {g : Graph (List obj)} -> {a, b, c : List obj} -> g b c -> MonCat a b -> MonCat a c
    (+++) : {a, b, c : List obj} -> MonCat b c -> MonCat a b -> MonCat a c
    -- Compose two edges in parallel, this uses the append operation on the underlying lists
    Par : {l1, r1, l2, r2 : List obj} -> MonCat l1 r1 -> MonCat l2 r2 -> MonCat (l1 ++ l2) (r1 ++ r2)

namespace PreBicat 
  -- A 'bicategory' with no vertical composition. Essentially just a path of 2d-edges between edges
  data Path2 : Graph (Graph obj) where
    -- These rules are the same as Path
    Id : Path2 e e
    HComp : Path2 g h -> Path2 f g -> Path2 f h 
    -- We don't have enough structure to define vertical composition, or parallel composition

namespace BiCat
  -- A bicategory over a category, ie a 2-category of paths between paths
  data BiCat : Graph (Path a b) where
    -- These rules stay the same
    Id : BiCat e e
    HComp : BiCat g h -> BiCat f g -> BiCat f h 
    -- Vertical Composition, uses the sequential composition of the underlying paths
    VComp : {l1, r1 : Path b c} -> {l2, r2 : Path a b} -> 
      BiCat l1 r1 -> BiCat l2 r2 -> BiCat (l1 +++ l2) (r1 +++ r2)
    -- We still can't define parallel composition

namespace MonPreBiCat 
  -- A monoidal pre-bicategory. A 2-monoidal category between parallel edges
  data MonPreBiCat : Graph (Parallel as bs) where
    -- These rules stay the same
    Id : MonPreBiCat e e
    HComp : MonPreBiCat g h -> MonPreBiCat f g -> MonPreBiCat f h 
    -- Parallel Composition, uses the parallel composition of edges
    Par : {l1, r1 : Parallel as bs} -> {l2, r2 : Parallel cs ds} -> 
      MonPreBiCat l1 r1 -> MonPreBiCat l2 r2 -> MonPreBiCat (l1 *** l2) (r1 *** r2)
    -- We've lost vertical composition

namespace MonBiCat 
  -- A monoidal bicategory. A 2-monoidal category between monoidal categories
  -- We're indexing by both Path and Parallel, in other words by MonCat
  data MonBiCat : Graph (MonCat as bs) where
    -- These rules stay the same
    Id : MonBiCat e e
    HComp : MonBiCat g h -> MonBiCat f g -> MonBiCat f h 
    -- Vertical Composition, uses the sequential composition of the monoidal category
    VComp : {l1, r1 : MonCat bs cs} -> {l2, r2 : MonCat as bs} -> 
      MonBiCat l1 r1 -> MonBiCat l2 r2 -> MonBiCat (l1 +++ l2) (r1 +++ r2)
    -- Parallel Composition, uses the parallel of the monoidal category
    Par : {l1, r1 : MonCat as bs} -> {l2, r2 : MonCat cs ds} -> 
      MonBiCat l1 r1 -> MonBiCat l2 r2 -> MonBiCat (l1 *** l2) (r1 *** r2)

namespace PreTriCat 
  -- Pre-tricategory. A path of 3d edges between 2d edges
  data Path3 : Graph (Graph (Graph obj)) where 
    Id : Path3 e e
    HComp : Path3 g h -> Path3 f g -> Path3 f h 

namespace TriCat 
  -- Tricategory. A 3-category over a bicategory
  data TriCat : Graph (BiCat f g) where
    -- Id stays the same
    Id : TriCat e e
    -- X-composition is just horizontal composition
    XComp : TriCat g h -> TriCat f g -> TriCat f h 
    -- Y-composition uses the sequential composition of the underlying bicategory
    YComp : {l1, r1 : BiCat b c} -> {l2, r2 : BiCat a b} -> 
      TriCat l1 r1 -> TriCat l2 r2 -> TriCat (HComp l1 l2) (HComp r1 r2)
    -- Z-composition uses the vertical composition of the underlying bicategory
    ZComp : {l1, r1 : BiCat b c} -> {l2, r2 : BiCat a b} -> 
      TriCat l1 r1 -> TriCat l2 r2 -> TriCat (VComp l1 l2) (VComp r1 r2)

namespace MonTriCat 
  -- Monoidal tricategory over a monoidal bicategory
  data MonTriCat : Graph (MonBiCat m n) where 
    -- Id stays the same
    Id : MonTriCat e e
    -- X-composition is just horizontal composition
    XComp : MonTriCat g h -> MonTriCat f g -> MonTriCat f h 
    -- Y-composition uses the sequential composition of the underlying bicategory
    YComp : {l1, r1 : MonBiCat b c} -> {l2, r2 : MonBiCat a b} -> 
      MonTriCat l1 r1 -> MonTriCat l2 r2 -> MonTriCat (HComp l1 l2) (HComp r1 r2)
    -- Z-composition uses the vertical composition of the underlying bicategory
    ZComp : {l1, r1 : MonBiCat b c} -> {l2, r2 : MonBiCat a b} -> 
      MonTriCat l1 r1 -> MonTriCat l2 r2 -> MonTriCat (VComp l1 l2) (VComp r1 r2)
    -- Parallel composition uses parallel composition of the underlying bicategory
    Par : {l1, r1 : MonBiCat as bs} -> {l2, r2 : MonBiCat cs ds} -> 
      MonTriCat l1 r1 -> MonTriCat l2 r2 -> MonTriCat (Par l1 l2) (Par r1 r2)