In order to maintain consistency with the clock irrelevance axiom, universes in CloTT are indexed by
clock contexts. To see why this is necessary, note that
naively adding a closed universe \(\operatorname{U}_{}\) , with a map \(\triangleright : \operatorname{U}_{} \rightarrow \forall \kappa . \operatorname{U}_{}\) ,
the clock irrelevance principle would state that the type operation \(\triangleright ^\kappa (-)\)  would
be independent of \(\kappa \)  on small types.
With the subscripting, the type operation \(\triangleright \)  can be restricted on \(\operatorname{U}_{\Delta }\)  to the \(\kappa \in \Delta \)  avoiding this problem.
Note that the formulation of CloTT used here differs from that presented in [1]}, which for simplicity used a single
universe but retained consistency since the clock irrelevance axiom was not modelled (although mentioned in the paper). The presentation
of universes used here follows that of GDTT [2]}, [3]}, but extends it with ticks.
