In Haskell, the hom set isomorphism of Adjunction (Prod s) (Reader s) is: ((a, s) -> b) (a -> (s -> b)) So is currying also related to this adjunction and the state monad?
Watching that part about isomorphisms on monoids I got stuck at arond min 9 where you write Mon(Fx,m) ~ Set(x,Um) Say I take the unit set x = 1 = {*}, and I map that to the Free Monoid F1, which would be the set of all lists made of stars = { [], [*], [*,*],...} In the category of monoids I could then choose m=N the monoid of natural numbers. It seems clear that there is only one mapping from F1 to N, namely the mapping that maps the length of the list to N. Now the Underlying set of N, U(m) = N. But there are an infinite number of arrows from 1 to N, namely 1 for each number. So I don't see how there can be an isomorphism there...
I suppose there are a lot more morphisms in monoid from F1 to N... I thought up a few: 1. we map every list to 0. Then f([*]+[*])=0=f([*])+f([*])=0+0 2. we map [] to 0, and [*] to 2. Then f([*])+f([*])=2+2=f([*,*]) Since we can map [*] to any number we get the same number of morphisms in Mon as we do in Set...
Exactly! You must map [] to 0, but the singleton [*] can be mapped to any number, which gives you exactly the 1 to 1 correspondence with the mappings of * to N.
Wait, but representables in Hask are already Monads (since they have to be isomorphic to (Reader r) which is Hask's Hom-object ). Does this mean that adjunctions in Hask are a way to "extend" a Monad using an endofunctor?
There is something I'm getting wrong about the intuition of free monoids in its representation as free-forgetful adjuntions. I understand that list of natural numbers with concatenation is a free monoid that can have a morphism to the monoid of natural numbers with sum. In sum we map 2 and 3 to 6, while in concatenation it is just another element [2, 3]. But how does it make its generator sets differ? Isn't the set of natural numbers the generator set in both cases?
The set of natural numbers with addition has only one generator, 1. So it's generator set is a singleton. In Haskell you could write it as a list of unit type [()]. The only relevant information in a list of units is its length, which is a natural number.
I got stuck at 4:50, you said "The Left functor have to map the whole category Set into some sub category of monoids that have lots of homomorphisms coming from that". It is OK about "The Left functor have to map the whole category Set into some sub category of monoids". Because functor may loss information, e.g: collape objects and morphisms. So the red circle is a sub category of Mon. But what's the really mean about "have lots of homomorphisms coming from that"? I think the morphisms in Set are not necessary homomorphisms, they can be arbitrary functions. We got homomorphisms in Mon due to the functor F collapse some things. Could you explain it further? I might miss something... Very thanks.
Today I revisited this video and found that my previous understanding was wrong. The following is my new understanding (correct me, if I am wrong): The observation is although the Set is richer than Mon in morphisms, the Mon is richer than Set in objects (i.e: the number of objects in Mon is much larger than the number of objects in Set). This because: (1) Forgetful functor U from Mon to Set may collapse thing. For example, addition and multiplication can form two monoids (called m_add, m_mul), but their use the same underlying set Nat. (2) From another point of view, for every nonempty set in Set, we can select a binary operation making it a monoid. (due to Axiom of choice, see mathoverflow.net/a/12988/144229) So, a functor F from Set to Mon, the image in Mon should be a subset of Mon (sub-category of Mon, more precisely). For example, suppose we have a set Nat in Set, the functor F will map it to Mon, the image of Nat in Mon can be m_add or m_mul or so on (F must choose one of them). We want this F to map the set Nat to the best one in Mon! (In fact, it is neither m_add nor m_mul, it must be a free monoid) Therefore in 4:50, the F functor : Set -> Mon (which map the whole Set to the red circle in Mon) is not a arbitrarily functor. It is a particular functor which map every set x in Set to the free-monoid (which look x as a generator set) in the Mon. (N.B: empty set will map to trivial monoid {e}).
I'm a little bit of confused at 34:05 when defining unit. The type signature is a -> Reader s (Prod s a), but the implementation is missing the constrctor? I guess it should be unit = \s -> Reader (s -> (Prod (s, a))). And I think (s, a) is not the same as Prod (s, a). I don't know why you can omit the constrctor.
I can omit constructors because I'm writing pseudo-code. I keep saying "modulo constructors." The idea is that adding constructors is an exercise for the reader (with the help of the compiler).
