A parametricity-based formalization of semi-simplicial and semi-cubical sets

Abstract 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 their 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.