trivial
	modified:   RestrictionCat.agda