SymmetricMonoidalCategoryNotCompiling

module SymmetricMonoidalCategoryNotCompiling

cong2 : {f : t -> u -> v} -> a = b -> c = d -> f a c = f b d
cong2 Refl Refl = Refl

record Category where
  constructor MkCategory
  obj           : Type
  mor           : obj -> obj -> Type
  identity      : (a : obj) -> mor a a
  compose       : (a, b, c : obj)
               -> (f : mor a b)
               -> (g : mor b c)
               -> mor a c
  leftIdentity  : (a, b : obj)
               -> (f : mor a b)
               -> compose a a b (identity a) f = f
  rightIdentity : (a, b : obj)
               -> (f : mor a b)
               -> compose a b b f (identity b) = f

record CFunctor (cat1 : Category) (cat2 : Category) where
  constructor MkCFunctor
  mapObj          : obj cat1 -> obj cat2
  mapMor          : (a, b : obj cat1)
                 -> mor cat1 a b
                 -> mor cat2 (mapObj a) (mapObj b)

record NaturalTransformation
  (cat1 : Category)
  (cat2 : Category)
  (fun1 : CFunctor cat1 cat2)
  (fun2 : CFunctor cat1 cat2)
  where
    constructor MkNaturalTranformation
    component : (a : obj cat1) -> mor cat2 (mapObj fun1 a) (mapObj fun2 a)

record Isomorphism (cat : Category) (a : obj cat) (b : obj cat) (morphism : mor cat a b) where
  constructor MkIsomorphism
  Inverse: mor cat b a

record NaturalIsomorphism
  (cat1 : Category)
  (cat2 : Category)
  (fun1 : CFunctor cat1 cat2)
  (fun2 : CFunctor cat1 cat2)
where
  constructor MkNaturalIsomorphism
  natTrans : NaturalTransformation cat1 cat2 fun1 fun2

record ProductMorphism
  (cat1 : Category)
  (cat2 : Category)
  (a : (obj cat1, obj cat2))
  (b : (obj cat1, obj cat2))
  where
    constructor MkProductMorphism
    pi1 : mor cat1 (fst a) (fst b)
    pi2 : mor cat2 (snd a) (snd b)

productIdentity :
     (a : (obj cat1, obj cat2))
  -> ProductMorphism cat1 cat2 a a
productIdentity {cat1} {cat2} a = MkProductMorphism (identity cat1 (fst a)) (identity cat2 (snd a))

productCompose :
     (a, b, c : (obj cat1, obj cat2))
  -> (f : ProductMorphism cat1 cat2 a b)
  -> (g : ProductMorphism cat1 cat2 b c)
  -> ProductMorphism cat1 cat2 a c
productCompose {cat1} {cat2} a b c f g = MkProductMorphism
  (compose cat1 (fst a) (fst b) (fst c) (pi1 f) (pi1 g))
  (compose cat2 (snd a) (snd b) (snd c) (pi2 f) (pi2 g))

productLeftIdentity :
     (a, b : (obj cat1, obj cat2))
  -> (f : ProductMorphism cat1 cat2 a b)
  -> productCompose a a b (productIdentity a) f = f
productLeftIdentity {cat1} {cat2} a b (MkProductMorphism f1 f2)
  = cong2 {f = MkProductMorphism} (leftIdentity cat1 (fst a) (fst b) f1) (leftIdentity cat2 (snd a) (snd b) f2)

productRightIdentity :
     (a, b : (obj cat1, obj cat2))
  -> (f : ProductMorphism cat1 cat2 a b)
  -> productCompose a b b f (productIdentity b) = f
productRightIdentity {cat1} {cat2} a b (MkProductMorphism f1 f2)
  = cong2 {f = MkProductMorphism} (rightIdentity cat1 (fst a) (fst b) f1) (rightIdentity cat2 (snd a) (snd b) f2)

productCategory : (cat1, cat2 : Category) -> Category
productCategory cat1 cat2 = MkCategory
  (obj cat1, obj cat2)
  (ProductMorphism cat1 cat2)
  (productIdentity {cat1} {cat2})
  (productCompose {cat1} {cat2})
  (productLeftIdentity {cat1} {cat2})
  (productRightIdentity {cat1} {cat2})

postulate
functor3 : (cat : Category) -> CFunctor (productCategory cat (productCategory cat cat)) cat

Associator :
     (cat : Category)
  -> Type
Associator cat = NaturalIsomorphism (productCategory cat (productCategory cat cat))
                                    cat
                                    (functor3 cat)
                                    (functor3 cat)

data MonoidalCategory : Type where
  MkMonoidalCategory :
       (cat : Category)
    -> (associator : Associator cat)
    -> MonoidalCategory

AssociativityCoherence :
     (cat : Category)
  -> (associator : Associator cat)
  -> Type
AssociativityCoherence cat associator = ()

cat : MonoidalCategory -> Category
cat (MkMonoidalCategory innerCat _) = innerCat

associator : (mCat : MonoidalCategory) -> Associator (cat mCat)
associator (MkMonoidalCategory _ associator) = associator

data SymmetricMonoidalCategory : Type where
  MkSymmetricMonoidalCategory :
       (monoidalCategory : MonoidalCategory)
    -> AssociativityCoherence (cat monoidalCategory)
                              (associator monoidalCategory)
    -> SymmetricMonoidalCategory