The following remains to be defined in `univalent-combinatorics.repetitions-of-values`: - [ ] The predicate that `f` maps two different elements to the same value