This is the second in a pair of questions. For the other see Are representations in computable analysis the equivalent to countably-generated condensed sets?.
Dustin Clausen and Peter Scholze have a theory of condensed sets (see Lectures in condensed mathematics), which is a slightly different take on topology. For most cases, the behavior of the usual topology and the “condensed” one, align. However, for some quotient spaces, like $\mathbb{R} / \mathbb{Q}$, the usual quotient topology is indiscrete, so every map $f : \mathbb{R} / \mathbb{Q} \to \mathbb{R} / \mathbb{Q}$ is continuous. However, as a condensed set, more structure is preserved. Indeed, the “continuous” maps are exactly those coming from continuous functions $\mathbb{R} \to \mathbb{R}$ which commute with the equivalence relation. (See this answer to Examples of the difference between Topological Spaces and Condensed Sets for more motivation.)
I’m trying to understand condensed sets better and how they relate to topology as it comes up in constructive mathematics.
In constructive theories, for example dependent type theory, there is an interesting phenomenon that I’ve always found fascinating. Just from the axioms of type theory, we automatically get topological structure on types. For example, every constructively definable function $f : 2^\mathbb{N} \to 2^\mathbb{N}$ is continuous for the usual product topology applied to $2^\mathbb{N}$.
Now, many constructive theories also allow quotients. For example, in Coq you can add quotients, and similarly in Homotopy Type Theory quotients are implied by univalence and higher inductive types. While quotients may break computability in some theories, if I understand correctly, they don’t break continuity. (For example, you still can’t construct a term for a non-continuous function $f : 2^\mathbb{N} \to 2^\mathbb{N}$ in a constructive type theory with quotients, right?)
Now my question is as follows:
- Does it seem that the induced topological structure on quotient spaces in constructive type theory is actually the condensed set structure of Clausen and Scholze?
Here are some ways to make my question more formal:
- Consider the quotient space $2^\mathbb{N} / \text{fin}$ of all binary sequences, mod two sequences being equivalent if they agree on all but finitely many sequences. Can we (in say HoTT with univalence, or MLTT with quotients) construct a term for a function $f : 2^\mathbb{N} / \text{fin} \to 2^\mathbb{N} / \text{fin}$ which is not a condensed set endomorphism? I assume not.
- Is it possible to make this “induced topology” theory formal? For example, I’ve heard folks say that it is consistent with constructive mathematics that every function is continuous, but I don’t know what that means formally. For example, can we add an axiom to MLTT or some other type theory that says that every $f : A \to B$ is continuous for the induced topologies on $A$ and $B$? Or better, is there a topos model of MLTT where the types are topological spaces and the functions are continuous? (Sorry, if I’m not using the right terms here. I’m still getting used to categorical logic.)
- If there is a way to make this formal, can this formalism be extended to type theories with quotients, and then can one replace topological spaces with condensed sets?
- (Bonus) In HoTT, if indeed, one can endow all sets (homotopy 0-types) with a condensed set structure, what about higher homotopy types? If the sets can be though of as condensed sets, can say the n-groupoids be interpreted as condensed n-groupoids and so forth?