koyama41
おそらく、暗黙のうちに「外延性の公理」は前提にしているのだと思います。というか、そういう前提をいれてようやく Hask圏は圏になる、というか。
Monoid ∀m => (a -> m) -> m = Free a
Nat(Hom_Set(A,U(-)), U(-)) {- U は忘却関手。Freeとの随伴により -} = Nat(Hom_Monoid(Free(A),-), U(-)) {- 米田の補題により -} = U(Free(A)) = Free(A)
Nat(Hom(A,U(-)), U(-)) {- U と F の随伴により -} = Nat(Hom(F(A),-), U(-)) {- 米田の補題により -} = U(F(A)) = M(A)
Monad m => ∀b. (a -> m b) -> m b = m a