Changes to Later.agda: add dependent force function (where the type can mention the clock); remove "global" clock-irrel axiom, instead axiomatize it on a per-type basis