  This is the third in a series of papers extending Martin-L\"of's meaning
explanations of dependent type theory to a Cartesian cubical realizability
framework that accounts for higher-dimensional types. We extend this framework
to include a cumulative hierarchy of univalent Kan universes of Kan types,
exact equality and other pretypes lacking Kan structure, and a cumulative
hierarchy of pretype universes. As in Parts I and II, the main result is a
canonicity theorem stating that closed terms of boolean type evaluate to either
true or false. This establishes the computational interpretation of Cartesian
cubical higher type theory based on cubical programs equipped with a
deterministic operational semantics.
