作为合成微分凝聚同伦类型论中微线性类型的轨形

非正式地，轨形是一种光滑空间，其点可能具有有限个内部对称。然而，形式上，轨形的概念已以多种不同面貌呈现——从 Satake 的 V-流形到 Moerdijk 和 Pronk 的恰当 étale 群胚——这些在表面上并不类似非正式定义。这种形式与直觉的背离原因在于，在传统集合层级的奠基中，空间的点不能具有内部对称。这些对称的额外数据必须在整个理论中携带并得以解释。更根本地，以通常方式呈现的轨形之间的映射无法逐点定义。在本文中，我们提出合成微分凝聚同伦类型论中的轨形定义：轨形是一种微线性类型，其中任意两点间恒等类型恰当有限。在同伦类型论中，类型的点可具有内部对称，我们将能通过直接定义其点类型来构造轨形实例。此外，两轨形间的映射空间仅是函数类型。我们将通过在内证明每个恰当 étale 群胚都是轨形，来证成此合成定义。由此，我们将表明合成理论忠实地扩展了通常的轨形理论。在此过程中，我们将研究高阶类型（如 étale 群胚）的微线性，表明合成微分几何的方法优雅地推广到光滑空间的高阶类比。我们还将研究合成微分几何中 Dubuc-Penon 与开覆盖紧性定义的关系，并证明第二可数流形的任意离散 Dubuc-Penon 紧子集是可子有限枚举的。