minor cleanups and changes to proof style to Functors and Kleisli
	modified:   Functors.agda
	modified:   Kleisli.agda