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*^{1} structures, there is a
natural notion of sequences getting closer to a value: we say a sequence
$f:NβA$
is a *chain* if, given
$nβ€m,$
we have
$f(m)βnf(n).$
Looking at the case where
$m=1+n,$
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ββ}2_{βn}=0.$

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
$β$β:
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,$ and $f(n+k)$ certainly shares the first $n$ elements with $f(n).$ However, there is no single list of $As$ $l$ which shares its first $n$ elements with $f(n):$ $l$ must have a definite length, independent of $n,$ which bounds the size of its prefixes. Choosing any $n>length(l)$ results in a value of $f(n)$ has more elements than the length-$n$ prefix of $l.$

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,$ $aβnf(a).$

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,$
we have, for arbitrary
$n,$
$aβnf(a)βnb,$
meaning
$a=b.$

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 Ξ± Ξ²) where open OFE-H-Level P 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^{2} for short.

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

We can actually compute the limit of a sequence of sequences pretty easily: we have a function $s:NΓNβA,$ our sequence, and the chain condition says that, given $jβ€i$ and $k<j,$ we get $s(i,k)=s(j,k).$ Our limit is the sequence $l(i)=s(1+i,i):$ we must show that $lβns(n),$ which means that, given $k<n,$ we must have $s(1+k,k)=s(n,k).$ This follows by the chain condition: $k<1+k,$ and $(1+k)β€n,$ so we conclude $s(1+k,k)=s(n,k).$

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β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.$
It will suffice to show that
$f(a)=f(b),$
and, working in an OFE, this further reduces to
$f(a)βnf(b)$
for an arbitrary
$n.$

By induction, with a trivial base case, we can assume $f(a)βnf(b)$ to show $f(a)β1+nf(b):$ but $f$ is contractive, so it acts on the induction hypothesis to produce $f(f(a))β1+nf(f(b)).$ 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 = β₯-β₯-proj 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:β₯Pβ₯$
will suffice. That aside justifes this sentence: Fix a starting point
$x_{0}:P,$
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:$ we can calculate

$f(nlimβs(n))=nlimβf(s(n))=nlimβs(n+1)=nlimβs(n)$where we have, in turn, that non-expansive mappings preserve limits, the very definition of $s,$ 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)