Int Construction with Concategories

Int.idr

-- | Concategory
data Concat : List o -> List o -> Type where
  -- Identity
  Id : Concat as as
  -- Sequential composition
  Seq : Concat bs cs -> Concat as bs -> Concat as cs
  -- Par
  Par : {as, bs, cs, ds : List o} -> Concat as bs -> Concat cs ds -> Concat (as++cs) (bs++ds)
  -- Symmetry
  Sym : Concat (x ++ y) (y ++ x)
  -- Trace
  Trace : {as, bs, cs : List o} -> Concat (cs ++ as) (cs ++ bs) -> Concat as bs
  -- Permutation axiom, blah. 
  Perms : Concat ((as1 ++ bs2) ++ (cs1 ++ ds2)) ((as2 ++ bs1) ++ (cs2 ++ ds1)) -> Concat ((as1 ++ cs1) ++ (bs2 ++ ds2)) ((as2 ++ cs2) ++ (bs1 ++ ds1))

-- Concategory with involution
data InvCat : (List o, List o) -> (List o, List o) -> Type where
  IdI : InvCat (x, y) (x, y)
  SeqI : {x1,x2,y1,y2,z1,z2:List o} -> InvCat (x1, x2) (y1, y2) -> InvCat (y1, y2) (z1, z2) -> InvCat (x1, x2) (z1, z2)
  ParI : {as1, as2, bs1, bs2, cs1, cs2, ds1, ds2 : List o} -> InvCat (as1, as2) (bs1, bs2) -> InvCat (cs1, cs2) (ds1, ds2) -> 
    InvCat (as1++cs1, as2++cs2) (bs1++ds1, bs2++ds2)

-- Int(C) -> C == InvCat -> Concat 
evInt : InvCat (x1, y1) (x2, y2) -> Concat (x1 ++ y2) (y1 ++ x2) 
evInt IdI = Sym
evInt (ParI t1 t2) = Perms (Par (evInt t1) (evInt t2)) 
evInt (SeqI {y2, z2, y1} t1 t2) = ?zz