module Cat.Instances.OFE where

Ordered families of equivalence relations🔗

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

  • The maximal distance between two points is i.e., is the total relation;

  • Points that are within some distance of eachother are also within for any

  • 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

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 should be interpreted as equivalent for steps of computation: a program running for at most steps can not tell elements apart. Our axioms are then that a program running for no steps can not distinguish anything, so we have for any 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 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

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

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 is non-expansive if points under 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 that starts

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

private unquoteDecl eqv' = declare-record-iso eqv' (quote is-non-expansive)

instance
  H-Level-is-non-expansive
    : ∀ {ℓ ℓ₁ ℓ' ℓ₁'} {X : Type ℓ} {Y : Type ℓ₁} {f : X → Y}
        {O : OFE-on ℓ' X} {P : OFE-on ℓ₁' Y} {n}
    → H-Level (is-non-expansive f O P) (suc n)
  H-Level-is-non-expansive {P = P} = prop-instance (Iso→is-hlevel 1 eqv' (hlevel 1)) where
    module P = OFE-on P
    instance
      hlr : ∀ {n k x y} → H-Level (P.within x n y) (suc k)
      hlr = prop-instance (P .OFE-on.has-is-prop _ _ _)

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 is a set, then, for we can define the relations to mean the length- prefixes of and are equal. Let’s quickly go over the axioms informally before looking at the formalisation:

  • Each relation is an equivalence relation, since it is defined to be equality;

  • At the limit, suppose we have lists 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 and for the lengths, we can use our assumption that and agree at length the length prefixes of both and are both the entire lists and so we have

    where the middle step is

  • Finally, since a length prefix is necessarily adding an element onto a length prefix, we satisfy the monotonicity requirement. In the formalisation, we use a direct inductive argument for this. We’ll show that, for all if then

    On the one interesting case, we assume that which we can split into and The induction hypothesis lets us turn this latter equality into which pairs up with 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.

This example generalises incredibly straightforwardly to possibly infinite sequences in a set: that is, functions Our definition of is now that, for all 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🔗

  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)