Hello, thank you all for a very nice conference so far!

I would like to have some follow up on the question I asked professor Lafforgue about deriving results which should be valid for models in any category with enough structure. I asked about whether it would be worth it (for a non-logician) to go into the syntactic level to prove for example the isomorphism theorems of group theory, since this is supposed to be doable and these results are obviously of interest in diverse categories (not necessarily toposes, say in topological spaces, manifolds, schemes), or whether this level is so messy that it would not be worth it so that it would still be easier to derive the results individually. Lafforgue seems to think that it is not worth it to go to this level, so that perhaps non-logicians should keep working only on the semantic level (this might be an interesting discussion on its own), but instead referred to the world of classifying toposes, which would suit better since this is an object in the world of semantics. However, i do not yet understand this so well so I ask some naive follow up questions for those of you who actually know the subject we are dealing with:

- Is it somehow possible to derive the results for models of the theory in categories with weak structure, having only finite products, by proving them in the world of the classifying topos? If not, is it possible at least if the category is a topos, so that we can for example get the same standard algebraic results when working with sets, sheaves or sets acted on by a group?

- Are there other ways of doing it with only one proof when we just work semantically? I am not interested in working axiomatically with the formalism of ''group objects in a category'' since this is again very messy.

I am sorry about bothering the conference with things which should be obvious, but the first part is supposed to be a school to learn the subject after all, hehe.

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 them. On the other hand, the theory of groups features statements about a single group, and elements in this group.

A typical first order statement in the theory of groups would be $a^2 =1, a^3 =1 \vdash a=1$, so a statement about elements of the group rather than various different groups and their interactions.

I don't think the isomorphism theorems can be formulated in the first order theory of groups.

@jens-hemelaer My thoughts about this was based mainly on the comments made by professor Caramello in her course at topos à IHES ( https://www.youtube.com/watch?v=P5Mx7fwYVws around 18.00) where she says that very general facts can be retrieved at the semantic level, Pierre Cartier explicitly asks about isomorphism theorems where she says ''yes for instance'' so this is why I thought it should be doable and was thinking about if it's a practically nice way to work, maybe it's true they can't be formulated though.

Either way I understood now much better what Lafforgue was talking about since we have the theorem that a formula is provable on the syntactic level if and only if it is true in the universal model of the classifying topos, which seems like a much nicer way to work, even better since the theory is of presheaf type so that makes me wonder if you can translate this universal model together with an equivalence of toposes so as to be able to look at these questions for example in this category of presheaves of finetely presented set-based models, or one of the other nice examples? It would be nice to be able to prove in a setting like this, to then be able to conclude that it is provable on the syntactic level so that therefore it must be valed in models in any category with finite products.

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

But I'm not an expert on this, so I would be interested in hearing others confirm this. And maybe there is a way in which this connects back to first order geometric theories and classifying toposes.