diff --git a/src/Basic/Category.lidr b/src/Basic/Category.lidr
index fcedadb..bb1937c 100644
--- a/src/Basic/Category.lidr
+++ b/src/Basic/Category.lidr
@@ -36,7 +36,7 @@ Then, we implement the basic elements a category consists of.
 %
 < record Category where
 %
-A |record| in Idirs is just the product type of several values, which are called the fields of the record. It's a convenient syntax because Idris provides field access and update functions automatically for us. We add also the constructor |MkCategory| to be able to construct concrete values of type |Category|:
+A |record| in Idris is just the product type of several values, which are called the fields of the record. It's a convenient syntax because Idris provides field access and update functions automatically for us. We add also the constructor |MkCategory| to be able to construct concrete values of type |Category|:
 %
 %
 <   constructor MkCategory
diff --git a/src/Monoid/FreeMonoid.lidr b/src/Monoid/FreeMonoid.lidr
new file mode 100644
index 0000000..cf3a31d
--- /dev/null
+++ b/src/Monoid/FreeMonoid.lidr
@@ -0,0 +1,35 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Monoid.FreeMonoid
+>
+> import Data.Fin
+> import Interfaces.Verified
+> import Monoid.Monoid
+>
+> %access public export
+> %default total
+>
+> FreeMonoid : Type -> Monoid
+> FreeMonoid t = MkMonoid (List t) %implementation
+>
+> finSetToFreeMonoid : Nat -> Monoid
+> finSetToFreeMonoid n = FreeMonoid (Fin n)
diff --git a/src/MonoidalCategory/FreeMonoidalCategory.lidr b/src/MonoidalCategory/FreeMonoidalCategory.lidr
new file mode 100644
index 0000000..73fd6e4
--- /dev/null
+++ b/src/MonoidalCategory/FreeMonoidalCategory.lidr
@@ -0,0 +1,342 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module MonoidalCategory.FreeMonoidalCategory
+>
+> import Basic.Category
+> import Basic.Functor
+> import Basic.Isomorphism
+> import Basic.NaturalIsomorphism
+> import Basic.NaturalTransformation
+> import Data.List
+> import Monoid.FreeMonoid
+> import Monoid.Monoid
+> import MonoidalCategory.StrictMonoidalCategory
+> import MonoidalCategory.StrictSymmetricMonoidalCategory
+> import MonoidalCategory.SymmetricMonoidalCategoryHelpers
+> import Product.ProductCategory
+>
+> %access export -- we do not default to public so that we don't leak implementation details
+> %default total
+>
+> -- define privately the data type with its generators
+> private
+> data PreFreeMorphism :
+>      (t : Type)
+>   -> (generatingMorphisms : List (List t, List t))
+>   -> (domain : List t)
+>   -> (codomain : List t)
+>   -> Type
+> where
+>   MkIdFreeMorphism            : (x : List t) -> PreFreeMorphism t generatingMorphisms x x
+>   MkSymmetryFreeMorphism      : (x, y : List t) -> PreFreeMorphism t generatingMorphisms (x ++ y) (y ++ x)
+>   MkCompositionFreeMorphism   : PreFreeMorphism t generatingMorphisms a b
+>                              -> PreFreeMorphism t generatingMorphisms b c
+>                              -> PreFreeMorphism t generatingMorphisms a c
+>   MkJuxtapositionFreeMorphism : PreFreeMorphism t generatingMorphisms a b
+>                              -> PreFreeMorphism t generatingMorphisms c d
+>                              -> PreFreeMorphism t generatingMorphisms (a ++ c) (b ++ d)
+>   MkGeneratingFreeMorphism    : (e : (List t, List t))
+>                              -> Elem e generatingMorphisms
+>                              -> PreFreeMorphism t generatingMorphisms (Basics.fst e) (Basics.snd e)
+>
+> -- define the real data type which will represent the quotient
+> -- it gives no access to its constructors, so that we can limit the functions which are definable on it
+> FreeMorphism :
+>      (t : Type)
+>   -> (generatingMorphisms : List (List t, List t))
+>   -> (domain : List t)
+>   -> (codomain : List t)
+>   -> Type
+> FreeMorphism = PreFreeMorphism
+>
+> -- provide smart constructors to replicate the constructors of the non-quotiented version
+> idFreeMorphism : (x : List t) -> FreeMorphism t generatingMorphisms x x
+> idFreeMorphism = MkIdFreeMorphism
+>
+> symmetryFreeMorphism : (x, y : List t) -> FreeMorphism t generatingMorphisms (x ++ y) (y ++ x)
+> symmetryFreeMorphism = MkSymmetryFreeMorphism
+>
+> compositionFreeMorphism :
+>      FreeMorphism t generatingMorphisms a b
+>   -> FreeMorphism t generatingMorphisms b c
+>   -> FreeMorphism t generatingMorphisms a c
+> compositionFreeMorphism = MkCompositionFreeMorphism
+>
+> juxtapositionFreeMorphism :
+>      FreeMorphism t generatingMorphisms a b
+>   -> FreeMorphism t generatingMorphisms c d
+>   -> FreeMorphism t generatingMorphisms (a ++ c) (b ++ d)
+> juxtapositionFreeMorphism = MkJuxtapositionFreeMorphism
+>
+> generatingFreeMorphism :
+>      (e : (List t, List t))
+>   -> Elem e generatingMorphisms
+>   -> FreeMorphism t generatingMorphisms (Basics.fst e) (Basics.snd e)
+> generatingFreeMorphism = MkGeneratingFreeMorphism
+>
+> freeIdentity : (ts : List t) -> FreeMorphism t generatingMorphisms ts ts
+> freeIdentity = idFreeMorphism
+>
+> freeComposition :
+>      (as, bs, cs : List t)
+>   -> (fm1 : FreeMorphism t generatingMorphisms as bs)
+>   -> (fm2 : FreeMorphism t generatingMorphisms bs cs)
+>   -> FreeMorphism t generatingMorphisms as cs
+> freeComposition as bs cs fm1 fm2 = compositionFreeMorphism fm1 fm2
+>
+> postulate
+> freeLeftIdentity :
+>      (as, bs : List t)
+>   -> (fm : FreeMorphism t generatingMorphisms as bs)
+>   -> compositionFreeMorphism (freeIdentity as) fm = fm
+>
+> postulate
+> freeRightIdentity :
+>      (as, bs : List t)
+>   -> (fm : FreeMorphism t generatingMorphisms as bs)
+>   -> compositionFreeMorphism fm (freeIdentity bs) = fm
+>
+> postulate
+> freeAssociativity :
+>      (as, bs, cs, ds : List t)
+>   -> (fm1 : FreeMorphism t generatingMorphisms as bs)
+>   -> (fm2 : FreeMorphism t generatingMorphisms bs cs)
+>   -> (fm3 : FreeMorphism t generatingMorphisms cs ds)
+>   -> compositionFreeMorphism fm1 (compositionFreeMorphism fm2 fm3)
+>    = compositionFreeMorphism (compositionFreeMorphism fm1 fm2) fm3
+>
+> generateFreeCategory : (t : Type) -> List (List t, List t) -> Category
+> generateFreeCategory t generatingMorphisms =
+>   MkCategory
+>     (List t)
+>     (FreeMorphism t generatingMorphisms)
+>     freeIdentity
+>     freeComposition
+>     freeLeftIdentity
+>     freeRightIdentity
+>     freeAssociativity
+>
+> freeTensorObject : (List t, List t) -> List t
+> freeTensorObject pair = fst pair ++ snd pair
+>
+> freeTensorMorphism :
+>      (a, b : (List t, List t))
+>   -> ProductMorphism (generateFreeCategory t generatingMorphisms)
+>                      (generateFreeCategory t generatingMorphisms)
+>                      a b
+>   -> FreeMorphism t generatingMorphisms (fst a ++ snd a) (fst b ++ snd b)
+> freeTensorMorphism a b (MkProductMorphism f1 f2) = juxtapositionFreeMorphism f1 f2
+>
+> postulate
+> freeTensorPreserveId :
+>      (a : (List t, List t))
+>   -> freeTensorMorphism a a (MkProductMorphism (freeIdentity (fst a)) (freeIdentity (snd a)))
+>    = freeIdentity (freeTensorObject a)
+>
+> postulate
+> freeTensorPreserveCompose :
+>      (a, b, c : (List t, List t))
+>   -> (f : ProductMorphism (generateFreeCategory t generatingMorphisms)
+>                           (generateFreeCategory t generatingMorphisms)
+>                           a b)
+>   -> (g : ProductMorphism (generateFreeCategory t generatingMorphisms)
+>                           (generateFreeCategory t generatingMorphisms)
+>                           b c)
+>   -> freeTensorMorphism a c (productCompose a b c f g)
+>    = freeComposition (freeTensorObject a)
+>                      (freeTensorObject b)
+>                      (freeTensorObject c)
+>                      (freeTensorMorphism a b f)
+>                      (freeTensorMorphism b c g)
+>
+> freeTensor :
+>      (t : Type)
+>   -> (generatingMorphisms : List (List t, List t))
+>   -> CFunctor (productCategory (generateFreeCategory t generatingMorphisms)
+>                                (generateFreeCategory t generatingMorphisms))
+>               (generateFreeCategory t generatingMorphisms)
+> freeTensor t generatingMorphisms = MkCFunctor
+>   freeTensorObject
+>   freeTensorMorphism
+>   freeTensorPreserveId
+>   freeTensorPreserveCompose
+>
+> postulate
+> freeTensorAssociative :
+>      (a, b, c, d, e, f : List t)
+>   -> (g : FreeMorphism t generatingMorphisms a b)
+>   -> (h : FreeMorphism t generatingMorphisms c d)
+>   -> (k : FreeMorphism t generatingMorphisms e f)
+>   -> juxtapositionFreeMorphism g (juxtapositionFreeMorphism h k)
+>    = juxtapositionFreeMorphism (juxtapositionFreeMorphism g h) k
+>
+> generateFreeMonoidalCategory : (t : Type) -> List (List t, List t) -> StrictMonoidalCategory
+> generateFreeMonoidalCategory t generatingMorphisms = MkStrictMonoidalCategory
+>   (generateFreeCategory t generatingMorphisms)
+>   (freeTensor t generatingMorphisms)
+>   []
+>   (\a => Refl)
+>   appendNilRightNeutral
+>   appendAssociative
+>   freeTensorAssociative
+>
+> swapConcat : (x : (List t, List t)) -> snd x ++ fst x = fst (swap x) ++ snd (swap x)
+> swapConcat (x1, x2) = Refl
+>
+> postulate
+> freeTensorPreserveSwap :
+>      (a, b, c, d : List t)
+>   -> (f : FreeMorphism t generatingMorphisms a c)
+>   -> (g : FreeMorphism t generatingMorphisms b d)
+>   -> compositionFreeMorphism (symmetryFreeMorphism a b) (juxtapositionFreeMorphism g f)
+>    = compositionFreeMorphism (juxtapositionFreeMorphism f g) (symmetryFreeMorphism c d)
+>
+> private
+> freeSymmetryCommutativity :
+>      (a, b : (List t, List t))
+>   -> (f : ProductMorphism (generateFreeCategory t generatingMorphisms)
+>                           (generateFreeCategory t generatingMorphisms)
+>                           a b)
+>   -> let freeCat = (generateFreeCategory t generatingMorphisms)
+>      in  freeComposition (mapObj (freeTensor t generatingMorphisms) a)
+>                          (mapObj (functorComposition (productCategory freeCat freeCat)
+>                                                      (productCategory freeCat freeCat)
+>                                                      freeCat
+>                                                      (swapFunctor freeCat freeCat)
+>                                                      (freeTensor t generatingMorphisms))
+>                                  a)
+>                          (mapObj (functorComposition (productCategory freeCat freeCat)
+>                                                      (productCategory freeCat freeCat)
+>                                                      freeCat
+>                                                      (swapFunctor freeCat freeCat)
+>                                                      (freeTensor t generatingMorphisms))
+>                                  b)
+>                          (rewrite sym (swapConcat a) in symmetryFreeMorphism (fst a) (snd a))
+>                          (mapMor (functorComposition (productCategory freeCat freeCat)
+>                                                      (productCategory freeCat freeCat)
+>                                                      freeCat
+>                                                      (swapFunctor freeCat freeCat)
+>                                                      (freeTensor t generatingMorphisms))
+>                                  a b f)
+>    = freeComposition (mapObj (freeTensor t generatingMorphisms) a)
+>                      (mapObj (freeTensor t generatingMorphisms) b)
+>                      (mapObj (functorComposition (productCategory freeCat freeCat)
+>                                                  (productCategory freeCat freeCat)
+>                                                  freeCat
+>                                                  (swapFunctor freeCat freeCat)
+>                                                  (freeTensor t generatingMorphisms))
+>                              b)
+>                      (mapMor (freeTensor t generatingMorphisms) a b f)
+>                      (rewrite sym (swapConcat b) in symmetryFreeMorphism (fst b) (snd b))
+> freeSymmetryCommutativity (a1, a2) (b1, b2) (MkProductMorphism f1 f2) = freeTensorPreserveSwap a1 a2 b1 b2 f1 f2
+>
+> postulate
+> freeSymmetryIsInvolution :
+>      (a, b : List t)
+>   -> compositionFreeMorphism (symmetryFreeMorphism a b) (symmetryFreeMorphism b a)
+>    = idFreeMorphism (a ++ b)
+>
+> freeSymmetry :
+>      (t : Type)
+>   -> (generatingMorphisms : List (List t, List t))
+>   -> NaturalIsomorphism (productCategory (generateFreeCategory t generatingMorphisms)
+>                                          (generateFreeCategory t generatingMorphisms))
+>                         (generateFreeCategory t generatingMorphisms)
+>                         (freeTensor t generatingMorphisms)
+>                         (functorComposition (productCategory (generateFreeCategory t generatingMorphisms)
+>                                                              (generateFreeCategory t generatingMorphisms))
+>                                             (productCategory (generateFreeCategory t generatingMorphisms)
+>                                                              (generateFreeCategory t generatingMorphisms))
+>                                             (generateFreeCategory t generatingMorphisms)
+>                                             (swapFunctor (generateFreeCategory t generatingMorphisms)
+>                                                          (generateFreeCategory t generatingMorphisms))
+>                                             (freeTensor t generatingMorphisms))
+> freeSymmetry t generatingMorphisms = MkNaturalIsomorphism
+>   (MkNaturalTransformation (\a => rewrite sym (swapConcat a) in symmetryFreeMorphism (fst a) (snd a))
+>                            (\a, b, f => freeSymmetryCommutativity a b f))
+>   (\(a1, a2) => MkIsomorphism (symmetryFreeMorphism a2 a1)
+>                               (freeSymmetryIsInvolution a1 a2)
+>                               (freeSymmetryIsInvolution a2 a1))
+>
+> postulate
+> freeUnitCoherence :
+>      (a : List t)
+>   -> symmetryFreeMorphism a []
+>    = idFreeMorphism a
+>
+> postulate
+> freeAssociativityCoherence :
+>      (a, b, c : List t)
+>   -> symmetryFreeMorphism a (b ++ c)
+>    = compositionFreeMorphism (juxtapositionFreeMorphism (symmetryFreeMorphism a b) (idFreeMorphism c))
+>                              (rewrite__impl (\r => FreeMorphism t generatingMorphisms r ((b ++ c) ++ a))
+>                                             (sym (appendAssociative b a c))
+>                                             (rewrite__impl (\r => FreeMorphism t generatingMorphisms (b ++ a ++ c) r)
+>                                                            (sym (appendAssociative b c a))
+>                                                            (juxtapositionFreeMorphism (idFreeMorphism b)
+>                                                                                       (symmetryFreeMorphism a c))))
+>
+> generateFreeSymmetricMonoidalCategory : (t : Type) -> List (List t, List t) -> StrictSymmetricMonoidalCategory
+> generateFreeSymmetricMonoidalCategory t generatingMorphisms = MkStrictSymmetricMonoidalCategory
+>   (generateFreeMonoidalCategory t generatingMorphisms)
+>   (freeSymmetry t generatingMorphisms)
+>   (\a => freeUnitCoherence a)
+>   (\a, b, c => freeAssociativityCoherence a b c)
+>   (\a, b => freeSymmetryIsInvolution a b)
+>
+> foldOnMorphisms :
+>      {ssmc : StrictSymmetricMonoidalCategory}
+>   -> (onObj : List t -> obj (cat (smcat ssmc)))
+>   -> (onGeneratingMor :
+>           (f : (List t, List t))
+>        -> (Elem f generatingMorphisms)
+>        -> mor (cat (smcat ssmc)) (onObj $ fst f) (onObj $ snd f))
+>   -> (a, b : List t)
+>   -> mor (cat (smcat (generateFreeSymmetricMonoidalCategory t generatingMorphisms))) a b
+>   -> mor (cat (smcat ssmc)) (onObj a) (onObj b)
+> foldOnMorphisms {ssmc} onObj onGeneratingMor a a (MkIdFreeMorphism a) =
+>   identity (cat (smcat ssmc)) (onObj a)
+> foldOnMorphisms {ssmc} onObj onGeneratingMor (a ++ b) (b ++ a) (MkSymmetryFreeMorphism a b) =
+>   component (natTrans (symmetry ssmc)) (onObj a, onObj b)
+> foldOnMorphisms {ssmc} onObj onGeneratingMor a b (MkCompositionFreeMorphism g1 g2) =
+>   compose (cat (smcat ssmc)) _ _ _ g1 g2
+> foldOnMorphisms {ssmc} onObj onGeneratingMor (a ++ c) (b ++ d) (MkJuxtapositionFreeMorphism g1 g2) =
+>   mapMor (tensor (smcat ssmc)) _ _ (MkProductMorphism g1 g2)
+> foldOnMorphisms {ssmc} onObj onGeneratingMor (fst genMor) (snd genMor) (MkGeneratingFreeMorphism genMor prf) =
+>   onGeneratingMor genMor prf
+>
+> -- elimination rule for FreeMorphism
+> fold :
+>      {ssmc : StrictSymmetricMonoidalCategory}
+>   -> (onObj : List t -> obj (cat (smcat ssmc)))
+>   -> (onGeneratingMor :
+>           (f : (List t, List t))
+>        -> (Elem f generatingMorphisms)
+>        -> mor (cat (smcat ssmc)) (onObj $ fst f) (onObj $ snd f))
+>   -- TODO: this should really be a symmetric monoidal functor
+>   -> CFunctor (cat (smcat (generateFreeSymmetricMonoidalCategory t generatingMorphisms)))
+>               (cat (smcat ssmc))
+> fold {ssmc} onObj onGeneratingMor = MkCFunctor
+>   onObj
+>   (foldOnMorphisms {ssmc} onObj onGeneratingMor)
+>   (\a => ?preserveId)
+>   ?preserveComposition
diff --git a/src/MonoidalCategory/FreeQuotients.idr b/src/MonoidalCategory/FreeQuotients.idr
new file mode 100644
index 0000000..1272cbd
--- /dev/null
+++ b/src/MonoidalCategory/FreeQuotients.idr
@@ -0,0 +1,99 @@
+-- \iffalse
+-- SPDX-License-Identifier: AGPL-3.0-only
+
+-- This file is part of `idris-ct` Category Theory in Idris library.
+
+-- Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+-- This program is free software: you can redistribute it and/or modify
+-- it under the terms of the GNU Affero General Public License as published by
+-- the Free Software Foundation, either version 3 of the License, or
+-- (at your option) any later version.
+
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU Affero General Public License for more details.
+
+-- You should have received a copy of the GNU Affero General Public License
+-- along with this program.  If not, see <https://www.gnu.org/licenses/>.
+-- \fi
+
+module MonoidalCategory.FreeQuotients
+
+import Basic.Category
+import Basic.Functor
+import Basic.Isomorphism
+import Basic.NaturalIsomorphism
+import Basic.NaturalTransformation
+import Data.List
+import Monoid.FreeMonoid
+import Monoid.Monoid
+import MonoidalCategory.StrictMonoidalCategory
+import MonoidalCategory.StrictSymmetricMonoidalCategory
+import MonoidalCategory.SymmetricMonoidalCategoryHelpers
+import Product.ProductCategory
+import Quotient.Quotient
+import Quotient.UnsafeQuotient
+
+%access public export
+%default total
+
+parameters (t : Type, generatingMorphisms : List (List t, List t), extra : (List t -> List t -> Type) -> List t -> List t -> Type)
+
+  data PreFreeMorphism : List t -> List t -> Type where
+    MkIdFreeMorphism          : (x : List t) -> PreFreeMorphism x x
+    MkCompositionFreeMorphism : PreFreeMorphism a b
+                             -> PreFreeMorphism b c
+                             -> PreFreeMorphism a c
+    MkGeneratingFreeMorphism  : (e : (List t, List t))
+                             -> Elem e generatingMorphisms
+                             -> PreFreeMorphism (Basics.fst e) (Basics.snd e)
+    MkExtra                   : extra PreFreeMorphism a b -> PreFreeMorphism a b
+
+  data PreFreeMorphismEquality : (domain, codomain : List t) -> Rel (PreFreeMorphism domain codomain) where
+    LeftIdentityEq : (as, bs : List t)
+                  -> (fm : PreFreeMorphism as bs)
+                  -> PreFreeMorphismEquality as bs (MkCompositionFreeMorphism (MkIdFreeMorphism as) fm) fm
+    RightIdentityEq : (as, bs : List t)
+                  -> (fm : PreFreeMorphism as bs)
+                  -> PreFreeMorphismEquality as bs (MkCompositionFreeMorphism fm (MkIdFreeMorphism bs)) fm
+    AssociativeEq : (as, bs, cs, ds : List t)
+                 -> (fm1 : PreFreeMorphism as bs)
+                 -> (fm2 : PreFreeMorphism bs cs)
+                 -> (fm3 : PreFreeMorphism cs ds)
+                 -> PreFreeMorphismEquality as ds
+                                         (MkCompositionFreeMorphism fm1 (MkCompositionFreeMorphism fm2 fm3))
+                                         (MkCompositionFreeMorphism (MkCompositionFreeMorphism fm1 fm2) fm3)
+
+  FreeMorphism : (a, b : List t) -> Quotient' (PreFreeMorphism a b) (PreFreeMorphismEquality a b)
+  FreeMorphism a b = UnsafeQuotient' (PreFreeMorphism a b) (PreFreeMorphismEquality a b)
+
+parameters (t : Type, generatingMorphisms : List (List t, List t))
+
+  data PreFreeMonoidalMorphism : ((List t -> List t -> Type) -> List t -> List t -> Type) -> List t -> List t -> Type where
+    MkMonoidalFromFree          : PreFreeMorphism t generatingMorphisms extra a b -> PreFreeMonoidalMorphism extra a b
+    MkJuxtapositionFreeMorphism : PreFreeMonoidalMorphism extra a b
+                               -> PreFreeMonoidalMorphism extra c d
+                               -> PreFreeMonoidalMorphism extra (a ++ c) (b ++ d)
+    MkExtraMonoidal             : extra (PreFreeMonoidalMorphism extra) a b -> PreFreeMonoidalMorphism extra a b
+
+  IdFreeMonoidalMorphism : (x : List t) -> PreFreeMonoidalMorphism extra x x
+  IdFreeMonoidalMorphism x = MkMonoidalFromFree $ MkIdFreeMorphism _ _ _ x
+
+  data PreFreeMonoidalMorphismEquality : (extra : (List t -> List t -> Type) -> List t -> List t -> Type)
+                                      -> (domain, codomain : List t)
+                                      -> Rel (PreFreeMonoidalMorphism extra domain codomain) where
+    FreeTensorIdEq : (a, b : List t)
+                  -> PreFreeMonoidalMorphismEquality extra (a ++ b) (a ++ b)
+                       (MkJuxtapositionFreeMorphism (IdFreeMonoidalMorphism a) (IdFreeMonoidalMorphism b))
+                       (IdFreeMonoidalMorphism (a ++ b))
+
+-- parameters (t : Type, generatingMorphisms : List (List t, List t), extra : List t -> List t -> Type)
+
+--   data PreFreeSymmetricMonoidalMorphismExtra : List t -> List t -> Type where
+--     MkSymmetryFreeMorphism : (x, y : List t) -> PreFreeSymmetricMonoidalMorphismExtra (x ++ y) (y ++ x)
+--     MkExtraSymmetric       : extra a b -> PreFreeSymmetricMonoidalMorphismExtra a b
+
+--   PreFreeSymmetricMonoidalMorphism : List t -> List t -> Type
+--   PreFreeSymmetricMonoidalMorphism = PreFreeMonoidalMorphism t generatingMorphisms PreFreeSymmetricMonoidalMorphismExtra
diff --git a/src/MonoidalCategory/StrictMonoidalCategory.lidr b/src/MonoidalCategory/StrictMonoidalCategory.lidr
index 98edf13..02a7578 100644
--- a/src/MonoidalCategory/StrictMonoidalCategory.lidr
+++ b/src/MonoidalCategory/StrictMonoidalCategory.lidr
@@ -23,8 +23,12 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > import Basic.Category
 > import Basic.Functor
+> import Monoid.Monoid
 > import Product.ProductCategory
 >
+> -- contrib
+> import Interfaces.Verified
+>
 > %access public export
 > %default total
 >
@@ -49,3 +53,8 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                   (mapObj tensor (a,c), e)
 >                                   (mapObj tensor (b,d), f)
 >                                   (MkProductMorphism (mapMor tensor (a,c) (b,d) (MkProductMorphism g h)) k)
+>
+> smcObjectMonoid : StrictMonoidalCategory -> Monoid.Monoid
+> smcObjectMonoid smc = MkMonoid
+>   (obj (cat smc))
+>   ?asdf
diff --git a/src/MonoidalCategory/StrictSymmetricMonoidalCategory.lidr b/src/MonoidalCategory/StrictSymmetricMonoidalCategory.lidr
new file mode 100644
index 0000000..0fd2da6
--- /dev/null
+++ b/src/MonoidalCategory/StrictSymmetricMonoidalCategory.lidr
@@ -0,0 +1,118 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module MonoidalCategory.StrictSymmetricMonoidalCategory
+>
+> import Basic.Category
+> import Basic.Functor
+> import Basic.NaturalIsomorphism
+> import Basic.NaturalTransformation
+> import MonoidalCategory.StrictMonoidalCategory
+> import MonoidalCategory.SymmetricMonoidalCategoryHelpers
+> import Product.ProductCategory
+>
+> %access public export
+> %default total
+>
+> StrictUnitCoherence :
+>      (cat : Category)
+>   -> (unit : obj cat)
+>   -> (symmetry : NaturalIsomorphism (productCategory cat cat)
+>                                     cat
+>                                     tensor
+>                                     (functorComposition (productCategory cat cat)
+>                                                         (productCategory cat cat)
+>                                                         cat
+>                                                         (swapFunctor cat cat)
+>                                                         tensor))
+>   -> (a : obj cat)
+>   -> Type
+> StrictUnitCoherence cat unit symmetry a =
+>   (component (natTrans symmetry) (a, unit)) = identity cat a
+>
+> StrictAssociativityCoherence :
+>      (cat : Category)
+>   -> (tensor : CFunctor (productCategory cat cat) cat)
+>   -> (tensorIsAssociativeObj :
+>           (a, b, c : obj cat)
+>        -> mapObj tensor (a, mapObj tensor (b, c)) = mapObj tensor (mapObj tensor (a, b), c))
+>   -> (symmetry : NaturalIsomorphism (productCategory cat cat)
+>                                     cat
+>                                     tensor
+>                                     (functorComposition (productCategory cat cat)
+>                                                         (productCategory cat cat)
+>                                                         cat
+>                                                         (swapFunctor cat cat)
+>                                                         tensor))
+>   -> (a, b, c : obj cat)
+>   -> Type
+> StrictAssociativityCoherence cat tensor tensorIsAssociativeObj symmetry a b c =
+>   component (natTrans symmetry) (a, mapObj tensor (b, c)) =
+>   compose cat
+>           (mapObj tensor (mapObj tensor (a, b), c))
+>           (mapObj tensor (mapObj tensor (b, a), c))
+>           (mapObj tensor (mapObj tensor (b, c), a))
+>           (mapMor tensor
+>                   (mapObj tensor (a, b), c)
+>                   (mapObj tensor (b, a), c)
+>                   (MkProductMorphism (component (natTrans symmetry) (a, b)) (identity cat c)))
+>           (rewrite sym (tensorIsAssociativeObj b a c) in
+>            rewrite sym (tensorIsAssociativeObj b c a) in (mapMor tensor
+>                                                                  (b, (mapObj tensor (a, c)))
+>                                                                  (b, (mapObj tensor (c, a)))
+>                                                                  (MkProductMorphism (identity cat b)
+>                                                                                     (component (natTrans symmetry)
+>                                                                                                (a, c)))))
+>
+> data StrictSymmetricMonoidalCategory : Type where
+>   MkStrictSymmetricMonoidalCategory :
+>        (smcat : StrictMonoidalCategory)
+>     -> (symmetry : NaturalIsomorphism (productCategory (cat smcat) (cat smcat))
+>                                       (cat smcat)
+>                                       (tensor smcat)
+>                                       (functorComposition (productCategory (cat smcat) (cat smcat))
+>                                                           (productCategory (cat smcat) (cat smcat))
+>                                                           (cat smcat)
+>                                                           (swapFunctor (cat smcat) (cat smcat))
+>                                                           (tensor smcat)))
+>     -> ((a : obj (cat smcat)) -> StrictUnitCoherence (cat smcat) (unit smcat) symmetry a)
+>     -> ((a, b, c : obj (cat smcat)) -> StrictAssociativityCoherence (cat smcat)
+>                                                                     (tensor smcat)
+>                                                                     (tensorIsAssociativeObj smcat)
+>                                                                     symmetry
+>                                                                     a b c)
+>     -> ((a, b : obj (cat smcat)) -> InverseLaw (cat smcat) (tensor smcat) symmetry a b)
+>     -> StrictSymmetricMonoidalCategory
+>
+> smcat : StrictSymmetricMonoidalCategory -> StrictMonoidalCategory
+> smcat (MkStrictSymmetricMonoidalCategory smcat _ _ _ _) = smcat
+>
+> symmetry :
+>      (ssmc : StrictSymmetricMonoidalCategory)
+>   -> NaturalIsomorphism (productCategory (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                         (cat (smcat ssmc))
+>                         (tensor (smcat ssmc))
+>                         (functorComposition (productCategory (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                                             (productCategory (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                                             (cat (smcat ssmc))
+>                                             (swapFunctor (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                                             (tensor (smcat ssmc)))
+> symmetry (MkStrictSymmetricMonoidalCategory _ symmetry _ _ _) = symmetry
diff --git a/src/Quotient/Quotient.idr b/src/Quotient/Quotient.idr
new file mode 100644
index 0000000..17c186b
--- /dev/null
+++ b/src/Quotient/Quotient.idr
@@ -0,0 +1,69 @@
+module Quotient.Quotient
+
+import Control.Isomorphism
+
+%access public export
+%default total
+
+extEq : (a -> b) -> (a -> b) -> Type
+extEq {a} f g = (x : a) -> f x = g x
+
+Rel : Type -> Type
+Rel x = x -> x -> Type
+
+record EqRel (x : Type) where
+  constructor MkEqRel
+  rel : Rel x
+  refl : (a : x) -> rel a a
+  sym : (a, b : x) -> rel a b -> rel b a
+  trans : (a, b, c : x) -> rel a b -> rel b c -> rel a c
+
+parameters (rel : Rel x)
+  data EqClosure' : Rel x where
+    ClosureIncl : rel a b -> EqClosure' a b
+    ClosureRefl : EqClosure' a a
+    ClosureSym : EqClosure' a b -> EqClosure' b a
+    ClosureTrans : EqClosure' a b -> EqClosure' b c -> EqClosure' a c
+
+EqClosure : Rel x -> EqRel x
+EqClosure r = MkEqRel (EqClosure' r)
+                      (\a => ClosureRefl r)
+                      (\a, b, h => ClosureSym r h)
+                      (\a, b, c, h, h' => ClosureTrans r h h')
+
+RespectingMap : (x, y : Type) -> EqRel x -> Type
+RespectingMap x y eq = (f : (x -> y) ** ((a, b : x) -> (rel eq) a b -> f a = f b))
+
+record Quotient (x : Type) (eq : EqRel x) where
+  constructor MkQuotient
+  carrier : Type
+  proj : RespectingMap x carrier eq
+  exists : (y : Type) -> (f : RespectingMap x y eq)
+        -> (g : (carrier -> y) ** (extEq (fst f) (g . (fst proj))))
+  unique : (y : Type) -> (f : RespectingMap x y eq)
+        -> (g : (carrier -> y)) -> extEq (fst f) (g . (fst proj))
+        -> extEq g (fst (exists y f))
+
+Quotient' : (x : Type) -> Rel x -> Type
+Quotient' x eq = Quotient x (EqClosure eq)
+
+existsUnique : (q : Quotient x eq) -> (f : RespectingMap x y eq)
+            -> (g : carrier q -> y) -> (extEq (fst f) (g . (fst $ proj q)))
+            -> (h : carrier q -> y) -> (extEq (fst f) (h . (fst $ proj q)))
+            -> extEq g h
+existsUnique {y=y} (MkQuotient carrier proj exists unique) f g gh h hh x =
+  trans (unique y f g gh x) $ sym $ unique y f h hh x
+
+projectionInducesIdentity : (q : Quotient x eq) -> (f : carrier q -> carrier q) -> extEq (fst $ proj q) (f . (fst $ proj q)) -> extEq f Basics.id
+projectionInducesIdentity q f h x = sym $ existsUnique q (proj q) id (\a => Refl) f h x
+
+QuotientUnique : (q, q' : Quotient x eq)
+              -> (iso : Iso (carrier q) (carrier q') ** (extEq ((to iso) . (fst $ proj q)) (fst $ proj q')))
+QuotientUnique q q' = let
+                        (isoTo ** commTo) = exists q (carrier q') (proj q')
+                        (isoFrom ** commFrom) = exists q' (carrier q) (proj q)
+                        iso = MkIso isoTo isoFrom
+                                (projectionInducesIdentity q' (isoTo . isoFrom) (\a => trans (commTo a) (cong $ commFrom a)))
+                                (projectionInducesIdentity q (isoFrom . isoTo) (\a => trans (commFrom a) (cong $ commTo a)))
+                      in (iso ** (\a => sym $ commTo a))
+
diff --git a/src/Quotient/Quotients.idr b/src/Quotient/Quotients.idr
new file mode 100644
index 0000000..8571ac7
--- /dev/null
+++ b/src/Quotient/Quotients.idr
@@ -0,0 +1,24 @@
+module Quotient.Quotients
+
+import Quotient.Quotient
+
+%access public export
+%default total
+
+trivialEqRel : (x : Type) -> EqRel x
+trivialEqRel x = MkEqRel (\x, y => x = y) (\x => Refl) (\x, y, r => sym r) (\x, y, z, l, r => trans l r)
+
+trivialQuotient : (x : Type) -> Quotient x $ trivialEqRel x
+trivialQuotient x = MkQuotient x
+                      ((id {a=x}) ** (\a, b, h => h))
+                      (\y, f => ((fst f) ** (\a => Refl)))
+                      (\y, f, g, h, a => sym $ h a)
+
+fullEqRel : (x : Type) -> EqRel x
+fullEqRel x = MkEqRel (\x, y => ()) (\x => ()) (\x, y, r => ()) (\x, y, z, l, r => ())
+
+fullQuotient : (x : Type) -> (a : x) -> Quotient x $ fullEqRel x
+fullQuotient x a = MkQuotient ()
+                     ((\b => ()) ** (\a, b, h => Refl))
+                     (\y, f => ((\b => (fst f) a) ** (\b => snd f b a ())))
+                     (\y, f, g, h, () => sym $ h a)
diff --git a/src/Quotient/UnsafeQuotient.idr b/src/Quotient/UnsafeQuotient.idr
new file mode 100644
index 0000000..39fee7e
--- /dev/null
+++ b/src/Quotient/UnsafeQuotient.idr
@@ -0,0 +1,33 @@
+module Quotient.UnsafeQuotient
+
+import Quotient.Quotient
+
+%default total
+%access export
+
+private
+data InternalQuotientType : (x : Type) -> (eq : EqRel x) -> Type where
+  InternalWrap : x -> InternalQuotientType x eq
+
+QuotientType : (x : Type) -> (eq : EqRel x) -> Type
+QuotientType = InternalQuotientType
+
+Wrap : x -> QuotientType x eq
+Wrap = InternalWrap
+
+private
+unwrap : QuotientType x eq -> x
+unwrap (InternalWrap a) = a
+
+postulate
+QuotientEquality : (x : Type) -> (eq : EqRel x) -> (rel eq a b) -> Wrap a = Wrap b
+
+UnsafeQuotient : (x : Type) -> (eq : EqRel x) -> Quotient x eq
+UnsafeQuotient x eq = MkQuotient
+  (QuotientType x eq)
+  (Wrap ** (\a, b, h => QuotientEquality x eq h))
+  (\y, f => ((\a => fst f $ unwrap a) ** (\a => Refl)))
+  (\y, f, g, h, (InternalWrap a) => sym $ h a)
+
+UnsafeQuotient' : (x : Type) -> (eq : Rel x) -> Quotient' x eq
+UnsafeQuotient' x eq = UnsafeQuotient x (EqClosure eq)