This is a great question. I think a proof of $\top \vdash \exists x (SS0 = x + x)$ is as follows. The trick is to start with the identity $\exists x...

My guess is that you can formulate and prove the isomorphism theorems in intuitionistic higher logic, and that they then automatically hold in any top...

I think this is a very interesting topic. One remark is that a lot of the typical results about groups involve multiple groups and morphisms between t...

Hi @orlando, Great! Your calculations made me think that this Grothendieck topology (the smallest Grothendieck topology such that $U \to 1$ is a cov...

The more general context is interesting, in topos theory terminology you showed above that the classifying topos of $\mathbb{F}_2$-algebras is an open...

Hi @orlando, I agree that the two toposes agree. An alternative proof would be to use the Comparison Lemma, as follows. The morphism $R \to R/2R$ ge...

Hi @orlando, The constructions you are describing about the tangent bundle make a lot of sense, and it looks interesting to replace the ring object ...

Hi! To show injectivity: if $\mathbb{Z} \to \mathbb{Z}[x,y](x^2+y^2=3)$ is not injective, then $(x^2+y^2-3)$ would contain a nonzero integer $n$. But ...

Thanks, I understand now what you mean with the remark. And yes, the generic model will be the sheafification of the original generic model. The reaso...

Hi @orlando,Nice example. I agree with your notation, and I agree that the sieve generated by $R \to R[a,b]/(a^2+b^2=1)$ is a covering sieve for the c...

@elio-pivet Yes, I agree, I didn't notice that part. In the notation of page 281, the model $M_{\{e . e^2=e\}}$ should for example correspond to the r...

I'm still learning about this, but here are some ideas. First, we need to translate the axioms that you suggest to geometric sequents. In axioms for...

Hi! Topological spaces can often be interpreted as solutions to classification problems. For example, the complex projective line "classifies" lines...

I agree that sheafification will not give an essential subtopos if the boolean algebra is not atomic. A proof is as follows. If the subtopos is essent...

Thanks! I didn't know Zoonekynd's thesis was available online. I can recommend his paper "The Fundamental Group of an Algebraic Stack". There the ba...