open import Cat.Displayed.Univalence.Thin
open import Cat.Diagram.Coproduct
open import Cat.Displayed.Total
open import Cat.Instances.OFE
open import Cat.Prelude

open import Data.Sum.Base

module Cat.Instances.OFE.Coproduct where

Coproducts of OFEsπŸ”—

The category of OFEs admits binary coproducts. Unlike the construction of products, in which we could define the approximations by lifting those of the factor OFEs, the definition of coproducts requires a fair bit more busywork.

open OFE-Notation

module _ {β„“a β„“b β„“a' β„“b'} {A : Type β„“a} {B : Type β„“b} (O : OFE-on β„“a' A) (P : OFE-on β„“b' B)
  where
  private
    instance
      _ = O
      _ = P
    module O = OFE-on O
    module P = OFE-on P

To get it right, let’s use the computational interpretation of OFEs. Having done no steps of computation, we have not yet managed to distinguish the left summand from the right summand. Motivated by this, and to satisfy the boundedness axiom, we simply define to be the unit type everywhere.

Having taken some positive number of steps, it is possible to distinguish the summands, and we must do so, defining the relations by cases. The relations where ranges over the coproduct injections, are defined to be Note the index: we do not want to take a step back! In case the summands are mismatched, e.g.Β  we give back the bottom type: we have taken enough steps that it is impossible for them to be equal.

  ⊎-OFE : OFE-on (β„“a' βŠ” β„“b') (A ⊎ B)
  ⊎-OFE .within zero p q = Lift (β„“a' βŠ” β„“b') ⊀
  ⊎-OFE .within (suc n) (inl x) (inl y) = Lift β„“b' (x β‰ˆ[ suc n ] y)
  ⊎-OFE .within (suc n) (inr x) (inr y) = Lift β„“a' (x β‰ˆ[ suc n ] y)
  ⊎-OFE .within (suc n) (inl x) (inr y) = Lift (β„“a' βŠ” β„“b') βŠ₯
  ⊎-OFE .within (suc n) (inr x) (inl y) = Lift (β„“a' βŠ” β„“b') βŠ₯

The proofs of all the axioms will have to make the same case distinctions to get at a concrete type for the approximations. Let’s see it for reflexivity:

  • We first distinguish on the number of steps. If we’ve not taken any yet, then our relation is trivial, and we can (have to!) give back its trivial point.

  • Having taken a number of steps, we distinguish on the summand. Having exposed the underlying relation, we can lift its proof of reflexivity to the sum.

  ⊎-OFE .has-is-ofe .β‰ˆ-refl zero            = lift tt
  ⊎-OFE .has-is-ofe .β‰ˆ-refl (suc n) {inl _} = lift (O.β‰ˆ-refl (suc n))
  ⊎-OFE .has-is-ofe .β‰ˆ-refl (suc n) {inr _} = lift (P.β‰ˆ-refl (suc n))
The other fields are essentially the same, so there’s not a lot to write about. 
  ⊎-OFE .has-is-ofe .has-is-prop zero x y _ _ = refl
  ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inl _) (inl _) = hlevel 1
  ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inr _) (inr _) = hlevel 1

  ⊎-OFE .has-is-ofe .β‰ˆ-sym zero p = lift tt
  ⊎-OFE .has-is-ofe .β‰ˆ-sym (suc n) {inl _} {inl _} p = lift (O.β‰ˆ-sym _ (p .lower))
  ⊎-OFE .has-is-ofe .β‰ˆ-sym (suc n) {inr _} {inr _} p = lift (P.β‰ˆ-sym _ (p .lower))

  ⊎-OFE .has-is-ofe .β‰ˆ-trans zero p q = lift tt
  ⊎-OFE .has-is-ofe .β‰ˆ-trans (suc n) {inl _} {inl _} {inl _} p q = lift (O.β‰ˆ-trans _ (p .lower) (q .lower))
  ⊎-OFE .has-is-ofe .β‰ˆ-trans (suc n) {inr _} {inr _} {inr _} p q = lift (P.β‰ˆ-trans _ (p .lower) (q .lower))

  ⊎-OFE .has-is-ofe .bounded a b  = lift tt
  ⊎-OFE .has-is-ofe .step zero _ _ p = lift tt
  ⊎-OFE .has-is-ofe .step (suc n) (inl x) (inl y) p = lift (O.step _ x y (p .lower))
  ⊎-OFE .has-is-ofe .step (suc n) (inr x) (inr y) p = lift (P.step _ x y (p .lower))

This minor quibble might be of note to the reader curious enough to expand this note: To prove that our approximations converge, we also need a case distinction. At the zeroth entry, we appeal to boundedness of the summand OFEs to get a witness of since is uninformative.

  ⊎-OFE .has-is-ofe .limit (inl x) (inl y) f = ap inl (O.limit x y f') where
    f' : βˆ€ n β†’ O.within n x y
    f' zero    = O.bounded x y
    f' (suc n) = f (suc n) .lower
  ⊎-OFE .has-is-ofe .limit (inr x) (inr y) f = ap inr (P.limit x y f') where
    f' : βˆ€ n β†’ P.within n x y
    f' zero    = P.bounded x y
    f' (suc n) = f (suc n) .lower
  ⊎-OFE .has-is-ofe .limit (inl x) (inr y) f = absurd (f 1 .lower)
  ⊎-OFE .has-is-ofe .limit (inr x) (inl y) f = absurd (f 1 .lower)

open Coproduct
open is-coproduct
open Total-hom

We now prove that this construction, which despite my best efforts may still feel unmotivated, is the categorical product in OFEs. We start by defining the coproduct of morphisms, the operation taking and to Once again, it’s a case bash, and we have to use boundedness of the codomain when showing that points with distance 1 stay with distance 1.

OFE-Coproduct : βˆ€ {β„“ β„“'} A B β†’ Coproduct (OFEs β„“ β„“') A B
OFE-Coproduct A B = mk where
  module A = OFE-on (A .snd)
  module B = OFE-on (B .snd)

  it = from-ofe-on (⊎-OFE (A .snd) (B .snd))

  disj : βˆ€ {Q} β†’ OFEs.Hom A Q β†’ OFEs.Hom B Q β†’ OFEs.Hom it Q
  disj f g .hom (inl x) = f # x
  disj f g .hom (inr x) = g # x
  disj {Q = Q} f g .preserves .pres-β‰ˆ {n = zero} _ = OFE-on.bounded (Q .snd) _ _
  disj f g .preserves .pres-β‰ˆ {inl x} {inl y} {suc n} (lift Ξ±) =
    f .preserves .pres-β‰ˆ Ξ±
  disj f g .preserves .pres-β‰ˆ {inr x} {inr y} {suc n} (lift Ξ±) =
    g .preserves .pres-β‰ˆ Ξ±

We can then define the coprojections: since we must now produce an approximation in the sum, if our points have distance 1, we can produce a trivial datum.

  in0 : OFEs.Hom A it
  in0 .hom = inl
  in0 .preserves .pres-β‰ˆ {n = zero}  _ = lift tt
  in0 .preserves .pres-β‰ˆ {n = suc n} Ξ± = lift Ξ±

  in1 : OFEs.Hom B it
  in1 .hom = inr
  in1 .preserves .pres-β‰ˆ {n = zero}  _ = lift tt
  in1 .preserves .pres-β‰ˆ {n = suc n} Ξ± = lift Ξ±

It suffices to show that all the relevant diagrams in the definition of a coproduct actually commute, and that the coproduct of morphisms is unique: but it suffices to reason at the level of sets.

  mk : Coproduct (OFEs _ _) A B
  mk .coapex = it
  mk .ι₁ = in0
  mk .ΞΉβ‚‚ = in1
  mk .has-is-coproduct .is-coproduct.[_,_] {Q = Q} f g = disj f g
  mk .has-is-coproduct .[]βˆ˜ΞΉβ‚ = trivial!
  mk .has-is-coproduct .[]βˆ˜ΞΉβ‚‚ = trivial!
  mk .has-is-coproduct .unique p q = ext Ξ» where
    (inl x) β†’ p #β‚š x
    (inr x) β†’ q #β‚š x