These sorts of answers that usefully supplement another answer (even if not directly addressing the OP's question) have typically been accepted by the community as worth keeping around, and so I think we can let it stand, if only for the sake of getting the poster to the 50-point threshold (so that next time he/she can comment instead).

(Okay, it seems the OP has tried to ask this question twice before; the first time it was closed with one reason being that more details are needed. I believe that OP is trying in good faith to provide details; the problem is in the deleting and then reasking in another post. Technically, this is a site violation.) To the OP: in future, please do not delete and reask; instead, edit the original question to improve it.

@MatthévanderLee How is your comment responsive to Matt's point that Hilbert's system is not first-order? The archimedean and completeness axioms in Hilbert's system fall outside Tarski's system (and so cannot be deduced therein).

Most of Blass's paper however is simply brimming with meaningful and rigorous combinatorial (and later, logical) considerations. I think of it as being more "fun" than actually "quirky".

Where do you see in the nLab the claim that $Bool^{op} \to Set$ is monadic?

I'd say there's no question this meets the cuteness criterion.

Regarding the conjecture: it turns out that all closed subgroup inclusions between compact Hausdorff groups are equalizers. This is shown in D. Poguntke, Einige Eigenschaften des Darstellungsringes kompakter Gruppen, Math. Z. 130, 107-117 (1973) (link: pub.uni-bielefeld.de/download/1775049/2311754); see Satz 1.3 and Bemerkung 1.4, page 109.

You have your answer now. Please don't use the bounty system to evade normal community moderation. As has been pointed out, the question probably won't be considered appropriate for this site, and so if the community wants to close it, they should be allowed to.

What does "normal" mean in this context?

niran90, I would delete the duplicate at math.se since it's been answered here. Then, if I were you, I would post the smooth bijection question over there first, and wait some days for a response. If there is none, you can try asking here (although it might easily be closed as off-topic for this site).

I'm voting to close this question as off-topic because it was simultaneously asked at Mathematics (no cross-posting, please). If after a week there is no answer there, it may be asked here. (Update: there was an answer at math.se: see math.stackexchange.com/questions/3503269/…)

@mattecapu I may have meant to say (but didn't) that since we have $Set/X \simeq (Set/Y)/f$, we just relativize the object of sections construction, replacing $Set$ in the first construction by a new base topos $Set/Y$, and replacing $X$ by $f$. Thus we just internalize the first construction to the new base topos. In effect, $\prod_f: (Set/Y)/f \to Set/Y$ is a bundle of instances of the first object of sections construction parametrized over $y \in Y$, each of the form $\prod_{X_y}: Set/(X_y) \to Set$ where $X_y$ is the fiber $f^{-1}(y)$. This gives $\prod_{x \in f^{-1}(y)} p^{-1}(x)$.

There's a 5-minute window for combining multiple edits into one.

There have been numerous edits in a short span of time. Please be aware that every edit bumps the post to the top of the stack, and pushes off the front page other questions that are vying for attention.

Graham's number is not a good example; it was a number he made up during an interview with Martin Gardner, and was not used in a serious mathematical proof. See here en.wikipedia.org/wiki/Graham%27s_number#Publication or for that matter here mathoverflow.net/a/118650/2926