Let $X$ be some space and let $T$ be topos on $X$ (e.g. Grohtendieck topos on the topological space).
Topos $T$ is the category of sheaves ${S_i}$, where each sheaf $S_i$ maps each open subset $O_j$ of $X$ into set $s_{ij}$. So, the topos $T$ essentially is the collection of sets $\{s_{ij}\}_{ij}$.
There is nice example in the realm of Homotopy Type Theory. $T$ can be topos as some particular model of some particular HoTT theory $Th$. Theory $Th$ consists of dependent types (types in the context) and their terms. Each sheaf $S_i$ of $T$ models some type $Type_i$: this sheaf assigns to each context $j$ some set $s_{ij}$ whose section is the terms of $Type_i$ in the context $j$.
So, the model topos $T$ of theory $Th$ is collection $s_{ij}$ as well.
This motivates me to research this collection $s_{ij}$? Is it category? Are there any relationships (geometric relationships) among those sets or even the points in those sets? Apparently there should be really rich structure on $s_{ij}$. As index $i$ denotes sheaf, then the collection $\{s_{ij}\}_{j}$ for particular sheaf $S_i$ is determined by the gluing conditions of the sheaf which is impacted by the underlying object/subset relations of $X$. Form the other hand, index $j$ denotes the open set $O_j$ and so $s_{ij}$ and $s_{ik}$ should be related as well for fixed $i$.
My question is - are there any results, research trend for $\{s_{ij}\}$?
I am aware the HoTT is conceived as the alternative foundation of math and my question can be courageous (or silly). But actually I am more modest - I like idea about the use of HoTT in the knowledge representation in the approach of https://global.oup.com/academic/product/modal-homotopy-type-theory-9780198853404?cc=us&lang=en& and that means that I would like to apply my approach to more modest, maybe even discrete types. But of course, it can be possible, that deep mathematics can be uncovered as well. E.g. there is an article about the category of all possible HoTT theories https://www.sciencedirect.com/science/article/pii/S0001870818303062 (it proves that such category have the model structure of the model categories), so, if $k$ models theory, $l$ models the model of this theory (of course this can be collapsed if we consider classifying topos of models), then there is even the more complex structure $\{s_{kl,ij}\}$ which is the collection of the sets for any theory, model, type, context.