Our motivation for constructing this model is to study extensions of CloTT. In particular, we would like to extend CloTT with
path types as in [1]}. This requires an adaptation of the model to the cubical setting,
using \(\mathbb {T}\) -indexed
families of cubical sets [2]} rather than just sets. The resulting variant of CloTT should be closer to the intensional type theory presented
in [3]} than the extensional type theory modelled here. For example, fixed
points should unfold only up to path equality. We also hope that formulating the clock irrelevance
axiom using path equality the universes can be modelled differently, simplifying the perhaps
most technical part of the present model construction.
