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

arrow
Paris

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

/logic/semi-ntypes/1.png /logic/semi-ntypes/2.png