The main challenge when adapting the model of [1]} to CloTT is to model ticks, which were not present
in the language modelled in [1]}. In particular, how does one model tick assumptions of the form
\(\alpha : \kappa \)  in a context, when there appears to be no object of ticks in the model to be used as the
denotation of the clock \(\kappa \) ? In this paper we observe that these assumptions can be modelled using a left adjoint
\(\operatorname{\blacktriangleleft }^\kappa \)  to the functor \(\operatorname{\blacktriangleright }^\kappa \)  used in [1]} to model the delay modality \(\triangleright ^\kappa \) 
associated to the clock \(\kappa \) . Precisely we model context extension as \({\llbracket \Gamma , \alpha : \kappa  \rrbracket } =\operatorname{\blacktriangleleft }^\kappa {\llbracket \Gamma  \rrbracket }\) . The modality \({\triangleright }\, (\alpha :\kappa ) .A\)  is then modelled as a dependent right adjoint
to \(\operatorname{\blacktriangleleft }^\kappa \) ,
a notion studied in detail in [4]}: If \(\mathcal {C}\)  is a category with family (CwF) [5]} (a standard notion of model
for dependent type theory) and \(L\)  an endofunctor on (the underlying category of) \(\mathcal {C}\) , a dependent right
adjoint to \(L\)  is an operation mapping a family \(A\)  over \(L\Gamma \)  to a family \(RA\)  over \(\Gamma \)  with a bijective
correspondence between elements of \(A\)  and elements of \(RA\)  natural in \(\Gamma \) . Dependent right adjoints model
Fitch-style modal operators in type theory, a general pattern seen also in the model of fresh name abstraction of
FreshMLTT [6]} and dependent path types in cubical type theory [7]}.
In CloTT the type operator \(\triangleright \)  is indexed by clocks, and since the model has an object of clocks
this can be understood as an internally indexed family of Fitch-style modal operators. We show how to model this as a dependent
right adjoint on the slice category over the object of clocks.
