working on pullback property of sections of restriction idempotents.
	modified:   Categories.agda
	modified:   RestrictionCat.agda