XTT and Computational Bishop Sets

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Opening obstruction

Cartesian cubes support paths and univalence, but a computational theory of sets asks additionally for exact equality reflection at a controlled h-level.

Development contract

Define XTT’s dimensions, coercion/composition, exact equality and universe of Bishop sets; prove canonicity at the published calculus and compare it with Cartesian cubical type theory without theorem transfer.