Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of n-simplices or n-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call indexed. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.

翻译：半单纯集与半立方集通常定义为分别在半单纯范畴或半立方范畴上的预层。同伦类型论随后推广了一种替代定义，将n-单纯形或n-立方体集合重新组织为其面上的纤维族，从而产生一种我们称之为索引式的刻画。此外，已知半单纯集与半立方集分别与单变体和二变体形式的迭代Reynolds参数性相关。我们利用这种对应关系，开发了增广半单纯集与半立方集的一种统一索引式定义，并在Coq中对其进行了完整形式化。