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 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.
Cite
@article{arxiv.2401.00512,
title = {A parametricity-based formalization of semi-simplicial and semi-cubical sets},
author = {Hugo Herbelin and Ramkumar Ramachandra},
journal= {arXiv preprint arXiv:2401.00512},
year = {2025}
}
Comments
Version corresponds to the published version (though with a different formatting). Associated formalization in Coq at https://github.com/artagnon/bonak