equationalising
	modified:   CatofAdj2.agda