关于拓扑斯中集合族{sᵢⱼ}的研究成果与趋势问询

大家好，我最近在探索拓扑斯和同伦类型论（HoTT）的交叉领域，先跟大家梳理下我的思考背景：

假设$X$是某个空间，$T$是$X$上的拓扑斯（比如Grothendieck拓扑斯）。拓扑斯$T$是由层${S_i}$构成的范畴，每个层$S_i$会把$X$的每个开子集$O_j$映射到集合$s_{ij}$——这么看的话，拓扑斯$T$本质上就是集合族${s_{ij}}_{ij}$。

在HoTT领域有个很有意思的例子：$T$可以作为某个特定HoTT理论$Th$的模型。理论$Th$由依赖类型（语境中的类型）及其项组成，$T$中的每个层$S_i$对应建模某个类型$Type_i$：这个层会给每个语境$j$指派一个集合$s_{ij}$，它的截面就是$Type_i$在语境$j$中的项。所以理论$Th$的模型拓扑斯$T$同样是这样的集合族$s_{ij}$。

这让我对集合族${s_{ij}}$产生了研究兴趣，我有几个基础疑问：

• 这个集合族${s_{ij}}$本身是一个范畴吗？
• 这些集合之间，甚至集合里的点之间，存在几何相关的联系吗？

显然${s_{ij}}$应该有非常丰富的结构：

• 当索引$i$固定（对应某个层$S_i$）时，集合族${s_{ij}}_j$由层的粘合条件决定，而粘合条件又受$X$的底层对象/子集关系影响；
• 另一方面，索引$j$对应开集$O_j$，所以对固定的$i$，$s_{ij}$和$s_{ik}$之间也应该存在关联。

我的核心问题是：目前关于集合族${s_{ij}}$有没有相关的研究成果，或者正在发展的研究趋势？

我知道HoTT被看作数学的替代基础，这个问题可能有点大胆（甚至有点蠢），但其实我的诉求更务实：我很认同《Modal Homotopy Type Theory》里用HoTT做知识表示的思路，想把相关方法应用到更简单的、甚至离散的类型上。当然，这背后也可能藏着深刻的数学内容——比如有研究证明所有可能的HoTT理论构成的范畴具有模型范畴的模型结构；如果用$k$表示理论的模型、$l$表示该理论模型的模型（当然如果考虑模型的分类拓扑斯，这层结构可能会坍缩），那甚至会出现更复杂的集合族${s_{kl,ij}}$，对应任意理论、模型、类型、语境的集合集合。

希望了解相关领域的朋友能给我一些指引！

备注：内容来源于stack exchange，提问作者TomR