Are the “topologies” arising from constructive type theories with quotients actually condensed sets? 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?

 A: Not quite a complete answer, but:
There are models of constructive mathematics where sets are $T_0$ second-countable (optionally zero-dimensional) topological spaces equipped with equivalence relations, morphisms are continuous maps which respect the equivalence relation, and pointwise-equivalent morphisms are equal. In these two models, quotients are taken simply by inflating the equivalence relation, and the result satisfies all of the usual rules of MLTT + Quotient Types. (We need to add an equivalence relation structure so that the quotients are well-behaved enough for exponents to exist.)
In particular, each functions $f : 2^{\mathbb{N}}/\operatorname{fin} \to 2^{\mathbb{N}}/\operatorname{fin}$ arises from some continuous function $g:2^{\mathbb{N}} \to 2^{\mathbb{N}}$
These models don't have a set of truth values (hence no power-set operation), but they can be upgraded to contain one. (Roughly speaking - the above models arise as categories of PERs over two different PCAs, and there's a general technique for upgrading these, called realisability topoi.) This is the smallest change I know to the category of topological spaces that results in a model of MLTT.

As for what "every function is continuous" means - there are three ways that I know of. The first is, to every set, assign a topology (we could say that the opens are the unions of preimages of arbitrary functions into $\mathbb{R}$, for instance), and then every function is continuous with respect to this topology. This could also be done in classical mathematics, but there all sets would be given the discrete topology. Constructively, it may be the case that we get nontrivial topologies, and may even happen to get the 'correct' topologies for spaces such as $2^{\mathbb{N}}$ or $\mathbb R$.
The second way gives a number of examples where this holds. It is consistent that all functions $2^{\mathbb{N}} \to \mathbb{R}$ are continuous. In the presence of countable choice (which is consistent with this; iirc both (and MP, mentioned below) hold in Johnstone's topological topos, which has FirstCountableTop as a full subcategory and which I suspect is a full subcategory of that of condensed sets), this implies the stronger theorem that If $M$, $N$ are metric spaces with $M$ complete, then all functions $f:M \to N$ are continuous. (If MP ($\not \geq_{\mathbb{R}}$ implies $<_{\mathbb{R}}$) holds, we can weaken "complete" to "complement of a subset of a complete metric space".)
The third way is to generalise to grothendieck topologies, which is the main way to make (grothendieck) topoi, which model MLTT + quotients. Here, we specify a small category of "test spaces" and specify some families of morphisms to be "coverings" (for example, we could take all compact second-countable spaces for test spaces, and finite joint surjections as coverings) satisfying some technical conditions. The resulting grothendieck topos includes the spaces from the test category, and doesn't add any new morphisms between them - so if all of your morphisms between test spaces were continuous, they will continue to all be in the larger topos. The condensed sets are formed very similarly to this, except that the category of test spaces is no longer small, so we need to deal with size issues to get a grothendieck topos, like Simon mentioned.
