Solutions to lcpt@fmi 2019/2020 Agda stuff requires 2.6.1, because of implicit non-dependent functions ({A} -> B).