> Actually, if anyone knows any good literature on set-based algorithms, maybe I can clean up my attempt above.

Well, in Haskell there's [`Data.Set`](https://hackage.haskell.org/package/containers- in the `containers` module. This is for representing finite sets. The docs carefully talk about the complexity of all operations. This is nice if you want to micro-optimize your algorithm.

There's also [`Data.HashSet`](https://hackage.haskell.org/package/unordered-containers- which is more like sets in Python or Clojure.

In a computer proof system definitions tend to be declarative rather than recursive. This is because proving the correctness of recursive algorithms is hard. For instance, check out John Wiegley's [Comma-Category construction in Coq](https://github.com/jwiegley/category-theory/blob/master/Construction/Comma.v). He just declares his Comma category *hom-set* in terms of a base *hom-set* and proves the definition is well defined, rather than using recursion or fixedpoints.

If there's a HoTT expert around, I am curious how they approach this problem.