> 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-0.5.11.0/docs/Data-Set.html) 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-0.2.9.0/docs/Data-HashSet.html) 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.