module Cat.Instances.OFE.Later where

The “Later” OFE🔗

Given a OFE we define an OFE the later modality of systems of guarded recursion. The idea is that is like but we have to wait a bit to think about it: at level zero, is an indiscrete blob, but at positive time steps, it looks just like

The construction extends to an endofunctor of OFE, equipped with a natural transformation expressing that if we have something now, we can very well stop thinking about it for a step. This natural transformation actually has a universal property, within the category of OFEs: Non-expansive maps are equivalent to contractive maps

To emphasize that the distinction between and is entirely in skipping a step, we have formatted the construction below so the cases are split between time zero and positive time.

  Later : OFE-on ℓ' A
  Later .within zero x y    = Lift ℓ' 
  Later .within (suc n) x y = x ≈[ n ] y

  -- Trivial!
  Later .has-is-ofe .has-is-prop zero = λ _ _ _ _ _  _
  Later .has-is-ofe .≈-trans     zero = _
  Later .has-is-ofe .≈-refl      zero = _
  Later .has-is-ofe .≈-sym       zero = _
  Later .has-is-ofe .step        zero = _

  -- Just like A!
  Later .has-is-ofe .has-is-prop (suc n) = P.has-is-prop n
  Later .has-is-ofe .≈-trans     (suc n) = P.≈-trans     n
  Later .has-is-ofe .≈-refl      (suc n) = P.≈-refl      n
  Later .has-is-ofe .≈-sym       (suc n) = P.≈-sym       n
  Later .has-is-ofe .step        (suc n) = P.step        n

  Later .has-is-ofe .bounded x y = _
  Later .has-is-ofe .limit x y a = P.limit x y λ n  a (suc n)
 :  { ℓ'}  OFE  ℓ'  OFE  ℓ'
 (A , O) = from-ofe-on (Later O)

to-later :  { ℓ'} (A : OFE  ℓ')  OFEs.Hom A ( A)
to-later A .hom x = x
to-later A .preserves .pres-≈ {n = zero} α  = lift tt
to-later A .preserves .pres-≈ {n = suc n} α = A .snd .OFE-on.step n _ _ α

The universal property promised, that represents the contractive maps with domain is a short exercise in shuffling indices:

    : (f : A  B)
     is-non-expansive f (Later P) Q  is-contractive f P Q
  later-contractive f = prop-ext! {A = is-non-expansive _ _ _} {B = is-contractive _ _ _}
     { r .contract {n = n} α  r .pres-≈ {n = suc n} α })
     { r .pres-≈ {n = zero} α   Q.bounded _ _
       ; r .pres-≈ {n = suc n} α  r .contract α

We can put this together to define something akin to Löb induction: if is an inhabited, complete OFE, Banach’s fixed point theorem implies that non-expansive functions have fixed points.

  löb :  A   is-cofe P  (f : Later P →ⁿᵉ P)  Σ A λ x  f .map x  x
  löb pt lim f = banach P lim pt record {
    contract = λ n p  f .pres-≈ (suc n) p }