defined the necessary map for the first pasting lemma, need to prove various things commute and then completeness.
	modified:   Categories.agda