open import Cat.Displayed.Univalence.Thin
open import Cat.Displayed.Total
open import Cat.Instances.OFE
open import Cat.Prelude

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.

open OFE-Notation

module _ {β„“a β„“b β„“a' β„“b'} {A : Type β„“a} {B : Type β„“b} (O : OFE-on β„“a' A) (P : OFE-on β„“b' B)
  where
  private
    instance
      _ = O
      _ = P
    module O = OFE-on O
    module P = OFE-on P

  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
  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)