definition of the category where every idempotent split and first steps in the proof of the completeness theorem.
	modified:   Categories.agda
	modified:   RestrictionCat.agda