finished pasting lemma 1
	modified:   Categories.agda