Elegant demonstration with minimum category theory knowledge I come from computer science background so Category Theory show up naturally inside the Category Hask (Types and Functions). I studied a little bit of the theory, but I wish to have some examples of mathematical proofs that use it.
Do you have examples of (useful/practical) theorem that can proven using Category theory and yet is accessible to someone with little knowleadge of theory (functors, limits, colimits, maybe natural transformations, ...)
I think this will help me understand deeper the usefulness and beauty of category theory !
Thanks :)
 A: A typical application is of the following kind. At some point in a proof you might need to know whether or not some functor $F$ commutes with limits or colimits of a particular shape. The easiest way to resolve such questions is that


*

*if $F$ is a left adjoint then it commutes with all colimits, and

*if $F$ is a right adjoint then it commutes with all limits.


Otherwise things are hard. But this is already a very useful observation: for example, it implies that tensor product $M \otimes (-)$ (say, of modules) commutes with colimits, since it is left adjoint to hom $\text{Hom}(M, -)$. 
Here is an example; there are many more like it. The symmetric algebra functor $S(V) = \bigoplus_n S^n(V)$ is the left adjoint to the forgetful functor from commutative $k$-algebras to $k$-vector spaces. It follows that it commutes with colimits, and in particular that it sends direct sums of vector spaces to tensor products of $k$-algebras, so we get that
$$S(V \oplus W) \cong S(V) \otimes S(W)$$
(a kind of categorified exponential property). Keeping track of gradings gives the following identity involving symmetric powers: 
$$S^n(V \oplus W) \cong \bigoplus_{i+j=n} S^i(V) \otimes S^j(W).$$
An analogous fact is true for exterior powers but it requires slightly more work to state the appropriate universal property. 
