define restriciton category of total maps, I think
	modified:   RestrictionCat.agda