Guarded Cubical Type Theory

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

Opening obstruction

Guarded recursion supplies delayed fixed points and cubical paths supply extensional equality, but combining them requires clocks to commute coherently with composition.

Development contract

Develop the published guarded-cubical syntax and model, prove its fixed-point/path principles and stated canonicity or consistency boundary, and keep it separate from ordinary Cartesian cubical theory.