split Bidir.agda to FinMap.agda