Second pullback lemma added.
	modified:   Categories.agda