We explain how to construct in two different ways a cartesian closed fibration of higher-order regular languages in the sense of Salvati. In the first construction, we use fibrational techniques to derive the cartesian closed fibration from the various categories of regular languages of $λ$-terms associated to finite sets of ground states. In the second construction, we take advantage of the recent notion of profinite $λ$-calculus to define the cartesian closed fibration by a change-of-base from the fibration of clopen subsets over the category of Stone spaces, using an elegant idea coming from Hermida. We illustrate the expressive power of the cartesian closed fibration by generalizing the notion of Brzozowski derivative to higher-order regular languages, using an Isbell-like adjunction in the sense of Melliès and Zeilberger.

翻译：我们阐述了如何以两种不同方式构建Salvati意义下的高阶正则语言的笛卡尔闭纤维化。在第一种构建方法中，我们运用纤维化技术，从与有限基态集相关联的λ项正则语言的各类范畴中推导出笛卡尔闭纤维化。在第二种构建方法中，我们利用近期提出的profinite λ-演算概念，通过从Stone空间范畴上的闭开子集纤维化进行基变换来定义笛卡尔闭纤维化，这一优雅思路源自Hermida。我们通过将Brzozowski导数的概念推广到高阶正则语言，展示了该笛卡尔闭纤维化的表达能力，其中运用了Melliès和Zeilberger意义上的Isbell型伴随关系。