open import 1Lab.Reflection hiding (absurd)

open import Cat.Displayed.Univalence.Thin
open import Cat.Prelude

open import Data.Nat.Properties
open import Data.Nat.Order
open import Data.Nat.Base
open import Data.List

module Cat.Instances.OFE where

Ordered families of equivalence relations🔗

An ordered family of equivalence relations (OFE, for short) is a set $X$ equipped with a family of equivalence relations, indexed by natural numbers $n$ and written $x \approx n y,$ that approximate the equality on $X .$ The family of equivalence relations can be thought of as equipping $X$ with a notion of fractional distance: $x \approx n y$ means that $x$ and $y$ are “within distance $2^{- n}$ of each other”. The axioms of an OFE are essentially that

The maximal distance between two points is $1,$ i.e., $x \approx n y$ is the total relation;
Points that are within some distance $d$ of eachother are also within $d^{'},$ for any $d^{'} \leq d;$
Arbitrarily close points are the same.

Warning

We remark that the term OFE generally stands for ordered family of equivalences, rather than equivalence relations; However, this terminology is mathematically incorrect: there is no meaningful sense in which an OFE is a family $I \to (A \equiv B) .$

To preserve the connection with the literature, we shall maintain the acronym “OFE”; Keep in mind that we do it with disapproval.

Another perspective on OFEs, and indeed a large part for the justification of their study, is in the semantics of programming languages: in that case, the relation $x \approx n y$ should be interpreted as equivalent for $n$ steps of computation: a program running for at most $n$ steps can not tell $\approx n -related$ elements apart. Our axioms are then that a program running for no steps can not distinguish anything, so we have $x \approx 0 y$ for any $x, y,$ and that our approximations become finer with an increasing number of steps: with arbitrarily many steps, the only indistinguishable elements must actually be equal.

record is-ofe {ℓ ℓ'} {X : Type ℓ} (within : Nat → X → X → Type ℓ') : Type (ℓ ⊔ ℓ') where
  no-eta-equality

  field
    has-is-prop : ∀ n x y → is-prop (within n x y)

    ≈-refl  : ∀ n {x} → within n x x
    ≈-sym   : ∀ n {x y} → within n x y → within n y x
    ≈-trans : ∀ n {x y z} → within n y z → within n x y → within n x z

    bounded : ∀ x y → within 0 x y
    step    : ∀ n x y → within (suc n) x y → within n x y
    limit   : ∀ x y → (∀ n → within n x y) → x ≡ y

  ofe→ids : is-identity-system (λ x y → ∀ n → within n x y) (λ x n → ≈-refl n)
  ofe→ids = set-identity-system
    (λ x y → Π-is-hlevel 1 λ n → has-is-prop n x y)
    (limit _ _)

From a HoTT perspective, this definition works extremely smoothly: note that since we require the approximate equalities $x \approx n y$ to be propositions, every subsequent field of the record is also a proposition, so equality of is-ofe is trivial, like we would expect. Moreover, since “equality at the limit”, the relation

R (x, y) = \forall n, x \approx n y

is a reflexive relation (since each $x \approx n y$ is reflexive) that implies equality, the type underlying a OFE is automatically a set; its identity type is equivalent to equality at the limit.

private unquoteDecl eqv = declare-record-iso eqv (quote is-ofe)

opaque instance
  H-Level-is-ofe
    : ∀ {ℓ ℓ'} {X : Type ℓ} {rs : Nat → X → X → Type ℓ'} {n}
    → H-Level (is-ofe rs) (suc n)
  H-Level-is-ofe {X = X} {rs = rs} = prop-instance λ x →
    let
      instance
        hlr : ∀ {n k x y} → H-Level (rs x n y) (suc k)
        hlr = prop-instance (x .is-ofe.has-is-prop _ _ _)

        hs : H-Level X 2
        hs = basic-instance 2 $
          identity-system→hlevel 1 (is-ofe.ofe→ids x) (λ x y → hlevel 1)
    in Iso→is-hlevel 1 eqv (hlevel 1) x

record OFE-on {ℓ} ℓ' (X : Type ℓ) : Type (ℓ ⊔ lsuc ℓ') where
  field
    within     : (n : Nat) (x y : X) → Type ℓ'
    has-is-ofe : is-ofe within
  open is-ofe has-is-ofe public

private
  hlevel-within : ∀ {ℓ ℓ'} {X : Type ℓ} (O : OFE-on ℓ' X) {x y n} → is-prop (O .OFE-on.within n x y)
  hlevel-within O = O .OFE-on.has-is-prop _ _ _

instance
  open hlevel-projection

  hlevel-proj-ofe : hlevel-projection (quote OFE-on.within)
  hlevel-proj-ofe .has-level       = quote hlevel-within
  hlevel-proj-ofe .get-level _     = pure (quoteTerm (suc zero))
  hlevel-proj-ofe .get-argument (_ ∷ _ ∷ _ ∷ o v∷ _) = pure o
  hlevel-proj-ofe .get-argument _ = typeError []

module
  _ {ℓ ℓ₁ ℓ' ℓ₁'} {X : Type ℓ} {Y : Type ℓ₁} (f : X → Y)
    (O : OFE-on ℓ' X) (P : OFE-on ℓ₁' Y)
  where

  private
    module O = OFE-on O
    module P = OFE-on P

The correct notion of morphism between OFEs is that of non-expansive maps, once again appealing to the notion of distance for intuition. A function $f : X \to Y$ is non-expansive if points under $f$ do not get farther. Apart from the intuitive justification, we note that the structure identity principle essentially forces non-expansivity to be the definition of morphism of OFEs: the type of OFEs is equivalent to a $Σ -type$ that starts

Σ (X : Type) Σ (R : X \to N \to X \to Type) Σ...,

where all the components in $...$ are propositional. Its identity type can be computed to consist of equivalences between the underlying types that preserve the relations $R,$ and since the relations are propositions, bi-implication suffices: an identification between OFEs is a non-expansive equivalence of types with non-expansive inverse.

  record is-non-expansive : Type (ℓ ⊔ ℓ' ⊔ ℓ₁') where
    no-eta-equality
    field
      pres-≈ : ∀ {x y n} → O.within n x y → P.within n (f x) (f y)

module _ {ℓa ℓb ℓa' ℓb'} {A : Type ℓa} {B : Type ℓb} (O : OFE-on ℓa' A) (P : OFE-on ℓb' B)
  where

  private
    module O = OFE-on O
    module P = OFE-on P

  record _→ⁿᵉ_ : Type (ℓa ⊔ ℓb ⊔ ℓa' ⊔ ℓb') where
    field
      map    : A → B
      pres-≈ : ∀ n {x y} → O.within n x y → P.within n (map x) (map y)

open _→ⁿᵉ_ public

module _ {ℓa ℓb ℓa' ℓb'} {A : Type ℓa} {B : Type ℓb} {O : OFE-on ℓa' A} {P : OFE-on ℓb' B} where
  private module P = OFE-on P

  Nonexp-ext : ∀ {f g : O →ⁿᵉ P} → (∀ x → f .map x ≡ g .map x) → f ≡ g
  Nonexp-ext α i .map z = α z i
  Nonexp-ext {f = f} {g} α i .pres-≈ n {x} {y} β =
    is-prop→pathp (λ i → P.has-is-prop n (α x i) (α y i)) (f .pres-≈ n β) (g .pres-≈ n β) i

unquoteDecl
  H-Level-is-non-expansive = declare-record-hlevel 1 H-Level-is-non-expansive (quote is-non-expansive)

open is-non-expansive

OFE-structure : ∀ {ℓ ℓ'} → Thin-structure (ℓ ⊔ ℓ') (OFE-on {ℓ} ℓ')
∣ OFE-structure .is-hom f O P ∣ = is-non-expansive f O P
OFE-structure .is-hom f O P .is-tr = hlevel 1
OFE-structure .id-is-hom .pres-≈ w = w
OFE-structure .∘-is-hom f g α β .pres-≈ w = α .pres-≈ (β .pres-≈ w)
OFE-structure .id-hom-unique {s = s} {t = t} α β = q where
  module s = OFE-on s
  module t = OFE-on t

  p : ∀ x y n → (s.within x n y) ≃ (t.within x n y)
  p x y n = prop-ext (s.has-is-prop _ _ _) (t.has-is-prop _ _ _)
    (α .pres-≈) (β .pres-≈)

  q : s ≡ t
  q i .OFE-on.within x n y = ua (p x y n) i
  q i .OFE-on.has-is-ofe = is-prop→pathp
    (λ i → hlevel {T = is-ofe (λ x n y → ua (p x y n) i)} 1)
    s.has-is-ofe t.has-is-ofe i

OFEs : ∀ ℓ ℓ' → Precategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
OFEs ℓ ℓ' = Structured-objects (OFE-structure {ℓ} {ℓ'})
module OFEs {ℓ ℓ'} = Precategory (OFEs ℓ ℓ')

OFE : ∀ ℓ ℓ' → Type (lsuc (ℓ ⊔ ℓ'))
OFE ℓ ℓ' = OFEs.Ob {ℓ} {ℓ'}

open OFE-on hiding (ofe→ids) public
open is-ofe public
open is-non-expansive public

Examples🔗

A canonical class of examples for OFEs is given by strings, or, more generally, lists: if $X$ is a set, then, for $x, y : List (X),$ we can define the relations $x \approx n y$ to mean the length- $n$ prefixes of $x$ and $y$ are equal. Let’s quickly go over the axioms informally before looking at the formalisation:

Each relation $\approx n$ is an equivalence relation, since it is defined to be equality;
At the limit, suppose we have lists $x, y :$ we do not yet know that their lengths agree, but we do know that taking a “prefix” longer than the list gives back the entire list.

So, writing $l_{x}$ and $l_{y}$ for the lengths, we can use our assumption that $x$ and $y$ agree at length $l = max (l_{x}, l_{y}) :$ the length $l$ prefixes of both $x$ and $y$ are both the entire lists $x$ and $y,$ so we have
$x = take (l, x) = take (l, y) = y,$
where the middle step is $x \approx l y .$
Finally, since a length $l + 1$ prefix is necessarily adding an element onto a length $l$ prefix, we satisfy the monotonicity requirement. In the formalisation, we use a direct inductive argument for this. We’ll show that, for all $x s, ys, n,$ if $take (1 + n, x s) = take (1 + n, ys),$ then $take (n, x s) = take (n, ys) .$

On the one interesting case, we assume that $x :: take (1 + n, x s) = y :: take (1 + n, ys),$ which we can split into $x = y$ and $take (1 + n, x s) = take (1 + n, ys) .$ The induction hypothesis lets us turn this latter equality into $take (n, x s) = take (n, ys),$ which pairs up with $x = y$ to conclude exactly what we want.

Lists : ∀ {ℓ} {X : Type ℓ} → is-set X → OFE-on ℓ (List X)
Lists X-set .within n xs ys = take n xs ≡ take n ys
Lists X-set .has-is-ofe .has-is-prop n xs ys = ListPath.is-set→List-is-set X-set _ _
Lists X-set .has-is-ofe .≈-refl  n     = refl
Lists X-set .has-is-ofe .≈-sym   n p   = sym p
Lists X-set .has-is-ofe .≈-trans n p q = q ∙ p
Lists X-set .has-is-ofe .bounded x y   = refl

Lists X-set .has-is-ofe .limit x y wit = sym rem₁ ·· agree ·· rem₂ where
  enough = max (length x) (length y)
  agree : take enough x ≡ take enough y
  agree = wit enough

  rem₁ : take enough x ≡ x
  rem₁ = take-length-more x enough (max-≤l _ _)
  rem₂ : take enough y ≡ y
  rem₂ = take-length-more y enough (max-≤r _ _)

Lists X-set .has-is-ofe .step n x y p = steps x y n p where
  steps : ∀ {ℓ} {A : Type ℓ} (x y : List A) n
        → take (suc n) x ≡ take (suc n) y → take n x ≡ take n y
  steps (x ∷ xs) (y ∷ ys) (suc n) p =
    ap₂ _∷_ (ap (head x) p) (steps xs ys n (ap tail p))

Since the rest of this proof is a simple case bash[^5 cases are reflexivity, 2 assume an impossibility], we’ve hidden it on the website. You can choose to display comments on the side bar, or check out this module on GitHub.

  steps []       []       zero    p = refl
  steps []       []       (suc n) p = refl
  steps []       (x ∷ ys) zero    p = refl
  steps (x ∷ xs) (y ∷ ys) zero    p = refl
  steps (x ∷ xs) []       zero    p = refl
  steps []       (x ∷ ys) (suc n) p = absurd (∷≠[] (sym p))
  steps (x ∷ xs) []       (suc n) p = absurd (∷≠[] p)

This example generalises incredibly straightforwardly to possibly infinite sequences in a set: that is, functions $N \to X .$ Our definition of $x \approx n y$ is now that, for all $k < n,$ $x (k) = y (k) .$ Once again we are using equality to approximate equality, so this is levelwise an equivalence relation; surprisingly, the other three properties are simpler to establish for sequences than for lists!

Sequences : ∀ {ℓ} {X : Type ℓ} → is-set X → OFE-on ℓ (Nat → X)
Sequences _ .within n xs ys = ∀ k (le : k < n) → xs k ≡ ys k
Sequences {X = X} X-set .has-is-ofe .has-is-prop n xs ys = hlevel 1 where instance
  _ : H-Level X 2
  _ = basic-instance 2 X-set
Sequences _ .has-is-ofe .≈-refl  n k le     = refl
Sequences _ .has-is-ofe .≈-sym   n p k le   = sym (p k le)
Sequences _ .has-is-ofe .≈-trans n p q k le = q k le ∙ p k le

Sequences _ .has-is-ofe .bounded xs ys k ()
Sequences _ .has-is-ofe .step n xs ys p k le = p k (≤-sucr le)
Sequences _ .has-is-ofe .limit xs ys wit     = funext λ k → wit (suc k) k ≤-refl

Contractive maps🔗

module
  _ {ℓ ℓ₁ ℓ' ℓ₁'} {X : Type ℓ} {Y : Type ℓ₁} (f : X → Y)
    (O : OFE-on ℓ' X) (P : OFE-on ℓ₁' Y)
  where

  private
    module O = OFE-on O
    module P = OFE-on P

  record is-contractive : Type (ℓ ⊔ ℓ' ⊔ ℓ₁') where
    no-eta-equality
    field
      contract : ∀ {x y n} → O.within n x y → P.within (suc n) (f x) (f y)

unquoteDecl
  H-Level-is-contractive = declare-record-hlevel 1 H-Level-is-contractive (quote is-contractive)

module _ {ℓa ℓb ℓa' ℓb'} {A : Type ℓa} {B : Type ℓb} (O : OFE-on ℓa' A) (P : OFE-on ℓb' B)
  where

  private
    module O = OFE-on O
    module P = OFE-on P

  record _→ᶜᵒⁿ_ : Type (ℓa ⊔ ℓb ⊔ ℓa' ⊔ ℓb') where
    field
      map      : A → B
      contract : ∀ n {x y} → O.within n x y → P.within (suc n) (map x) (map y)

open _→ᶜᵒⁿ_ public
open is-contractive public

module OFE-Notation {ℓ ℓ'} {X : Type ℓ} ⦃ O : OFE-on ℓ' X ⦄ where
  private module O = OFE-on O
  _≈[_]_ : X → Nat → X → Type ℓ'
  x ≈[ n ] y = O.within n x y

from-ofe-on : ∀ {ℓ ℓ'} {X : Type ℓ} → OFE-on ℓ' X → OFEs.Ob
∣ from-ofe-on {X = X} O .fst ∣ = X
from-ofe-on O .fst .is-tr = identity-system→hlevel 1 (OFE-on.ofe→ids O) λ x y → Π-is-hlevel 1 λ n → OFE-on.has-is-prop O n x y
from-ofe-on O .snd = O