Prove kan extensions/(co)limits are functorial

It follows very straightforwardly from the construction of adjoints of
initial/terminal morphisms, but required fixing a typo in the definition
of colimits (oops).

I renamed KanExtension/KanExtension.v to KanExtension/Core.v (and similarly for limits), to follow with the naming convention of other folders.