I probably should have added an abstract :) What I am getting at here is that *free* object constructions build higher-order structures relative to those they are built from and relative to the target of their associated right-adjoint (often the category of sets via a forgetful functor). That these higher-order structures then support notions that may not exist in a direct way relative to the structures they are built from, one can view these newly supported notions as a kind of *epiphenomena* relative to the underlying structure.
While it is not meaningful to speak about the length of a set, we can support a higher-order monoidal structure where length is a meaningful notion. For a monoid relevant example[𝜆], consider the following recursive definition of the length of a list: len :: [a] -> Int len [] = 0 len [t] = 1 len (t:ts) = len [t] + len ts What I seek to show is that this definition follows directly from an adjunction that constructs *free* monoids from sets. A functor F :: Set -> Mon builds from the elements of a set X, the set of all possible words on X and equips this set with a multiplication (++) and an identity element ([]). This functor has a right 'forgetful' functor which forgets the monoidal structure and returns the set of all possible words on X, X*. We can then look at morphisms from this object (X*, ++, []) into a natural number monoid (ℕ, +, 0), taking concatenation to addition and the empty word to the additive identity (the first and third rule in the definition above). Now, the second rule (len [t] = 1) is a little arbitrary and finds its meaning in the interaction between the underlying category of sets and the higher-order monoidal category. There in Set, we find a composition that ultimately gives len its character. The composition of Functors (G∘F) gives a natural map, η, which includes X into X* as an inclusion of generators. Looking at η: X -> X* and the map const1 :: X -> ℕ (Where ℕ is given by the same forgetful functor G and all elements of X are mapped to the number 1), we find that the unique function G(len) :: X* -> ℕ that makes the triangle commute and respects the functorial conditions gives via the monoidal structure the notion of length we seek. The structural functors (G and F) can be seen as *founding* a category of monoids upon a category of sets, and dually *structuring* the category of sets by the category of monoids. [𝜆] This example is from Benjamin Pierce's 'Category Theory for Computer Scientists'. -- Sent from: http://friam.471366.n2.nabble.com/ - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/
