An indexed construction of semi-simplicial and semi-cubical sets

The formalization effort is complete, and the journal paper is currently in preparation. Here's an early preview of the core of the construction.