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