I read that some magic called Stone duality makes the category of complete atomic boolean algebras and the opposite category of sets equivalent.
https://ncatlab.org/nlab/show/Set#OppositeCategory
I've been interested in a nice way of working with $\text{Set}^{\text{op}}$. I've actually trying to figure out an internal language for it. Directly working with coexponentials and such is really confusing though. So Stone duality sounds super interesting to me.
Can I use Stone duality to get a nice way of talking about $\text{Set}^{\text{op}}$?
There seems to be some weirdness with respect to constructivity though? Perhaps a similar construction works with Heyting Algebras? My theorem prover of choice is Coq if that helps.