Kleisli is the initial adjunction
	modified:   Everything.agda
	new file:   InitAdj2.agda