module Cat.Instances.OFE.Closed where

Function OFEs🔗

If and are OFEs, then so is the space of non-expansive functions this makes the category OFE into a Cartesian closed category.

  Function-OFE : OFE-on (ℓa  ℓb') (O →ⁿᵉ P)
  Function-OFE .within n f g =  x  f .map x ≈[ n ] g .map x
  Function-OFE .has-is-ofe .has-is-prop n x y = hlevel 1
    where open OFE-H-Level P
  Function-OFE .has-is-ofe .≈-refl n x  = P.≈-refl n
  Function-OFE .has-is-ofe .≈-sym n p x = P.≈-sym n (p x)
  Function-OFE .has-is-ofe .≈-trans n p q x = P.≈-trans n (p x) (q x)
  Function-OFE .has-is-ofe .bounded f g x = P.bounded (f .map x) (g .map x)
  Function-OFE .has-is-ofe .step n f g α x = P.step n (f .map x) (g .map x) (α x)
  Function-OFE .has-is-ofe .limit f g α = Nonexp-ext λ x 
    P.limit (f .map x) (g .map x)  n  α n x)