'Pullback with identities implies monic' lemma added.
	modified:   PullbacksLemmas.agda