A notion of semi-cubical tribe

Abstract

The important notions our ideas revolve around are that of tribes, a class of categories aiming at modeling intensional type theory, and that of semi-cubical objects, for a category of cubes with symmetries and reversals. We introduce a general notion of $J$-tribes, tribes suitably enriched in presheaves over $J$, and $J$-frames in a tribe $\mathcal{T}$ as a category of $J$-shaped resolutions in $\mathcal{T}$, for a direct category $J$, and we construct the $J$-tribe of $J$-frames in $\mathcal{T}$. Similar notions of $R$-tribes and $R$-frames are introduced for $R$ a suitable generalized direct category, and corresponding properties are established thanks to a construction relating $R$ to a strictly direct category. In particular, our framework applies to semi-cubes, which is our main motivation, and yields an appropriate notion of a semi-cubical tribe.