For example, consider the standard powerset function that maps the representation of a set as the list of its elements (in any order and without repetition) to the representation of its powerset:Definition powerset (V : Type) (vs : list V)

@article{paperbot732,
  title = {Folding left and right over Peano numbers},
  author = {OLIVIER DANVY},
  journal = {Journal of Functional Programming},
  volume = {29},
  year = {2019},
  doi = {10.1017/s0956796819000042}
}