Fix a set $𝑋$. The objects of the free monoidal category over $𝑋$, $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)$, are generated inductively by the elements of $𝑋$ and a unit element $𝐼$ over a binary operation $\otimes$. The morphisms are given by a quotient-inductive type. They are generated by associators, unitors, and identity over composition and parallel action over $\otimes$ then quotiented by associativity and composition equation to satisfy the category laws, equations constraining the associators/unitors to be natural isomorphisms, and pentagon/triangle equations to satiate the axioms of a monoidal category.