preservation of equality axioms by a monoidal functor 
[Dec. 20th, 201004:03 pm]
beroal

A year ago, I wrote (in Russian) on how a functor, preserving finite products, carries over algebraic operations and, more importantly, equational axioms. Therefore we can construct new algebraic structures from old ones without wasting our time on proving axioms in each case.
The general proof of preservation of axioms goes like this. If the interpretation of a term is built up from id, composition, projections, products of morphisms, and the functor preserves all of those, than interpretations of 2 terms in the carried over algebra are equal, provided that interpretations of those terms in the original algebra are equal.
There are interesting functors that preserve finite products not strictly, but up to an isomorphism. The functor brings a companion, an isomorphism, which also has its role to play. Intuitively, it does no harm, because isomorphic objects are “the same”.
There are lax monoidal functors that do not preserve finite products. E.g. Maybe is similar to NULL values in SQL. The covariant power set functor P is often used in mathematics. E.g. if we can sum 2 numbers, say ℤ numbers, we sum 2 sets of numbers by adding every element of the first set to every element of the second set, thus P carries over sum from ℤ to P ℤ . We sum ideals this way, for instance.
It seems we can apply previous reasoning to lax monoidal functors by mere generalizing finite products to monoidal structure. But a lax monoidal functor has another puzzling distinction: it has no isomorphism as a companion, just a plain morphism. I thought that isomorphism was necessary. If a functor can not preserve strictly, it should remain as strict as possible.
Here is an example in Haskell, where lax monoidal functors coincide with Applicative . The companion is a family of functions
liftA0 ()
liftA2 (,)
…
∀n∈ℕ. liftA${n} ${the data constructor of nary tuples}
Strictly speaking, we should, in addition, uncurry them. (Remark. liftA0 = pure .)
Neither base.Control.Monad nor base.Control.Applicative nor Wikipedia give them a particular name, so I will call them liftCon (lift a constructor).
Example of that companion not being an isomorphism:
uncurry (liftA2 (,)) :: (Maybe Bool, Maybe Bool) > Maybe (Bool, Bool)
Is not an isomorphism by the cardinality argument:
card (Maybe Bool × Maybe Bool) = (1+2)×(1+2) = 9
card (Maybe (Bool × Bool)) = 1+(2×2) = 5
In more deep, here is the graph of uncurry (liftA2 (,)) :
argument 
result 
(Nothing, Nothing) 
Nothing 
(Nothing, Just bv) 
Nothing 
(Just av, Nothing) 
Nothing 
(Just av, Just bv) 
Just (av, bv) 
Clearly Nothing has distinct preimages, then uncurry (liftA2 (,)) is not an injection, then it is not an isomorphism.
Back to preservation of axioms. There is no reason we need an isomorphism, which preservation is up to, though I did not work out proofs. We are speaking there about an isomorphism because that morphism become the isomorphism by its own means. Rigorously, if a functor preserves finite products up to some morphism f , f is an isomorphism.
Proof. F preserves finite products, then F preserves projections.
π_i = F π_i ∘ liftCon // the property of product
id = ⟨π_0, π_1⟩ = ⟨F π_0 ∘ liftCon, F π_1 ∘ liftCon⟩ // distributivity of the product of morphisms
= ⟨F π_0, F π_1⟩ ∘ liftCon
F preserves finite products, then F preserves the product of morphisms.
f_0:A→B_0 f_1:A→B_1 F ⟨f_0, f_1⟩ = liftCon ∘ ⟨F f_0, F f_1⟩ // assume f_0:=π_0, f_1:=π_1
F ⟨π_0, π_1⟩ = liftCon ∘ ⟨F π_0, F π_1⟩ // the property of product
= F id // the functor preserves id
= id
(liftCon, ⟨F π_0, F π_1⟩) is an isomorphism. Qed.
If we want axioms to be carried over, we should be able to interpret axioms, i.e. terms in them, in a monoidal category. A monoidal category in a sense is weaker than a category with finite products, i.e. not every term may be interpreted in a monoidal category and not every axiom is preserved.
E.g. the list functor does not preserve idempotence, as it does not preserve even the length of lists:
length (liftA2 (,) xs xs) == (length xs)^2 ≠ length xs It also does not preserve commutativity, in a trickier way:
$ let
xs = [1,2]
ys = [1,3]
in (liftA2 (+) xs ys, liftA2 (+) ys xs)
([2,4,3,5],[2,3,4,5])
As there are different species of monoidal categories, functors and axioms are classified accordingly. For an axiom to be preserved we need a category with a peculiar structure, a functor that preserves that structure, the axiom is interpretable by that structure. In a monoidal category we may interpret terms in which:
(the list of variables of the left term = the list of variables of the right term) and (every term contains no repetition of any variable) I.e. the order of variables should be the same in both terms. In a symmetric monoidal category we may interpret terms in which:
(the multiset of variables of the left term = the multiset of variables of the right term) and (every term contains no repetition of any variable) Beware that if you change “multiset” to “set”, you will not obtain the condition for a category with finite products. A category with finite products requires nothing.
Here is a handful of examples, at the first level there are kinds of category/functor, at the second level there are axioms:
 monoidal:
 symmetric monoidal:
 with finite products:
[Update 20110221. The axioms of a group is an interesting case. The axioms of inverse, i.e.
∀x.(x)+x=0 ∀x.x+(x)=0 are not symmetric monoidal. But their famous consequences, call them MI:
∀x y. (x+y)=(y)+(x) is symmetric monoidal,
∀x. (x)=x is monoidal. Therefore MI are preserved by the covariant powerset functor. It does not matter, is it an axiom or a theorem, as long as it is true.
Do not try to derive the axioms of inverse from MI. There is a counterexample ({0,1})+{0,1}={0,1}+{0,1}={1,0,1}≠{0}.] 

