I have been reading the real-cohesive homotopy type theory paper and one of the remarks has sparked an interest. In this paper a string of monadic and comonadic modalities is introduced together with cohesion axioms, such that it is possible to prove that $\int \mathbb{S}^1 = S^1$ (Theorem 9.17), where $\int$ is one of the comonadic modalities, $S^1$ is the higher inductive type of circle, and $\mathbb{S}^1$ is defined as some circle in terms of the type of reals $\mathbb{R}$.

Are there any result, papers, blogposts, mailing list discussions etc., which (attempt to) connect the lambda calculus term for various topological spaces as in Abstract stone duality with the higher inductive types in homotopy type theory?

Is there a theory which extends Abstract stone duality to homotopy type theory and where it would be possible to develop synthetic topology and connect it to the higher inductive types? Something I am imagining is some form of synthetic topology in terms of types connected with higher inductive types using modalities without mentioning reals.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.