I cannot understand the homotopy type theory book. It just makes no sense to me, sorry.
> The logic of toposes is higher order intuitionistic logic.
Yes, I have read that a lot. Eventually, I would like to understand how toposes form a model of higher-order intuitionistic logic (which is what "The logic of toposes is higher order intuitionistic logic" probably means?). But first, I would like to understand what a topos is in first-order logic terms. You know, baby steps.
The category of sets is a topos and can be expressed/presented with first order classical logic but the general logic of toposes is intuitionistic and non-classical. There is no single topos with a single logic, each topos has its own logic and the common thread is that they're non-classical and higher order.
So are you saying that "T is a topos" cannot be expressed via first-order classical logic? Unlike something such as "G is a group", or "T is a topology" or "C is a category"?
None of your examples are expressible in first order logic either. Those are all instances of mathematical structures which can be formalized in different toposes with different logics.
Groups in the topos of sets are different from groups in the topos of smooth sets. The structure of a group can be expressed as a diagram which can then be interpreted in any topos with the prerequisite mathematical structures. Toposes have products (finite limits) so every topos can potentially have group objects just like every topos can have a natural number object which is an initial algebra (colimit) for a certain diagram.
In any case, there is no royal road and if you're not willing to spend the time and effort to learn what others have written about toposes then there isn't much I can help you with here. There are no royal roads in mathematics.
Oh, I see what you mean. You mean that for the definition of groups, topology, etc. I need to refer to a mathematical theory like set theory within first-order logic. Ok, let's do that. But then there is a definition of what "T is a topos" means, in terms of set theory based on first-order logic, right? Obviously, that definition cannot include the category of sets, because that category wouldn't be a set itself, so I am fine with considering only "small" toposes which are representable as sets, just as I am fine with just considering "small" groups, "small" topologies, and "small" categories.
So what is your question? The standard definition of a topos spells out the structural constraints for subobject classifier, finite limits, and Cartesian closure. You can write out these definitions for the topos of sets and any "small" structures in your topos which are points of the specified logical/structural variety will be small toposes internal to the topos of sets.
But there are royal roads. I mean, that is what mathematics is all about, finding those royal roads. We just may not know them yet. I doubt that topos theory is a royal road. But it is at least one of these dirty side roads I need to travel to get to the royal road.
> The logic of toposes is higher order intuitionistic logic.
Yes, I have read that a lot. Eventually, I would like to understand how toposes form a model of higher-order intuitionistic logic (which is what "The logic of toposes is higher order intuitionistic logic" probably means?). But first, I would like to understand what a topos is in first-order logic terms. You know, baby steps.