Agda library for general computation