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

module Cat.Instances.OFE.Product where

Products of OFEsπŸ”—

The category of OFEs admits products: the relations are, levelwise, pairwise! That is, if and Distributing the axioms over products is enough to establish that this is actually an OFE.

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

  Γ—-OFE : OFE-on (β„“a' βŠ” β„“b') (A Γ— B)
  Γ—-OFE .within n (x , y) (x' , y') = (x β‰ˆ[ n ] x') Γ— (y β‰ˆ[ n ] y')
  Γ—-OFE .has-is-ofe .has-is-prop n x y = hlevel 1

  Γ—-OFE .has-is-ofe .β‰ˆ-refl  n = O.β‰ˆ-refl n , P.β‰ˆ-refl n
  Γ—-OFE .has-is-ofe .β‰ˆ-sym   n (p , q) = O.β‰ˆ-sym n p , P.β‰ˆ-sym n q
  Γ—-OFE .has-is-ofe .β‰ˆ-trans n (p , q) (p' , q') =
    O.β‰ˆ-trans n p p' , P.β‰ˆ-trans n q q'

  Γ—-OFE .has-is-ofe .bounded (a , b) (a' , b') = O.bounded a a' , P.bounded b b'
  Γ—-OFE .has-is-ofe .step n _ _ (p , p') = O.step n _ _ p , P.step n _ _ p'
  Γ—-OFE .has-is-ofe .limit x y f =
    apβ‚‚ _,_ (O.limit _ _ Ξ» n β†’ f n .fst) (P.limit _ _ Ξ» n β†’ f n .snd)

open Product
open is-product
open Total-hom

By construction, this OFE is actually the proper categorical product of the OFE structures we started with: since this is a very concrete category, most of the reasoning piggy-backs off of that for types, which is almost definitional. Other than the noise inherent to formalisation, the argument is immediate:

OFE-Product : βˆ€ {β„“ β„“'} A B β†’ Product (OFEs β„“ β„“') A B
OFE-Product A B .apex = from-ofe-on (Γ—-OFE (A .snd) (B .snd))
OFE-Product A B .π₁ .hom = fst
OFE-Product A B .π₁ .preserves .pres-β‰ˆ = fst

OFE-Product A B .Ο€β‚‚ .hom = snd
OFE-Product A B .Ο€β‚‚ .preserves .pres-β‰ˆ = snd

OFE-Product A B .has-is-product .⟨_,_⟩ f g .hom x = f # x , g # x
OFE-Product A B .has-is-product .⟨_,_⟩ f g .preserves .pres-β‰ˆ p =
  f .preserves .pres-β‰ˆ p , g .preserves .pres-β‰ˆ p

OFE-Product A B .has-is-product .Ο€β‚βˆ˜βŸ¨βŸ© = trivial!
OFE-Product A B .has-is-product .Ο€β‚‚βˆ˜βŸ¨βŸ© = trivial!
OFE-Product A B .has-is-product .unique p q = ext Ξ» x β†’ p #β‚š x ,β‚š q #β‚š x

module
  _ {β„“i β„“f β„“r} {I : Type β„“i} (F : I β†’ Type β„“f) (P : βˆ€ i β†’ OFE-on β„“r (F i)) where
  private
    instance
      P-ofe : βˆ€ {i} β†’ OFE-on β„“r (F i)
      P-ofe {i} = P i
    module P {i} = OFE-on (P i)

Indexed productsπŸ”—

We now turn to a slightly more complicated case: indexed products of OFEs: because Agda is, by default, a predicative theory, we run into some issues with universe levels when defining the indexed product. Let’s see them:

Suppose we have an index type in the universe, and a family valued now in the universe. Moreover, the family should be pointwise an OFE, with nearness relation living in, let’s say, the universe. We will define the relation on to be

but this type is too large: Since we quantify over and return one of the approximate equalities, it must live in the universe; but if we want indexed products to be in the same category we started with, it should live in the

Fortunately, to us, this is an annoyance, not an impediment: here in the 1Lab, we assume propositional resizing throughout. Since the product type is a proposition, it is equivalent to a small type, so we can put it in any universe, including the

The construction is essentially the same as for binary products: however, since resizing is explicit, we have to do a bit more faffing about to get the actual inhabitant of that we’re interested in.

  Ξ -OFE : OFE-on β„“r (βˆ€ i β†’ F i)
  Ξ -OFE .within n f g = Lift β„“r (β–‘ (βˆ€ i β†’ f i β‰ˆ[ n ] g i))
  Ξ -OFE .has-is-ofe .has-is-prop n x y = Lift-is-hlevel 1 squash
  Ξ -OFE .has-is-ofe .β‰ˆ-refl n = lift (inc Ξ» i β†’ P.β‰ˆ-refl n)
  Ξ -OFE .has-is-ofe .β‰ˆ-sym n (lift x) = lift do
    x ← x
    pure Ξ» i β†’ P.β‰ˆ-sym n (x i)
  Ξ -OFE .has-is-ofe .β‰ˆ-trans n (lift p) (lift q) = lift do
    p ← p
    q ← q
    pure Ξ» i β†’ P.β‰ˆ-trans n (p i) (q i)
  Ξ -OFE .has-is-ofe .bounded x y = lift (inc Ξ» i β†’ P.bounded (x i) (y i))
  Ξ -OFE .has-is-ofe .step n x y (lift p) = lift do
    p ← p
    pure Ξ» i β†’ P.step n (x i) (y i) (p i)
  Ξ -OFE .has-is-ofe .limit x y wit i j = P.limit (x j) (y j) (Ξ» n β†’ wit' n j) i
    where
      wit' : βˆ€ n i β†’ within (P i) n (x i) (y i)
      wit' n i = β–‘-out! (wit n .lower) i

open is-indexed-product
open Indexed-product

And, again, by essentially the same argument, we can establish that this is the categorical indexed product of in the category of OFEs, as long as all the sizes match up.

OFE-Indexed-product
  : βˆ€ {β„“o β„“r} {I : Type β„“o} (F : I β†’ OFE β„“o β„“r)
  β†’ Indexed-product (OFEs β„“o β„“r) F
OFE-Indexed-product F .Ξ F = from-ofe-on $
  Ξ -OFE (Ξ» i β†’ ∣ F i .fst ∣) (Ξ» i β†’ F i .snd)
OFE-Indexed-product F .Ο€ i .hom f = f i
OFE-Indexed-product F .Ο€ i .preserves .pres-β‰ˆ Ξ± =
  β–‘-out! ((_$ i) <$> Ξ± .lower)
OFE-Indexed-product F .has-is-ip .tuple f .hom x i = f i # x
OFE-Indexed-product F .has-is-ip .tuple f .preserves .pres-β‰ˆ wit =
  lift $ inc Ξ» i β†’ f i .preserves .pres-β‰ˆ wit
OFE-Indexed-product F .has-is-ip .commute = trivial!
OFE-Indexed-product F .has-is-ip .unique f prf =
  ext Ξ» x y β†’ prf y #β‚š x