Incl is a RestFun, postulated RFun= (for now)
	modified:   RestrictionFunctors.agda
	modified:   SplitRestCats.agda
	modified:   Splits.agda