open import Cat.Instances.OFE
open import Cat.Prelude

open import Data.Nat.Order
open import Data.Nat.Base

module Cat.Instances.OFE.Complete where

open OFE-Notation

module _ {ℓ ℓ'} {A : Type ℓ} (P : OFE-on ℓ' A) where
  private
    instance _ = P
    module P = OFE-on P

Limits and complete OFEs🔗

Since OFEs are metric-space-like¹ structures, there is a natural notion of sequences getting closer to a value: we say a sequence $f:\mathbb{N}\to A$ is a chain if, given $n\le m\text{,}$ we have $f(m)\stackrel{n}{\approx }f(n)\text{.}$ Looking at the case where $m=1+n\text{,}$ this says that we have a sequence

where the metric interpretation of OFEs lets us read this as the distance between successive points approaching ${\lim }_{n\to \infty }{2}^{-n}=0\text{.}$

  is-chain : (x : Nat → A) → Type _
  is-chain f = ∀ m n → n ≤ m → f m ≈[ n ] f n

However, in a general OFE, there is not necessarily anything “at $\infty$”: the values of the sequence get closer to each other, but there’s no specific point they’re getting closer to. An example of chain without limit is as follows: let $a:A$ be an element of a set, and consider the sequence

in the OFE of finite sequences. Clearly this satisfies the chain condition: w.l.o.g. we can assume $m=n+k$ for some $k\text{,}$ and $f(n+k)$ certainly shares the first $n$ elements with $f(n)\text{.}$ However, there is no single list of $A\text{s}$ $l$ which shares its first $n$ elements with $f(n)\text{:}$ $l$ must have a definite length, independent of $n\text{,}$ which bounds the size of its prefixes. Choosing any $n>\mathrm{length}(l)$ results in a value of $f(n)$ has more elements than the length-$n$ prefix of $l\text{.}$

The previous paragraph contains an unfolding of the definition of a sequence having a limit, or, more specifically, it contains a definition of what it means for a point to be the limit of a sequence: $a$ is the limit of $f$ if, for all $n\text{,}$ $a\stackrel{n}{\approx }f(a)\text{.}$

  is-limit : (x : Nat → A) → A → Type _
  is-limit f a = ∀ n → a ≈[ n ] f n

It follows at once that the limit of a sequence is uniquely determined: if $a$ and $b$ both claim to be limits of $f\text{,}$ we have, for arbitrary $n\text{,}$ $a\stackrel{n}{\approx }f(a)\stackrel{n}{\approx }b\text{,}$ meaning $a=b\text{.}$

  limit-is-unique
    : ∀ (f : Nat → A) {x y}
    → is-limit f x → is-limit f y → x ≡ y
  limit-is-unique f l1 l2 = P.limit _ _ λ n →
    P.≈-trans n (P.≈-sym n (l2 n)) (l1 n)

  Limit : (Nat → A) → Type _
  Limit f = Σ A (is-limit f)

  Limit-is-prop : (f : Nat → A) → is-prop (Limit f)
  Limit-is-prop f (a , α) (b , β) = Σ-prop-path! (limit-is-unique f α β)

  limit-from-tail
    : ∀ (f : Nat → A) x → is-chain f → is-limit (λ n → f (suc n)) x → is-limit f x
  limit-from-tail f x chain lim zero = P.bounded _ _
  limit-from-tail f x chain lim (suc n) = P.≈-trans _
    (chain (suc (suc n)) (suc n) (≤-sucr ≤-refl))
    (lim (suc n))

  limit-to-tail
    : ∀ (f : Nat → A) x → is-chain f → is-limit f x → is-limit (λ n → f (suc n)) x
  limit-to-tail f x chain lim zero = P.bounded _ _
  limit-to-tail f x chain lim (suc n) = P.step _ _ _ (lim _)

However, some OFEs do have limits for all chains: the OFE of infinite sequences is one, for example. We refer to such an OFE as a complete ordered family of equivalences, or COFE² for short.

  is-cofe : Type _
  is-cofe = ∀ (f : Nat → A) → is-chain f → Limit f

module _ {ℓ} {X : Type ℓ} (X-set : is-set X) where

We can actually compute the limit of a sequence of sequences pretty easily: we have a function $s:\mathbb{N}\times \mathbb{N}\to A\text{,}$ our sequence, and the chain condition says that, given $j\le i$ and $k<j\text{,}$ we get $s(i,k)=s(j,k)\text{.}$ Our limit is the sequence $l(i)=s(1+i,i)\text{:}$ we must show that $l\stackrel{n}{\approx }s(n)\text{,}$ which means that, given $k<n\text{,}$ we must have $s(1+k,k)=s(n,k)\text{.}$ This follows by the chain condition: $k<1+k\text{,}$ and $(1+k)\le n\text{,}$ so we conclude $s(1+k,k)=s(n,k)\text{.}$

  Sequences-is-cofe : is-cofe (Sequences X-set)
  Sequences-is-cofe seq chain = (λ j → seq (suc j) j) , λ n k k<n →
    sym (chain _ _ k<n _ ≤-refl)

module _ {ℓa ℓa' ℓb ℓb'} {A : Type ℓa} {B : Type ℓb} (P : OFE-on ℓa' A) (Q : OFE-on ℓb' B) where
  private
    instance
      _ = P
      _ = Q
    module P = OFE-on P
    module Q = OFE-on P

In passing, let us note that non-expansive maps preserve both chains and their limits.

  non-expansive→chain
    : (f : A → B) (s : Nat → A)
    → is-non-expansive f P Q → is-chain P s → is-chain Q (λ n → f (s n))
  non-expansive→chain f s ne p m n n≤m = ne .pres-≈ (p m n n≤m)

  non-expansive→limit
    : (f : A → B) (s : Nat → A) (x : A)
    → is-non-expansive f P Q → is-limit P s x → is-limit Q (λ n → f (s n)) (f x)
  non-expansive→limit f s x ne lim n = ne .pres-≈ (lim n)

Banach’s fixed point theorem🔗

module _ {ℓ ℓ'} {A : Type ℓ} (P : OFE-on ℓ' A) (lim : is-cofe P) where
  private
    instance _ = P
    module P = OFE-on P

Banach’s fixed point theorem, in our setting, says that any contractive $f:P\to P$ on an inhabited COFE has a unique fixed point. We’ll start with uniqueness: suppose that some $a,b$ satisfy $f(a)=a$ and $f(b)=b\text{.}$ It will suffice to show that $f(a)=f(b)\text{,}$ and, working in an OFE, this further reduces to $f(a)\stackrel{n}{\approx }f(b)$ for an arbitrary $n\text{.}$

By induction, with a trivial base case, we can assume $f(a)\stackrel{n}{\approx }f(b)$ to show $f(a)\stackrel{1+n}{\approx }f(b)\text{:}$ but $f$ is contractive, so it acts on the induction hypothesis to produce $f(f(a))\stackrel{1+n}{\approx }f(f(b))\text{.}$ But we assumed both $a$ and $b$ are fixed points, so this is exactly what we want.

  banach : ∥ A ∥ → (f : P →ᶜᵒⁿ P) → Σ A λ x → f .map x ≡ x
  banach inhab f = ∥-∥-out fp-unique fp' where
    fp-unique : is-prop (Σ A λ x → f .map x ≡ x)
    fp-unique (a , p) (b , q) =
      Σ-prop-path (λ x → from-ofe-on P .fst .is-tr _ _)
        (sym p ·· P.limit _ _ climb ·· q) where
      climb : ∀ n → f .map a ≈[ n ] f .map b
      climb zero    = P.bounded _ _
      climb (suc n) = transport (λ i → f .map (p i) ≈[ suc n ] f .map (q i)) (f .contract n (climb n))

The point of showing uniqueness is that the fixed point is independent of how $P$ is inhabited: in other words, for a contractive mapping on a COFE to have a fixed point, we needn’t $x:P$ — $x:\Vert P\Vert$ will suffice. That aside justifes this sentence: Fix a starting point $x_0:P\text{,}$ and consider the sequence

which is a chain again by an inductive argument involving contractivity (formalised below for the curious).

    approx : A → Nat → A
    approx a zero    = a
    approx a (suc n) = f .map (approx a n)

    chain : ∀ a → is-chain P (approx a)
    chain a m zero x                = P.bounded (approx a m) a
    chain a (suc m) (suc n) (s≤s x) = f .contract n (chain a m n x)

I claim that the limit of $s$ is a fixed point of $f\text{:}$ we can calculate

where we have, in turn, that non-expansive mappings preserve limits, the very definition of $s\text{,}$ and the fact that limits are insensitive to dropping an element at the start.

    fp' : ∥ _ ∥
    fp' = do
      pt ← inhab
      let
        (it , is) = lim (approx pt) (chain pt)

        ne : is-non-expansive (f .map) P P
        ne = record { pres-≈ = λ p → P.step _ _ _ (f .contract _ p) }

        prf : f .map it ≡ it
        prf =
          f .map it                               ≡⟨ limit-is-unique P _ (non-expansive→limit _ _ _ _ _ ne is) (lim _ _ .snd) ⟩≡
          lim (λ n → f .map (approx pt n)) _ .fst ≡⟨ ap fst (ap (lim _) (λ i → non-expansive→chain _ _ _ _ ne (chain pt))) ⟩≡
          lim (λ n → approx pt (suc n)) _ .fst    ≡⟨ limit-is-unique P _ (lim _ _ .snd) (limit-to-tail P (approx pt) _ (chain pt) is) ⟩≡
          it                                      ∎

      pure (it , prf)