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-like1 structures, there is a natural notion of sequences getting closer to a value: we say a sequence is a chain if, given we have Looking at the case where this says that we have a sequence

where the metric interpretation of OFEs lets us read this as the distance between successive points approaching

  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 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 for some and certainly shares the first elements with However, there is no single list of which shares its first elements with must have a definite length, independent of which bounds the size of its prefixes. Choosing any results in a value of has more elements than the length- prefix of

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: is the limit of if, for all

  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 and both claim to be limits of we have, for arbitrary meaning

  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 COFE2 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 our sequence, and the chain condition says that, given and we get Our limit is the sequence we must show that which means that, given we must have This follows by the chain condition: and so we conclude

  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 on an inhabited COFE has a unique fixed point. Weβll start with uniqueness: suppose that some satisfy and It will suffice to show that and, working in an OFE, this further reduces to for an arbitrary

By induction, with a trivial base case, we can assume to show but is contractive, so it acts on the induction hypothesis to produce But we assumed both and 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 is inhabited: in other words, for a contractive mapping on a COFE to have a fixed point, we neednβt β will suffice. That aside justifes this sentence: Fix a starting point 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 is a fixed point of we can calculate

where we have, in turn, that non-expansive mappings preserve limits, the very definition of 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)


1. An OFE is a 1-bounded, bisected ultrametric space.β©οΈ

2. Feel free to pronounce it βcoffeeβ.β©οΈ