proved that SplitCat is a split restriction category
	modified:   Functors.agda
	modified:   RestrictionCat.agda
	modified:   Splits.agda