Pattern runs on matter: The free monad monad as a module over the cofree comonad comonad
Sophie Libkind David I. Spivak


Identifying the ground state phases by spin-patterns in the Shastry-Sutherland model
    Hong-Gang Luo
    Received March XX, 2024; accepted XX XX, 2024
====================================================================================

plain


Interviews run on people, programs run on operating systems, voting schemes run on voters, games run on players. Each of these is an example of the abstraction pattern runs on matter. Pattern determines the decision tree that governs how a situation can unfold, while matter responds with decisions at each juncture. 

In this article, we will give a straightforward and concrete construction of the free monad monad for (, , ), the category of polynomial functors with the substitution monoidal product. 
Although the free monad has been well-studied in other contexts, the construction we give is streamlined and explicitly illustrates how the free monad represents terminating decision trees. We will also explore the naturally arising interaction between the free monad and cofree comonad. Again, while the interaction itself is known, the perspective we take is the free monad as a module over the cofree comonad. Lastly, we will give four applications of the module action to interviews, computer programs, voting, and games. In each example, we will see how the free monad represents pattern, the cofree comonad represents matter, and the module action represents runs on. 




§ INTRODUCTION




The etymology of matter and pattern are "mother" and "father"; this pair of terms offers a very basic sense in which to carve up the world. Like two parents, matter and pattern represent a fundamental dichotomy: matter is the pure material, unconcerned with our ideas about it; pattern is pure structure, unconcerned with what substantiates it. And yet one may have an intuitive sense that pattern "runs on"—must be instantiated in—matter. In this paper, we show that this idea matches both our intuition and the mathematics of a module structure by which free monads are a module over cofree comonads. 

Intuitively, interviews, programs, voting schemes, and games represent patterns. But what is an interview without a person to be interviewed; what is a program without a operating system to run it on; what is a voting scheme without voters to do the voting; what is a game without players to play it? In each case, the pattern runs on a material substrate.

In this paper we give an account for this intuition in terms of free monads  and cofree comonads  on polynomial functors. We show that for any p,q:, there is a natural map

    _p,q_p⊗_q→_p⊗ q.

In fact, this map gives  the structure of a -module, in a precise sense; see <ref>. 


Consider the behavior of a Moore machine, which transforms lists of A-inputs into lists of B-outputs for sets A,B. This behavior is determined by an element b→_B^A of the terminal coalgebra on the polynomial q B^A. But how does one apply this behavior to a list of A's? The latter is a map ℓ→_A. To actually apply the behavior b to the list ℓ, we use an obvious map φ A⊗ B^A→ B and the module structure (<ref>) to obtain a list of B's.

    ≅⊗ℓ⊗ b_A⊗_B^A_A,B^A_A⊗ B^A_φ_B


Whereas patterns start and end, matter is never destroyed. One can think of _p as the type of terminating programs and of _q as the type of operating systems or online algorithms. This intuition is captured by the fact that elements of the free monad _p are "well-founded trees" <cit.>—in the case p is finitary, a wellfounded tree is one with finite height—whereas elements of the cofree comonad _q are generally non-wellfounded, e.g. infinite in height even for finitary q. The module map _p,q pairs the wellfounded tree with the non-wellfounded tree, following the shape of the wellfounded one; for example the list of B's in (<ref>) will have exactly the same length as the list of A's. 




  
Related work.
A construction of the free monad for much more general (than polynomial) endofunctors was given by Kelly in <cit.>. The treatment was greatly simplified by Shulman and others in <cit.>. The case of polynomial endofunctors is more restrictive, and as such has a far more straightforward construction.

A monad-comonad interaction law, again in more general settings, was described in <cit.>. This paper structures interaction laws in an interesting and useful but somehow ad hoc way, as a category whose objects are triples (T,C,f), where T is a monad, C is a comonad, and f T⊗ C→𝕀 is a map satisfying certain natural conditions, and whose morphisms are maps T→ T' and C'→ C satisfying certain constraints. It should also be noted that this paper includes no proofs.



  
Contributions.


    
  * Simple concrete constructions of both free monads and cofree comonads in (, , ).
    
  * A proof that the free monad is a module over the cofree comonad.
    
  * Four applications of this module, each having the form pattern runs on matter.

For these, see <ref>; <ref>; and <ref>, respectively. We also give a precise definition of the notion of "dual" functor, defined in <cit.>, and generalize it to be functorial in a monad t; see (<ref>).



  
Notation.

We often denote the identity on an object x by the object name itself rather than 𝕀_x. We denote the cardinality of a set X by #X. 



If L⊣ R is an adjunction, we denote it

    CLRD

so that the 2-cell shown indicates the direction of both the unit C→ R ∘ L and the counit L ∘ R →D.



  
Acknowledgements.
The authors thanks Harrison Grodin and Brandon Shapiro for many useful conversations.
This material is based upon work supported by the Air Force Office of Scientific Research under award numbers FA9550-20-1-0348 and FA9550-23-1-0376.




 §.§ Preliminaries


Although we will assume basic familiarity with the category  of univariate polynomial functors on  and natural transformations between them, we will begin by clarifying notation. We write a polynomial functor p: as p = ∑_P: p(1)^p[P] where p(1) are the positions of p and p[P] are the directions at the position P. With this notation, a map ϕ: p → q in  consists of 

    
  * A function on positions ϕ(1): p(1) → q(1).
    
  * For each position P: p(1), a function backwards on directions ϕ^#_P: q[ϕ_1(P)] → p[P].

There are many monoidal products in  <cit.>, however in this article we focus on the Dirichlet and substitution products. 








The substitution product has unit  and is defined by

    p  q = ∑_P: p(1)∏_p[P]∑_Q:q(1)∏_q[Q]

Using the distributive law, a position in p  q is a position P in p and for every direction in p[P] a position in q.
It will be useful to consider the corolla forest view on polynomials and the -monoidal product, since these will be the building blocks of the decision trees represented by the free monad monad. 

Consider p = ^3 + ^2. We can notate p using a corolla forest in which each position P:p(1) is a tree with p[P]-many branches. The root of each tree is labeled by its corresponding position and  branches correspond to  directions.

    [trees,red, 
      level 1/.style=sibling distance=5mm,
      level 2/.style=sibling distance=2.5mm,
      level 3/.style=sibling distance=1.25mm]
    	 (a) 1
        	child node  
        	child node 
        	child node 
    		;
            [right = of a] (b) 2
    		  child node 
    		  child node 
    		;

Likewise, the polynomial q = 2^4 + ^2 + 1 is notated by the corolla forest:

    [trees,blue, 
      level 1/.style=sibling distance=5mm,
      level 2/.style=sibling distance=2.5mm,
      level 3/.style=sibling distance=1.25mm]
    	 (a) 1
        	child node 
        	child node 
                child node 
                child node 
    		;
            [right = 0.75in of a] (b) 2
    		  child node 
    		  child node 
                child node 
                child node 
    		;
            [right = 0.75in of b] (c) 3
        	child node 
        	child node 
    		;
            [right = 0.75in of c] (d) 4
    		;




Then the positions of p q can be represented by trees of height 2, whose building blocks are the trees corresponding to the positions of p and q. In particular, a position of p  q is a position of p and for each branch, a position of q. The directions are the number of dangling leaves. Here are three examples of positions in p  q with eight, eight, and two directions respectively.


    [trees,red, 
      level 1/.style=sibling distance=10mm,
      level 2/.style=sibling distance=3mm,
      level 3/.style=sibling distance=1.25mm]
    	[red] (a) 1
        	child[red] node[blue] 1
                        child[blue]
                        child[blue]
                        child[blue]
                        child[blue]
                
                child[red] node[blue] 3
                    child[blue]
                    child[blue]
                
                child[red] node[blue] 3
                    child[blue]
                    child[blue]
                
            ;
    
            [red, right = 1.5in of a] (b) 1
        	child[red] node[blue] 1
                    child[blue]
                    child[blue]
                    child[blue]
                    child[blue]
                
                child[red] node[blue] 4
                child[red] node[blue] 2
                    child[blue]
                    child[blue]
                    child[blue]
                    child[blue]
                
            ;
            [red, right = 1.5in of b] (c) 2
        	child[red] node[blue] 3
                    child[blue]
                    child[blue]
                
                child[red] node[blue] 4
            ;







§ THE FREE MONAD MONAD

For a polynomial p, we will define the free monad _p through transfinite induction by defining polynomials pα for each ordinal α and inclusions pα→ p β for ordinals α < β.

    
  * Base case:  Define p0.
    
  * For successor ordinals α+1: Define pα + 1 + p  pα. For the inclusions define ι0: → + p to be the inclusion; note that it is cartesian. Then, given ια, define ια + 1 to be
    
    pα+1 =  + p  p α + p  p α +1 = p α + 2.

    which is also cartesian.
    
  * For limit ordinals α: Define p α_α' < α pα'.  For each α' < α, let ια' pα'→ pα be the natural inclusion. These are cartesian by <ref>. Lastly, we define the inclusion ια p α→ p α + 1 to be induced by the cocone of maps which are defined for α' < α by
    
    pα' p α' + 1 =  + p  p α' + p  pα = pα + 1.




    By construction each ια is cartesian. 


For ease of notation, we will also use ια pα→ p β to represent the composite of inclusions for any pair of ordinals α < β.   
We will also define λα p  pα→ p α+1 to be the coproduct inclusion.



    If p is κ-small, then define _p  pκ. 


We will show in <ref> that _p is the free monad on p. Therefore, _p is unique and hence well-defined.

Think of the positions of _p as decision trees whose building blocks are the positions of p. For instance, suppose that a position P: p(1) is a question and the directions p[P] are possible answers to question P. Then   is a unique question with a unique answer, which we think of as "no further questions". Then, consider the positions of _p that factor through  pα. For example, the positions of p 2 =  + p ( + p) is either (1) no further questions or (2) a question and for each possible answer either no further questions or another question. Therefore p2 represents interviews with at most two questions, and in general for finite i, pi represents interviews with at most i questions.  


    For finitary p, the positions of _p are p-trees with finite height and whose directions are the dangling leaves. 



    A finite -tree is determined by its height and has one dangling leaf; thus, _≅.




 §.§ Monad structure on _p


Let () denote the category of monoids in (, , ).  Note that when viewed as endofunctors on , a -monoid is in fact a monad on . Therefore we refer to the objects of () as -monoids, polynomial monads, or simply monads. 


Next we will give a -monoid structure on _p.
The unit p→_p is defined to be the inclusion ι0 = p0→_p. The multiplication is more complicated so we begin with the following Lemma.



    For ordinals α, β there exist maps μα, β pα pβ→ pα + β such that for all α' < α and β' < β the following diagram commutes
    

    [column sep=large]
    	pα' p β'   pα' + β'
    pα pβ   pα + β["μα, β"', from=2-1, to=2-2]
    	["μα', β'", from=1-1, to=1-2]
    	["ια'ιβ'"', from=1-1, to=2-1]
    	["ια' + β'", from=1-2, to=2-2]



    We define the maps μα, β transinductively on α. 
    
    For α = 0, μα, β is the identity on pβ.

    For successor ordinals α + 1, suppose we have already defined μα, β. Note that 
    
    pα +1 pβ = ( + p  p α)  pβ = p β + p  pα pβ.
 So we define μα + 1,β to be the copairing of the inclusion ιβ pβ→ p α + β with the map 
    
    p  pα p β p  pα + β pα + β + 1.

    That the diagram in (<ref>) commutes for α' = α +1 can be shown inductively on α. 

    Next suppose that α is a limit ordinal and suppose we have defined μα', β pα' pβ→ pα' + β for α' < α. Then we define μα, β to be the composite
    
    pα p β = (_α' < α pα')  pβ_α' < α (pα' p β) 
            →_α' < α pα' + β→ p α + β.

    The second isomorphism follows from <ref>. That these maps make the diagram in (<ref>) commute is immediate.



This Lemma implies that for ordinals α, β < κ the maps

    pα p β p α + β→_p
 form a cocone into _p. Define the multiplication p_p _p →_p using the universal property: 

    _p _p    = (_α < κ pα) (_β < κ pβ)  ≅_α < κ_β < κ (p α pβ) →_p.

The second isomorphism follows from <ref> and <ref>.

From this definition and Lemma (<ref>), the following Lemma is immediate.


    Let p be κ-small. Then for all α, β < κ, the following diagram commutes.

    

    pα p β   pα + β
    _p _p   _p["ια + β", from=1-2, to=2-2]
    	["p"', from=2-1, to=2-2]
    	["μα, β", from=1-1, to=1-2]
    	["ιαιβ"', from=1-1, to=2-1]



As a predecessor to proving the associativity law for (_p, p, p) as a -monoid, we present the following variant of <ref> whose proof appears in <ref>.

lemmaassociativity

    For ordinals α, β, γ, the following diagram commutes:
    
    
    [column sep=huge,ampersand replacement=&]
        	pα pβ p γ&pα p β + γ
    pα + β p γ&pα + β + γ["μα, β p γ"', from=1-1, to=2-1]
        	["pαμβ,γ", from=1-1, to=1-2]
        	["μα, β + γ", from=1-2, to=2-2]
        	["μα + β, γ"', from=2-1, to=2-2]




    For every polynomial p:, there is a -monoid structure on _p, for which the unit and multiplication
    p→_p
    and
    p_p_p→_p
    are defined as above. 


    First we show the left unit law. Since _p is isomorphic to _β < κ ( pβ), the left unit law follows from <ref> with α = 0. Likewise, for the right unit law.

    Second we show associativity. Due to the isomorphism _p _p _p≅_α, β, γ < κ(pα p β p γ), it suffices to show that for  α, β, γ < κ, the outer diagram in the following commutes. 

    

    [column sep=huge]
    	pα pβ p γ   pα p β + γ   _ p _p
    pα + β p γ   pα + β + γ
    _p _p      _p["μα, β p γ"', from=1-1, to=2-1]
    	["pαμβ,γ", from=1-1, to=1-2]
    	["μα, β + γ", from=1-2, to=2-2]
    	["μα + β, γ"', from=2-1, to=2-2]
    	["ια + β + γ"', from=2-2, to=3-3]
    	["p", from=1-3, to=3-3]
    	["p"', from=3-1, to=3-3]
    	["ια + βιγ"', from=2-1, to=3-1]
    	["ιαιβ + γ", from=1-2, to=1-3]

The upper left-hand square commutes by  <ref> and the other squares commute by  <ref>.





 §.§ The monad _p is free


Now that we have verified that _p is indeed a monad, we want to justify calling it the free monad by giving a left adjoint  _-→()  to the forgetful functor U() → which takes a -monoid (q, η_q, μ_q) to its carrier q.

We begin by defining the action of _- on morphisms.
Let f p → q in . We will define _f _p →_q  by inductively defining morphisms fα pα→ q α such that for all α< β the following diagram commutes:


    pα   pβ
    qα   qβ["fα"', from=1-1, to=2-1]
    	["fβ", from=1-2, to=2-2]
    	["ια", from=1-1, to=1-2]
    	["ια"', from=2-1, to=2-2]


Define f0 p0→ q0 to be the identity on . For a successor ordinal α + 1, suppose that we have already defined fα p α→ q α. Then we define fα + 1 p α + 1→ q α + 1 to be 

    + p  pα + q  q α.

To show that the diagram in Equation (<ref>) commutes for successor ordinals, it suffices to show that for all α, the diagram with β = α + 1 commutes. By induction this is immediate by the definitions of ια + 1 and fα + 1.

Suppose that α is a limit ordinal and that we have defined fα' p α'→ q α' for all α' < α. For each α' < α we have maps 

    pα' qα' qα.
 Since the diagram in Equation (<ref>) commutes for all pairs of ordinals less than α, these maps form a cocone into qα. So, by the universal property of the colimit, pα = _α' < α p α', there is an induced map fα: p α→ qα. That the diagram in Equation (<ref>) commutes when β is a limit ordinal follows from the uniqueness of the universal map. 

Let κ be such that both p and q are κ-small. Then we define _f fκ. We defer the proof that _f is a map of -monoids to <ref>.

propositionfreef

    For f  p → q in , the polynomial map _f: _p →_q is a map of -monoids.

    
It is straightforward to show by transfinite induction that the action of _- on morphisms is functorial.
Therefore,  <ref> and <ref> define a functor _-: →(). 

theoremfreeadjunction

    There is an adjunction
    
    _-U().


Therefore _p is the free monad on the polynomial p and _- is the free monad monad. We defer the proof of <ref> and its requisite Lemmas to <ref>.






§ INTERACTIONS BETWEEN FREE MONAD AND COFREE COMONAD



 §.§ The cofree comonad comonad


It is a beautiful fact that in  the -comonoids are categories and -comonoid maps are cofunctors. Thus, we use  to denote the category of -comonoids and their maps. Dual to the construction of the free monad monad in Section <ref>, here we define the cofree comonad and show that it is right adjoint to the forgetful functor U→ given by U(c,ϵ,δ) c. In <ref> we prove the statements presented in this Section.

propositionpropcofree

    There is a functor _-→ such that _p has the structure of a -comonoid for each p:,

    _p→_p→_p_p.





For a polynomial functor q:, the positions of the cofree comonad are q-behavior trees. These are defined coinductively as a position  Q: q(1) and a map from directions of q[Q] to q-behavior trees. 















theoremcofreeadjunction

    There is an adjunction

    U_-.



Hence _q is the cofree comonad on the polynomial q and _- is the cofree comonad comonad. 



 §.§ The module structure _p ⊗_q →_p ⊗ q



For polynomials p and q consider the map 

    p ⊗_q → p ⊗ q →_p ⊗ q

where the first map is induced by the counit of _q and the second map is the unit of _p⊗ q. This composite induces a map of polynomials p → [_q, _p ⊗ q]. By duoidality of ⊗ and , the internal hom [_q, _p ⊗ q] is a -monoid as well. Therefore, by the adjunction in <ref> the map of polynomials p → [_q, _p ⊗ q] induces a map of -monoids  _p → [_q, _p ⊗ q], which is equivalent to a polynomial map

    _p,q_p ⊗_q →_p ⊗ q.

This map is the free monad-comonad interaction law described in <cit.>. In <ref> we prove the statements presented in this Section.

propositionnaturalinteraction
    The maps _p,q are natural in p and q.




Note that  is lax monoidal (see <ref>)

    _p⊗_q→_p⊗ q→_

so in this sense we would say "matter can also take the place of pattern."


Recall from <cit.> the notion of a module over a monoidal functor.

theoremmodule
    There is a left-module over _-: (, ⊗, ) → (, ⊗, ) consisting of:
    
        
  *  as a left module category over (, ⊗, ).
        
  * The functor _- →.
        
  * The natural transformation _- ⊗_- ⇒_- ⊗ -.
    






§ APPLICATIONS

In this Section, we will give four applications of the module structure introduced in Section <ref>. Each consists of:

    
  * A pattern of type p, represented by a map into _p.
    
  * Matter of type q, represented by a map into _q.
    
  * A runs on map p ⊗ q → r.

Then the composite _p ⊗_q →_p ⊗ q→_r represents the interaction pattern runs on matter.



 §.§ Interviews run on people










As in Section <ref>, suppose that the positions of p are questions and the directions are possible answers to each question. For example consider the polynomial,
p = {} ^{, } + {} ^{, , } which we can view as the corolla forest: 

    [trees, 
      level distance=10mm,
      level 1/.style=sibling distance=15mm,
      level 2/.style=sibling distance=2.5mm,
      level 3/.style=sibling distance=1.25mm]
    	 (a) 
        	child edge from parent node[left] 
        	child edge from parent node[right] 
    		;
            [right = 1in of a] (b) 
    		  child edge from parent node[left] 
    		  child edge from parent node[left] 
                child edge from parent node[right] 
    		;

Essentially, p consists of the questions:

    
  * "Do you want tea?", with possible answers "yes" or "no".
    
  * "What kind of tea do you like?", with possible answers "green", "black", or "herbal".

Consider the pattern →_p which selects the following interview:

    [trees, 
      level 1/.style=sibling distance=20mm,
      level 2/.style=sibling distance=7.5mm,
      level 3/.style=sibling distance=2.5mm]
    	
        	child node 
                    child
                    child
                    child
                 
        	child node 
                    child node 
                        child
                        child
                        child
                    
                    child 
                
    		;



The polynomial [p,] = (∏_P:p(1) p[P])  ^p(1) is the universal answerer for the polynomial p. Its positions are a choice of answer for each question in p(1) and its directions are the questions p(1). A person is a map →_[p, ]. In other words, a person is a behavior tree in which a node is an answer for each question and a branch is one such question. Each answer may depend on the sequence of questions asked so far. 

Note that [p,] is what is referred to in <cit.> as duals. We will see in <ref> that it is also interesting to consider generalizations of this duality to [p,t] for any polynomial monad t. Indeed, for any monad t, there is a map

    _p⊗_[p,t]→_t→ t


The evaluation map p ⊗ [p, ] → describes how to run a question on a universal answerer. Given an interview and a person we get the composite

    →_p ⊗_[p, ]→_p ⊗ [p, ]→_ = ,
which sends the single position of  to the number of questions asked when the interview is run on the person. For example, consider the person who would always respond that he does not want tea and he likes herbal tea. Running the tea interview on this person will cause two questions: "" then "". Conversely, consider the person who would at first respond that she does not want tea and that she likes black tea. Then after the first question, she would respond that she does want tea and she likes black tea. Running the tea interview on this person will cause three questions: "", "", then "".



 §.§ Programs run on operating systems


Consider the following program.
python
def guessing_game(max_guesses, goal):
    if max_guesses==0: 
        return False
    guess=read()
    if guess==goal:
        return True
    return guessing_game(max_guesses-1, goal)



We represent the argument/return type with the polynomial r = ∑_m: , g: ^ where m represents the variable pythonmax_guesses and g represents the variable pythongoal. We represent the effect type that reads in natural numbers with the polynomial p = ^. 
Finally, we will represent this program with a map r→_p that we  define inductively using the decomposition r = ∑_m:  r_m with r_m = ∑_g: ^. We start by defining the following maps:

    
  * Define a map r_0 →. Each position of r_0 is sent to the single position of . The single direction of  is sent to :. 
    
  * Define a map r_m+1→ p  ( + r_m).  On positions, for each position g: r_m +1(1), we need a  function from  to the positions of + r_m. In particular, we send g to the map sending g' to  if g = g' and to the position g: r_m(1) otherwise. Then on directions, if g = g', the single direction of  is sent to : and if g ≠ g', then we use the identity on directions. 

Now we will define maps r_m →_p inductively using the isomorphism _p  + p _p and the inclusion ι0→_p. As a base case, we have the composite
r_0 →_p.Given r_m →_p, we define

    r_m+1→ p  ( + _p)  p _p →_p.

A operating system with effects in [p, ] ≅ is a map →_[p, ]≅()^. It consists of a stream of natural numbers, which are the responses it will give to the pythonread() effect.

Using the interaction _p, [p, ] and the evaluation map p ⊗ [p, ] →, we get the composite

    r ≅ r ⊗→_p ⊗_[p,]→_p ⊗ [p, ]→_≅,

which expresses how the program runs on the chosen operating system. On positions it maps (m:, g:) to the minimum of m and the number of responses  the operating system takes to guess the goal g. On directions, it maps the single direction to  if the goal was guessed in at most m guesses and to  otherwise.



 §.§ Voting schemes run on voters


For a finite set of candidates X, consider the polynomial p = ∑_A ⊆ X^A. The positions of p are ballots and the directions are winners. A voting scheme with M voters is a map p →_⊗_M p where ⊗_0p and ⊗_M+1p p⊗⊗_Mp. On positions, a subset of candidates A ⊆ X maps to a terminating decision tree in which each node is a personalized ballot given to each of the M voters and each branch corresponds to the tuple  of each voter's selection. On directions, each leaf of this decision tree  maps to an overall winner. 

Exhaustive run-off is a voting scheme in which each voter selects their preference from the A candidates, and then the candidates with the fewest number of votes are eliminated. If only a single candidate remains, then they are elected the winner. Otherwise, another round of voting proceeds with the remaining candidates. This voting scheme can be encoded into a polynomial map p →_⊗_M p. As in Section <ref> we define the map inductively. Consider the decomposition p = ∑_n = 0^#X p_n where p_n = ∑_A ⊆ X, #A = n^A. Then consider the following maps:

    
  * Note that p_0 = 1 is isomorphic to ⊗_M p_0 = ⊗_M 1. There is an inclusion of p_0 into p and hence a map p_0 ⊗_M p_0 →⊗_M p.
    
  * There is a unique map p_1 →.
    
  * Define p_n + 1→(⊗_M p) (∑_k = 0^n p_k) as follows. On positions A ⊆ X maps to the product ∏_M A: ∏_M p(1) and the map ∏_M A →∑_k = 0^n p_k(1) defined by 
    (a_1,⋯, a_M) ↦ A'  A ∖#_(a_1, ⋯, a_n)
 where #_(a_1, ⋯, a_n) A → counts the number of votes for each candidate and so #_(a_1, ⋯, a_n) is the set of candidates with the fewest votes. On directions, it is the inclusion A' → A.

Now, we define p →_⊗_M p inductively as follows. As base cases we have the composites

    p_0 = 1 = ⊗_M 1 →⊗_M p →_⊗_M p
        p_1 →→_⊗_M p.

Given a maps p_k →_⊗_M p for k < n+1, we define

    p_n +1→(⊗_M p) (∑_k = 0^n p_k) →_⊗_M p(∑_k = 0^n_⊗_M p) →_⊗_M p_⊗_M p_⊗_M p.



A  voter selects a candidate from every subset of candidates. Such a voter is represented by a polynomial map → [p, ]. Running M elections on M voters is represented by the composite 
(⊗_M p) ⊗(⊗_M [p, ] )  ⊗_M  (p ⊗ [p, ]) →⊗_M  = . Therefore, given M voters, we get a composite

    p →_⊗_M p⊗(⊗_M [p, ]) →_⊗_M p⊗_⊗_M [p, ]→_ = .

On positions it maps a set of candidates A ⊆ X to the number of run-offs required to elect a candidate. On directions, it maps the single direction of  to the winner.

It is tempting to expect that the maps p →_⊗_M p define an operad enriched in the Kleisli category _ in the sense of <cit.>. However exhaustive run-off is gerrymander-able meaning that the division of voters into districts can affect the end-result of the election. This observation suggests the following definition of gerrymandering.


    A voting scheme p →_⊗_M p can be gerrymandered if and only if it does not extend to an operad enriched in _.




 §.§ Games run on players







For a game such as tic-tac-toe, let p be the polynomial whose positions are game states and whose directions are next possible moves. Then we can represent the game play as a position in _p. In the game tic-tac-toe, a  game state is a placement of 's and 's on a 3× 3 grid. In other words, it is a map b: 9 →{, , } where  represents an open grid position.  For m = 1,…, 9, let B_m be the set of valid board states with m open positions. Assuming that  always plays first, these are

    B_m {b: 9 →{, , }|#(b()) = m, #(b()) ≤#(b ()) ≤#(b()) + 1}.
 If there are an odd number of open positions, then it is 's turn. Otherwise, it is 's turn.

Given a board state b: B_m, the next possible moves are the open positions b(). Therefore,
the polynomial p_ = ∑_b: B_1 + B_3 + ⋯ + B_9 ^b() represents the board states and next possible moves for . Likewise the polynomial  p_ = ∑_b: B_2 + B_4 + ⋯ + B_8^b() represents the board states and next possible moves for .  

Consider the polynomial p = p_ ( + p_). This polynomial represents an  move followed by either game over or an  move. There exists a polynomial map ^{, , }→_p which selects the decision-tree in _p corresponding to the rules of tic-tac-toe, and maps directions to the winner of a completed game or  if the game is tied.
We will define the map  inductively. 
For m = 1,⋯, 9, let r_m = B_m ^{, , }. 

    
  * Define r_1 →, as follows. Given a board b: B_1 with a single open position, send the single direction in  to either the winner or to  if the game is tied.
    
  * Define r_m+1→ p_( + r_m) for odd m, and define r_m+1→ p_ ( + r_m) for even m, as follows. On positions send a board state b: B_m+1 to itself in p_(1) (resp. p_(1)). Then for each valid move m: b() let b': B_m be the updated board state. If b' contains a winner, then send m to  and send the single direction of  to the winner. Otherwise, send m to b': r_m(1) and let the map on directions be the identity.

Using these maps, we can inductively define maps r_m →_p for odd m as follows. As a base case we have the composite r_1 →→_p. Given a map r_m →_p, we have the composite

    r_m+2→  p_ ( + p_( + r_m)) → p_ ( + p_( + _p))    → p_ ( + p__p) 
       → p_ ( + p_) _p = p _p →_p.

The second to last map is induced by the composite

    + p__p =  + p__p →_p + p__p → ( + p_ ) _p.

Below is the image of a board state in r_3(1) under the map r_3 →_p. From left to right the directions are sent to , , , , and , as these are the win/loss/tie results of the games as shown.

    [trees, 
      level distance=20mm,
      level 1/.style=sibling distance=60mm,
      level 2/.style=sibling distance=30mm,
      level 3/.style=sibling distance=2.5mm]
    	 (a)       
          
          
        	child node       
          
          
                        child node       
          
           child[level distance=12mm]  
                        child node       
          
           child[level distance=12mm]  
        	child node       
          
          
                        child node       
          
           child[level distance=12mm]  
                        child node       
          
           child[level distance=12mm] 
                child node       
          
          
                        child[level distance=12mm] 
    		;

Define  to be the map r_9 =  ^{, , }→_p.



Let (t, η, μ) be a -monad. A polynomial map φ_→ [p_, t] represents an  player and a polynomial map φ_→ [p_, t] represents an  player. If t is the trivial monad , then for each board state, the player's next move is deterministic. If t is the lottery monad = ∑_M: ∑_P: Δ M ^M, then the players' next moves are stochastic. 

By duoidality we have 

    p ⊗ [p_, t] ⊗ [p_, t] → p ⊗ [p_, t] ⊗ [ + p_, t] → (p_x ⊗ [p_x , t])  (( + p_) ⊗ [ + p_, t]) → t  t → t
 where the first map is induced by the monoidal unit of t. Given an  player and an  player, we have a map ^{, , }≅^{, , }⊗⊗T⊗!⊗!_p⊗_⊗_.
Then, the game play is represented by the composite

    ^{, , }→_p⊗_⊗__p⊗_φ_⊗_φ__p⊗_[p_, t]⊗_[p_, t]→_p ⊗ [p_, t] ⊗ [p_, t]→_t → t

which maps directions in t to winners of completed games.

We can promote this setup to players which learn, in other words  players whose strategy dynamically changes after each completed game. A dynamic  player consists of a set of states S_ and a polynomial map S_^S_→ ^{, , }⊗_[p_, t]. Likewise for a dynamic  player. Such a player consists of the following:

    
  * For each state, a behavior tree describing the player's strategy.
    
  * For a winner or tied game and each finite path of the behavior tree, a new state.

Creating maps like φ is the subject of reinforcement learning <cit.>. As a typical such algorithm, take S_ to be the set of functions that assign a score in  to each move (direction in p_). Let S_^S_→ ^{, , }⊗_[p_, ] be defined as follows:

    
  * On positions, it takes a score for each move and assigns a (stochastic) strategy which selects moves based on their relative scores.
    
  * On directions, note that a direction of _[p_, ] contains a finite number of moves played by  in the game. If the winner is , then we add 1 to the score for each played move. Otherwise, we keep the original scores.




Using the copy-on-directions map ^{, , }⊗^{, , }→^{, , }, we have the composite

    S_^S_⊗ S_^S_→ ^{, , }⊗ ^{, , }⊗_[p_, t]⊗_[p_, t]
    → ^{, , }⊗_[p_, t]⊗_[p_, t]T_p ⊗_[p_, t]⊗_[p_, t]→ t.

This map takes a state for each player, runs the game using each player's strategy, and returns an updated state for each player based on the winner and the player's strategy.




§ CONCLUSION


In this paper, we constructed the free monad _p and cofree comonad _q on arbitrary polynomial functors p,q:, and defined a module structure _p⊗_q→_p⊗ q. We also gave a series of examples to explain how this models the intuition "pattern runs on matter."

From here, it is not hard to show that  and  respectively extend to a monad and a comonad on , the double category which serves as the base of enrichment for dynamic categorical structures for deep learning, prediction markets, etc., as defined in <cit.>. We (or others) may show in future work that for any polynomial monad t, there is a functor [-,t]_→^ from opposite of the -Kleisli category to the -coKleisli category. The latter offers the ability for different machines to operate at different rates in wiring diagrams, and the former offers the ability to call multiple subprocesses before returning, though we have not found compelling examples of either; this again is future work.

The constructions in this paper should generalize straightforwardly to free monads and cofree comonads for familial functors between copresheaf categories, as in <cit.>. One should check that there is again a module structure of the same form in that setting.








§ DISTRIBUTING COLIMITS OVER 


In general, colimits do not distribute over the subsitution product . However, in this section we give hypotheses under which the natural maps

    _j ∈ (p  q_j) → p  (_j ∈ q_j)
        _j ∈ (p_j  q) → (_j ∈ p_j)  q
 are in fact isomorphisms. 




 §.§ Right distribution

We begin with hypotheses under which colimits right distribute over .


    For an ordinal κ, a polynomial p is called κ-small if for all κ-filtered categories  and all diagrams Q→ 
    
    p ( _j  Q_j ) = _j (p  Q_j).




A polynomial p: is κ-small if and only if all of its direction-sets have cardinality less than κ. It is called finitary if and only if it is ω-small.




    If a polynomial p is κ-small, then for all κ-filtered categories  and diagrams q→
    
    p ( _j  q_j ) = _j (p  q_j).



    That this map is an isomorphism on positions follows directly from the definition of κ-small. That this map is an isomorphism on directions follows from the definition of colimits in  and the fact that connected limits preserve coproducts.




 §.§ Left distribution


Next we consider hypotheses under which colimits left distribute over .
A map ϕ p → q in  is cartesian if for every position P: p(1), the map on directions ϕ^#_P is an isomorphism (equivalently, when all ϕ's naturality squares are pullbacks). Let  be subcategory of  consisting of cartesian maps. If ϕ is cartesian, then so is pϕ and p+ϕ for any p:.

First we give a series of Lemmas which allow us to prove Proposition <ref>.





A polynomial map p→ q is an isomorphism if and only if for all sets X, the induced function p X→ q X is a bijection.


This is just a restatement of the fact that →^ is fully faithful; indeed, (p)(X)≅ p X.


The coproduct completion ΣC of a category C has as objects pairs (S,C) where S: and C S→C is a discrete diagram, and it has as morphisms lax triangles

    [column sep=10pt]
    	S_1[rr, "f"][dr, bend right=15pt, "C_1"', "" name=C1]      
    	S_2[dl, bend left=15pt, "C_2", ""' name=C2]
       C[from=C1,to=C2|-C1, shorten=5pt, Rightarrow, "f^♭"]

A diagram I→ΣC consists of a pair (S,C), where SI→ is a diagram and C S→C is a functor  from the category of elements of S to C. 


Let C be a category and let ΣC be its coproduct completion. If C has I-shaped colimits, then so does ΣC, and they are computed as follows.

Given a diagram (S,C)I→ΣC, consider the Kan extension

    S[r, "C", ""' name=C][d]   C
    π_0( S)[ur, bend right=20pt, "Lan"', "" name=colim]
    	[from=C, to=C|-colim, Rightarrow]

where π_0→ is the connected components reflection. Then the colimit is given by

    (S,C)≅(π_0( S),Lan).

For each element s_0:π_0( S), its image object Lan(s_0):C is given by the colimit over all (i,s_i)↦ s of C(s_i).


First consider the case C=1, so that ΣC≅. We need to check that for any SI→, there is a bijection

    S≅π_0( S).

This follows from the fact that the inclusion of diagrams of sets into diagrams of categories is a left adjoint, the Grothendieck construction taking diagrams of categories to categories is a left adjoint, and π_0 taking categories to sets is a left adjoint.

Given T:, a discrete diagram D T→C, and diagrams
(S_i,C_i)→(T,D), coherently over i:I, one obtains a diagram as left, which factors uniquely as right:

    [column sep=10pt]
    	 S[rr][dr, bend right=15pt, "C"', "" name=C]      
    	T[dl, bend left=15pt, "D", ""' name=D]
       C[from=C, to=C-|D, shorten=5pt, Rightarrow]
     S[r][dr, bend right=15pt, "C"', "" name=C]   π_0( S)[d, "Lan" description, "" name=L, ""' name=L'][r]   
    	T[dl, bend left=15pt, "D", ""' name=D]
       C[from=C|-L', to=L', shorten=5pt, Rightarrow]
    	[from=L, to=L-|D, shorten=5pt, Rightarrow]

This gives (<ref>). For the last statement, note that since 1→π_0( S) is a map of sets, the pullback of categories

    ∙[r][d][dr, phantom, very near start, "⌟"]    S[d]
    
      1[r, "s_0"']   π_0( S)

is also a comma square. Hence it is exact in the sense of <cit.>, completing the proof.


Lemma <ref> provides a formula for computing colimits in , since ≅Σ is the coproduct completion of . Namely, the position-set of the colimit of pI→ is given by the colimit _ip_i(1) of the position-sets, and the directions at a position P:_ip_i(1) are given by the limit (taken in , i.e. the colimit taken in ) of the associated connected diagram E_P of direction sets.

    E_P[r][d]    p(1)[r, "p[-]", ""' name=C][d]   
    
    	1[r, "P"']   _ip_i(1)[ur, bend right=20pt, "Lan"', "" name=colim]
    	[from=C, to=C|-colim, Rightarrow][ul, phantom, very near end, "⌟"]



The inclusion → reflects all colimits.


Suppose given a category I, a functor p I→, a polynomial p:, and cartesian maps φ_i p_i→p forming a cone. Suppose further that in  it is a colimit cone. To see that it is a colimit cone in  we need only check that for any q and cone ψ_i p_i→ q in , the induced map ψp→ q in  is in fact in , i.e. for any position P:p(1), the induced function ψ^♯_P q[φ(P)]→p[P] is bijective. 

By Lemma <ref>, the position-set of a colimit is the colimit of the position-sets for any diagram of polynomials, meaning there exists some i:I and P_i:p_i(1) representing P, i.e. with φ_i(P_i)=P. Since p_i→p is cartesian, we have a commuting triangle of functions q[φ(P)]→p[P]→ p_i[P_i] of which two are bijections; it follows that the required one is as well.



The inclusion → creates coproducts and filtered colimits. Moreover, the composite

    →^

creates coproducts and filtered colimits.


The functor →^ is fully faithful and hence reflects all colimits; by Proposition <ref>, → does too. It suffices to show that  has coproducts and filtered colimits, because and that the two functors → and →^ preserve them.

Coproduct inclusions of polynomials are cartesian, so the coproduct cone exists in , and hence it is a coproduct. Since  preserves coproducts, this concludes the case for coproducts.

By <cit.>, a category has (resp. a functor preserves) all filtered colimits iff it has (resp. preserves) all directed colimits, so let I be a directed category and pI→ a directed sequence of polynomials and cartesian maps. Then the induced map I→ has a colimit, say p, and it is easy to check that all the structure maps p_i→p are cartesian. Hence p≅_ip_i is a colimit in , and it is preserved by the inclusion.

It remains to check that p is a colimit in ^. That is, we need to check that for any X:, the function

    ∑_P:π_0( p)_e:E_PX^p[e]∑_P:π_0( p)X^lim_e:E_Pp[e]

is a bijection. Choose any P; it suffices to show that _e:E_P X^p[e]→ X^lim_e:E_Pp[e] is a bijection. But E_P is filtered and for any e→ e' in E_P, the map p[e']→ p[e] is a bijection. Hence we can pick any object e':E_P, replace all p_e with p_e', and have an isomorphic diagram. Now the colimit and limit are both constant, meaning that both sides of the desired map are isomorphic to X^p[e'], and hence to each other.


propositioncolimleftdistribute

For any polynomial q, filtered category I, and diagram pI→, the natural map

    _i:I(p_i q)→(_i:Ip_i) q

is an isomorphism in .


By Lemma <ref> it suffices to show that the function _i:I(p_i q) X→(_i:Ip_i) q X is a bijection for any X:. This is just two uses of Proposition <ref>:

    _i:I(p_i q) X≅_i:I(p_i q X)≅(_i:Ip_i) q X.






§ PROOFS FOR THE FREE MONAD MONAD


*

    We prove this lemma by transfinite induction on α. First, for α = 0 the result is immediate.

    Next, suppose that the result holds for α, and we will show that it holds for the successor ordinal α + 1. By definition of pα + 1, it suffices to show that the outer square in the following diagram commutes. 

    

    [column sep=75pt, row sep=large]
    	pβ pγ + p  p α p β p γ   p β + γ + p  p α p β + γ
    pβ p γ + p  p α + β p γ   pβ + γ + p α + β + γ
    pα + β + 1 p γ   pα + β + γ + 1["μβ, γ + p  pαμβ, γ", from=1-1, to=1-2]
    	["pβ pγ + p μα, β p γ"', from=1-1, to=2-1]
    	["(ιβ pγ, λα + β pγ)"', from=2-1, to=3-1]
    	["pβ + γ + p μα, β + γ", from=1-2, to=2-2]
    	["(ιβ + γ, λα + β + γ)", from=2-2, to=3-2]
    	["μβ, γ + p αμα + β, γ", from=2-1, to=2-2]
    	["μα + β + 1, γ"', from=3-1, to=3-2]


The top square commutes by the induction hypothesis. To check that the bottom squares commute, it suffices to show that the following diagrams commute as well.



    [column sep=50pt, row sep = large]
    	pβ pγ   pβ + γ
    pα + β + 1 p γ   pα + β + γ + 1["μβ, γ", from=1-1, to=1-2]
    	["μα + β + 1, γ"', from=2-1, to=2-2]
    	["ιβ p γ"', from=1-1, to=2-1]
    	["ιβ + γ", from=1-2, to=2-2]
    [column sep=50pt, row sep = large]
    	p  pα + β p γ   p  p α + β + γ
    p α + β + 1 p γ   p α + β + γ + 1["p μα + β, γ", from=1-1, to=1-2]
    	["μα + β + 1, γ"', from=2-1, to=2-2]
    	["λα + β + γ", from=1-2, to=2-2]
    	["λα + β p γ"', from=1-1, to=2-1]

The diagram on the left commutes by Equation (<ref>).
The diagram on the right commutes by the inductive definition of μα + β + 1, γ.

Finally, suppose that α is a limit ordinal and suppose that the diagram commutes for all α' < α. Recall that pα = _α' < α p α'. So it suffices to show that the outer diagram in the following diagram commutes. 



    [sep=huge]
    	pα' p β p γ   pα' pβ + γ   (_α' < α p α')  pβ + γ
    pα' + β p γ   p α' + β + γ
    (_α' < α p α' + β)  p γ      _α' < α p α' + β + γ["μα + β, γ"', from=3-1, to=3-3]
    	["μα, β + γ", from=1-3, to=3-3]
    	[from=2-2, to=3-3]
    	["μα' + β, γ"', from=2-1, to=2-2]
    	["μα', β + γ", from=1-2, to=2-2]
    	["μα', β p γ"', from=1-1, to=2-1]
    	[from=2-1, to=3-1]
    	[from=1-2, to=1-3]
    	["p α'μβ , γ", from=1-1, to=1-2]

The upper left square commutes by the induction hypothesis and the remaining diagrams commute by the definition of p for limit ordinals. 


*


    To show that _f respects the identity it suffices to show that the outer diagram in the following commutes: 


    p0   _p
       q0   _q["", from=1-1, to=1-2]
    	["f0", from=1-2, to=2-2]
    	[""', from=1-1, to=2-2]
    	["ι0", from=1-2, to=1-3]
    	["ι0"', from=2-2, to=2-3]
    	["_f", from=1-3, to=2-3]

The left triangle commutes because each map is the identity on . The square commutes as it is the diagram in Equation (<ref>).

To show that _f respects multiplication, it suffices to show that the following diagram commutes for all α and β.


    pα p β   pα + β
    qα qβ   qα + β["μα, β", from=1-1, to=1-2]
    	["μα, β"', from=2-1, to=2-2]
    	["fα + β", from=1-2, to=2-2]
    	["fα fβ"', from=1-1, to=2-1]

We show this by induction on α. For α = 0 this diagram commutes because the horizontal maps are the identity and the vertical maps are fβ. Suppose that the diagram commutes for α. Then for the successor ordinal α + 1, following the definitions of μα + 1, β and fα + 1, β we want to show that the following diagram commutes.


    [column sep = 9em, row sep = large]
    	 p β + p  p α p β   pα + β + 1
     q β + q  q α q β   qα + β + 1["(ιβ,(p μα, β) λα + β)", from=1-1, to=1-2]
    	["(ιβ, (p μα, β) λα + β)"', from=2-1, to=2-2]
    	["fα + β + 1", from=1-2, to=2-2]
    	["fβ + f  fα fβ"', from=1-1, to=2-1]

The diagram commutes on the first term of the coproduct because the diagram in Equation (<ref>) commutes with the pair β < α + β. To show that the diagram commutes on the second term, it suffices to show that the outer diagram in the following commutes.


    [sep=huge]
    	p  p α p β   p  p α + β   p α + β + 1
    q qα q β   q qα + β   qα + β + 1["f  fα fβ"', from=1-1, to=2-1]
    	["p μα, β", from=1-1, to=1-2]
    	["qμα, β"', from=2-1, to=2-2]
    	["f  fα + β", from=1-2, to=2-2]
    	["fα + β + 1", from=1-3, to=2-3]
    	["λα + β", from=1-2, to=1-3]
    	["λα + β"', from=2-2, to=2-3]

The left-hand square commutes by the induction hypothesis and the right-hand square commutes by definition of fα + β + 1.




 §.§ Proof of Theorem <ref>


The trickiest part of proving the adjunction in Theorem <ref> is defining the co-unit so we do it separately in the following series of Lemmas.

  
      

    Let (q, η_q, μ_q) be a -monoid. For each ordinal α, there exist a cocone of maps
    
    α qα→ q.



    We will define the cocone of maps α inductively.
    First, define 0 q 0 = → q to be the unit η_q.

    Next, suppose that we have a cocone of maps α': qα'→ q for all α' < α. 
    If α is a limit ordinal then we define α qα→ q to be the universal map induced by the cocone. If α + 1 is a successor ordinal, then we define α + 1 to be the composite
    
    qα + 1 =  + q  q α q + q  q q.


    To show that these maps form a cocone, it suffices to show that the following diagram commutes for all α' < α.
    
    
    qα'
    qα    q
        	["α'", from=1-1, to=2-2]
        	["α"', from=2-1, to=2-2]
        	["ια'"', from=1-1, to=2-1]


    If α is a limit ordinal, then this is immediate. Otherwise, α is a successor ordinal, say α = β + 1. It suffices to show that the following diagram commutes. 
    
    
    qβ
    qβ + 1    q
        	["β", from=1-1, to=2-2]
        	["β + 1"', from=2-1, to=2-2]
        	["ιβ"', from=1-1, to=2-1]

    
    Consider the following three cases.
    
        
  * Suppose that β = 0, then it is immediate that the desired diagram commutes as we see below.
        
        
    [column sep = 60pt]
            	q0 = 
    q1 =  + q    q + q    q
            	["ι0"', from=1-1, to=2-1]
            	["(1,1)"', from=2-2, to=2-3]
            	["η_q + μ_q ∘(q η_q)"', from=2-1, to=2-2]
            	["η_q", bend left=10pt, from=1-1, to=2-3]


        
  * Next suppose that β is a successor ordinal. In particular β = γ + 1. 
        To show that 
        
        
    [sep = large]
            	qγ + 1
    qγ + 2    q
            	["ιγ + 1"', from=1-1, to=2-1]
            	["γ + 1", from=1-1, to=2-2]
            	["γ + 2"', from=2-1, to=2-2]

        commutes, it suffices to show that 
        
        
    [sep = huge]
            	 + q  q γ
     + q  q γ + 1   q + q  q["η_q + q γ + 1"', from=2-1, to=2-2]
            	[" + q ιγ"', from=1-1, to=2-1]
            	["η_q + q γ", from=1-1, to=2-2]

        commutes. This is immediate from the induction hypothesis. 
        
  * Finally, suppose that β is a limit ordinal. Then we want to show that the outer diagram in the following commutes. 

        
        
    [sep = huge]
            	qβ'
    qβ' + 1 =  + q  qβ'
     + q  qβ   q + q q    q
            	["ιβ'"', from=1-1, to=2-1]
            	[" + q ιβ'"', from=2-1, to=3-1]
            	["(1, μ_q)"', from=3-2, to=3-3]
            	["β'", from=1-1, to=3-3]
            	["η_q + q β"', from=3-1, to=3-2]
            	["β' + 1"description, from=2-1, to=3-3]
            	["η_q + q β'"description, from=2-1, to=3-2]

        The top and bottom triangles commute by the induction hypothesis and the middle triangle commutes by definition of β' + 1.
    




    For all ordinals α, β the following diagram commutes.
    
    
    qα qβ   qα + β
    q q    q
        	["μ_q"', from=2-1, to=2-2]
        	["α + β", from=1-2, to=2-2]
        	["αβ"', from=1-1, to=2-1]
        	["μα, β", from=1-1, to=1-2]



    We induct on α.  Suppose that for all α' < α the diagram commutes. Consider the following cases.

    
        
  * For α = 0, we have that 
        
        
    qβ   qβ
    q q    q
            	["μ_q"', from=2-1, to=2-2]
            	["1_qβ", from=1-1, to=1-2]
            	["η_q β"', from=1-1, to=2-1]
            	["β", from=1-2, to=2-2]

        commutes by the unit law of the monoid (q, η_q, μ_q).

        
  * Suppose that α is a successor ordinal, say α = α' + 1. We must show that the following diagram commutes. 
        
        
    [column sep = 9em, row sep = huge]
            	 qβ + q  qα' qβ   qα' + β + 1
    q q    q
            	["(ηβ, (μ _q ∘(q α')) β)"', from=1-1, to=2-1]
            	["(ι_β, λα' + β∘ (q μα', β))", from=1-1, to=1-2]
            	["α' + β + 1", from=1-2, to=2-2]
            	["μ_q"', from=2-1, to=2-2]

        We will show that the diagram commutes on each component of the coproduct independently. For the first term observe  that 
        
        
    qβ   qβ   qα' + β + 1
    q q    q
            	["ηβ"', from=1-1, to=2-1]
            	["1_qβ", from=1-1, to=1-2]
            	["ι_β", from=1-2, to=1-3]
            	["β", from=1-2, to=2-2]
            	["μ_q"', from=2-1, to=2-2]
            	["α' + β + 1", from=1-3, to=2-2]

        commutes because of the unit law of the monoid (q, η_q, μ_q) and because the maps β form a cocone.

        For the second term consider the following diagram.

        
        
    [sep = huge]
            	q qα' q β   q  qα' + β   qα' + β + 1
    q q  q   q q
    q q       q
            	["qα'β"', from=1-1, to=2-1]
            	["μ_q  q"', from=2-1, to=3-1]
            	["q μ_q"', from=2-1, to=2-2]
            	["μ_q"', from=2-2, to=3-3]
            	["μ_q"', from=3-1, to=3-3]
            	["qμα', β", from=1-1, to=1-2]
            	["qα' + β", from=1-2, to=2-2]
            	["λα' + β", from=1-2, to=1-3]
            	["α' + β + 1", from=1-3, to=3-3]

        The upper left square commutes by the induction hypothesis. The bottom square commutes by associativity of μ_q, and the right-most square commutes by definition of α' + β + 1. Therefore the outer square commutes as desired.

        
  * Suppose that α is a limit ordinal. Recall that 
        
    qα qβ_α' < α qα' + β.
 
        The composite α + β∘μα, β is induced by the cocone defined for α' < α by
        
    qα' q β qα' + β q α + β q
 while the composite μ_q ∘ (αβ) is induced by the cocone defined for α' < α by 
        
    qα' q β q  q q.
 For each α' < α these composites are identical by the induction hypothesis. Therefore by uniqueness of the induced maps 
    α + β∘μα, β = μ_q ∘ (αβ)
 as desired.
    






*

    For p: define the unit of the adjunction, _p  p →_p, to be the composite
    
    p  p1_p.

    For f p → q in , consider the following diagram.
    
    
    p     + p  = p1   _p
    
        	q     + q = q1   _q["f"', from=1-1, to=2-1]
        	[" + f = f1", from=1-2, to=2-2]
        	["λ0", from=1-1, to=1-2]
        	["λ0"', from=2-1, to=2-2]
        	["_f", from=1-3, to=2-3]
        	["ι1"', from=2-2, to=2-3]
        	["ι1", from=1-2, to=1-3]

    The square on the left commutes by definition of f1 while the square on the right commutes by the commuting diagram in Equation (<ref>). Therefore, the outer square commutes and  is natural.

    For the  -monoid (q, η_q, μ_q), we define the counit of the adjunction _q  (_q, q, q) → (q, η_q, μ_q) to be ϵκ_q → q for κ such that q is κ-small. 
    The map _q preserves the unit because the maps α form a cocone. 
    That _q preserves multiplication is a direct result of Lemma <ref>. Therefore _q is indeed a map of -monoids. 

    Next we want to show that  is natural. Let f (p, η_p, μ_p) → (q, η_q, μ_q) in (). It suffices to show for all α the following diagram commutes. 
    
    
    pα   qα
    
        	p     q
        	["pα"', from=1-1, to=2-1]
        	["α", from=1-2, to=2-2]
        	["fα", from=1-1, to=1-2]
        	["f"', from=2-1, to=2-2]


    We show this by induction on α. For α = 0, fα is the identity on  and the diagram commutes because f preserves the unit.

    Suppose that the diagram commutes for all α' < α. If α is a successor ordinal — say α = α' + 1 — then we want to show that the following diagram commutes.
    
    
    + p  pα'    + q  qα'
    
        	p     q
        	[" + f  fα'", from=1-1, to=1-2]
        	["f", from=2-1, to=2-2]
        	["(η_p, μ_p ∘ (p pα'))"', from=1-1, to=2-1]
        	["(η_q, μ_q∘(q α')) ", from=1-2, to=2-2]


    It commutes on the first term of the coproduct, again because f preserves the unit. To show that it commutes on the second term, we want to show that the outer diagram in the following commutes. 

    
    
    [column sep = large]
        	p  p α'   q qα'
    p  p   q q
    
        	p     q
        	["f fα'", from=1-1, to=1-2]
        	["p pα'"', from=1-1, to=2-1]
        	["qα'", from=1-2, to=2-2]
        	["f f"', from=2-1, to=2-2]
        	["μ_p"', from=2-1, to=3-1]
        	["μ_q", from=2-2, to=3-2]
        	["f", from=3-1, to=3-2]

    The top square commutes by the induction hypothesis and the bottom square commutes because f preserves multiplication. 

    

















If α is a limit ordinal, consider the cocones

    pα'fα' qα'ϵα' q
        
        pα'ϵα' p f q.

By uniqueness, the cocone on the left induces the map pαfα qαϵα q. Also by uniqueness, the cocone on the right induces the map pαϵα p f q. Furthermore, these cocones are identical by the induction hypothesis and so their induced maps are equal, as desired.

   
        
Finally, to show that the unit and counit form an adjunction we must show that for a polynomial p

    _p __p_p
 is the identity and that for a -monoid (q, η_q, μ_q)

    q _q  q
 is the identity as well. It suffices to show the second as the first follows with q = _p.

Since the diagrams below commutes, it suffices to show that 1∘λ0 is the identity. This is immediate from the definition of 1 and the unit law for (q, η_q, μ_q).



    q    q1   _q    q
    	["ϵ_q", from=1-3, to=1-4]
    	["ι1", from=1-2, to=1-3]
    	["λ0", from=1-1, to=1-2]
    	["ϵ1"', curve=height=18pt, from=1-2, to=1-4]
    




§ PROOFS FOR THE COFREE COMONAD MONAD


*


Given a polynomial p, define polynomials p^(i) for i∈ by

    p0
      p1+i×(p pi)

There is a projection map π0 p1→ p0, and if πi p1+i→ pi has been defined, then we can define π1+i×(pπi). Now define the polynomial

    _plim(⋯π2p2π1p1π0p0)

and we note that this construction p↦_p is natural in p:.

This polynomial comes equipped with a counit ϵ_p→=p0 given by the projection. We next construct the comultiplication δ_p→_p_p. Since  commutes with connected limits, we have

    _p_p=
      (lim_i_1pi_1)(lim_i_2pi_2)≅lim_i_1,i_2(pi_1 pi_2)

To obtain the comultiplication lim_ipi→lim_i_1,i_2(pi_1 pi_2), it suffices to produce a natural choice of polynomial map φ_i_1,i_2 pi_1+i_2→ pi_1 pi_2 for any i_1,i_2:. When i_1=0 or i_2=0, we use the unit identity for . By induction, assume given φ_i_1,1+i_2; we construct φ_1+i_1,1+i_2 as follows:

    p1+i_1+1+i_2   =
      ×(p pi_1+1+i_2)
       →×(p pi_1 p1+i_2)
       →(× p pi_1) p1+i_2
       =
    
      p1+i_1 p1+i_2

where (<ref>) is φ_i_1,1+i_2 and it remains to construct (<ref>). Since - q preserves products for any q, constructing (<ref>) is equivalent to constructing two maps

    ×(p pi_1 p1+i_2)ϕi_1,i_2 p1+i_2×(p pi_1 p1+i_2)→ p pi_1 p1+i_2.

For the latter we use the second projection. The former, ϕi_1,i_2 p1+i_1+1+i_2→ p1+i_2, is the more interesting one; for it we also use projections pi_1→ p0= and πi_2 pi_2+1→ pi_2 to obtain:

    ×(p pi_1 p1+i_2)→×(p pi_2)≅ p1+i_2

We leave the naturality of this to the reader.

It remains to check that ϵ and δ satisfy unitality and coassociativity. The base cases above imply unitality. Proving coassociativity amounts to proving that the following diagram commutes:

    [column sep=50pt]
    	p1+i_1+1+i_2+1+i_3[r, "ϕi_1,i_2+1+i_3"][d, "ϕi_1+1+i_2,i_3"']   
    	p1+i_2+1+i_3[d, "ϕi_2,i_3"]
    
    	p1+i_3[r,equal]   p1+i_3

This can be shown by induction on i_3.




There is a monoidal structure on →

    →__p⊗_q→_p⊗ q.



The polynomial _≅^ has a unique position, and this defines the first map. However, it is conceptually cleaner to realize that comonads are closed under ⊗ by duoidality, and hence both  and _p⊗_q carry comonad structures. Thus the desired maps are induced by the obvious polynomial maps ≅ and _p⊗_q→ p⊗ q. It is straightforward to check that these are unital and associative.


*


We will abuse notation and denote the comonoid (c,ϵ,δ): simply by its carrier c. We first provide the counit and unit of the desired adjunction. The counit

    ϵ_p_p→ p

is given by composing the projection map _p→ p1 from construction (<ref>) with the projection p1≅× p→ p. Since _c is defined as a limit, the unit

    η_c c_c

will be given by defining maps ηi c→ ci commuting with the projections πi c1+i→ ci, for each i:, and then showing that the resulting polynomial map η_c is indeed a cofunctor. Noting that c0=, we define

    η0ϵ

Given ηi c→ ci, we define η1+i as the composite

    c(ϵ,δ)×(c c)×(cηi)×(c ci)=c1+i.

Clearly, we have η0=π0∘η1. It is easy to check that if ηi=πi∘η1+i then η1+i=π1+i∘η2+i. Thus we have constructed a polynomial map η c→_c. It clearly commutes with the counit, so it suffices to show that η commutes with the comultiplication, which amounts to showing that the following diagram commutes

    c[r, "δ"][d, "(ϵ,δ)"']   [27pt]
      c c[r, "(ϵ,δ)(ϵ,δ)"]   [15pt]
      (×(c c))(×(c c))[d, "(× cηi_1)(× cηi_2)"]
    ×(c c)[r, "× cηi_1+1+i_2"']   ×(c ci_1+1+i_2)[r, "φ_1+i_1,1+i_2"']   (×(c ci_1))(×(c ci_2))

for all i_1,i_2:, where φ_1+i_1,1+i_2 is the map constructed in Equation (<ref>) and Equation (<ref>). Commutativity follows from the counitality and coassociativity of the comonoid c.

The triangle identities are straightforward as well. Indeed, for any comonoid c:, the composite cU∘η_c_cϵ_Uc c is equal to the composite of c(ϵ,c)c1=× c, with the projection c1→ c, the result of which is the identity. Finally, for any polynomial p:, the composite _pη__p__p_ϵ_p_p is given by taking a limit of maps of the form

    _p(ϵ,δ)×(_p_p)×(_pηi)×(_p_pi)×(ϵ_pϵ_pi)×(p pi)

Each one is in fact the projection _p→ pi+1, so the resulting map is the identity on _p, completing the proof.




§ PROOFS FOR THE MODULE STRUCTURE _P ⊗_Q →_P ⊗ Q


*

    To show that ψ is natural in p, it suffices to show that for a maps p → p' and q → q' in  the following diagram commutes:
    
    
    p    [_q, _p ⊗ q]
    p'   [_q', _p' ⊗ q'][from=1-1, to=2-1]
        	[from=1-1, to=1-2]
        	[from=1-2, to=2-2]
        	[from=2-1, to=2-2]

    This follows immediately from the commutativity of the following diagram.
    
    
    p ⊗_q   p ⊗ q   _p ⊗ q
    p' ⊗_q'   p'⊗ q'   _p'⊗ q'[from=1-1, to=2-1]
        	[from=1-1, to=1-2]
        	[from=1-2, to=1-3]
        	[from=2-1, to=2-2]
        	[from=1-2, to=2-2]
        	[from=2-2, to=2-3]
        	[from=1-3, to=2-3]

    Note that the square on the left commutes by naturality of the counit of the adjunction in <ref>. The square on the right commutes by naturality of unit of the adjunction in <ref>.


* 


    We must show that two diagrams commute. First, we will  show that the following diagram commutes.
    
    
    ⊗_r   _r
    _⊗_r   _⊗ r["", from=1-1, to=1-2]
        	[from=1-1, to=2-1]
        	[from=2-1, to=2-2, "_,r"']
        	[""', from=2-2, to=1-2]

    It suffices to show that the diagram below commutes: 
    
    
    ⊗ r    r    _r
    _⊗ r   ⊗ r   _⊗ r[from=2-3, to=1-3]
        	[from=1-1, to=2-1]
        	[from=2-1, to=2-2]
        	[from=2-2, to=2-3]
        	[from=1-1, to=1-2]
        	[from=1-2, to=1-3]
        	[from=2-2, to=1-2]

    The square on the left commutes because →_→ is the identity. The square on the right commutes by the naturality of the unit of the adjunction in Theorem <ref>.

    Next we must show that the following diagram commutes.
    
    
    _p ⊗_q ⊗_r   _p ⊗_q ⊗ r
    _p ⊗ q⊗_r   _p ⊗ q⊗ r[from=2-1, to=2-2]
        	[from=1-1, to=2-1]
        	[from=1-1, to=1-2]
        	[from=1-2, to=2-2]

    It suffices to show that the following diagram commutes.
    
    
    _p ⊗_q ⊗ r   _p ⊗ q ⊗ r   _p ⊗_q ⊗ r
    _p ⊗ q⊗ r   p ⊗ q ⊗ r   _p ⊗ q ⊗ r["_p, q ⊗ r", from=1-3, to=2-3]
        	[from=2-2, to=2-3]
        	[from=1-2, to=2-2]
        	[from=1-2, to=1-3]
        	[from=1-1, to=1-2]
        	[from=2-1, to=2-2]
        	[from=1-1, to=2-1]

    The square on the left commutes by definition of the laxator of _- while the square on the right commutes by definition of _p, q ⊗ r.





