section and retraction are mono and epi respectively
	modified:   Categories.agda