Andreas Blass has pointed out to me that that there was a mistake in my recent mail. There does exist a global element n : 1 -> N such that G \cong K_n (n is the order of the group G) BUT the statement G \cong K_n contains a hidden existential quantifier over Iso(G,K_n) and this latter one is not witnessed by a global section of Iso(G,K_n). Thomas Streicher