Open finegeometer opened 1 year ago
Something just occurred to me: If you want the theorem to compute efficiently, it should probably be reimplemented using the union-find algorithm. Computational behavior wasn't a concern for my application, but it might be for some.
Also without that, I think that statement is a good addition to the library. Please make a (draft) pull request.
I recently found myself in need of a theorem that any set-coequalizer of finite sets is finite. Would it make sense to add this theorem to the standard library, either in
Cubical.Data.FinSet.Constructors
or inCubical.HITs.SetCoequalizer.Properties
?For reference, here's the proof I eventually managed to construct. This code would need some work to bring it up to the standards of this library, but it at least demonstrates that the theorem is correct, along with one possible method of proving it. (I'd be curious to know if there's a shorter proof!)