Dialectica Categories with Valeria

Dialectica.lagda.md

description
Dialectica categories with Valeria June 4th, 2024 at the HIM trimester. Created by Reed Mullanix, comments by vcvp (trying to understand).

module wip.Dialectica where

Let $\cC$ be a cartesian closed category with all pullbacks.

module _ {o ℓ}
  (C : Precategory o ℓ)
  (cart : has-products C)
  (term : Terminal C)
  (cc : Cartesian-closed C cart term)
  where

  open Cat.Reasoning C
  open Binary-products C cart
  open Terminal term
  open Cartesian-closed  cc

We begin by defining the type of relations internal to a cartesian category $\cC$.

vcvp: To build the (original) Dialectica construction over $\cC$ we first consider its objects.

vcvp: An object of Dial(C) is a triple $(U,X, \alpha)$, where $U$ and $X$ are objects in $\cC$, and $\alpha$ is a relation between $U$ and $X$ in $\cC$. Hence $\alpha$ is a monic into the product of objects $U\times X$. (Alternatively we could talk about a function $\alpha:U\times X\to 2$, where 2 is the Boolean type. different pros and cons. Elena wanted to prove the equivalence between the alternatives.)

vcvp: Now to represent these objects in code, we want to have the relation $\alpha$ itself represented. How?

Here the objects are called the src (source) and the tgt (target), hence $\alpha$ is a monic into src ⊗₀ tgt. The relation $\alpha$ is an object. why?

  record Rel : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      src : Ob
      tgt : Ob
      rel : Ob
      inj : Hom rel (src ⊗₀ tgt)
      inj-mono : is-monic inj

  open Rel

A witness of a relation $\alpha$ between two generalized elements $u, x$ is a generalized element of the subobject $\alpha$ that factorizes $\langle u, x \rangle$.

  record Witness {Γ : Ob} (α : Rel) (u : Hom Γ (α .src)) (x : Hom Γ (α .tgt)) : Type ℓ where
    no-eta-equality
    field
      im : Hom Γ (α .rel)
      related : ⟨ u , x ⟩ ≡ (α .inj ∘ im)

  open Witness

The type of witnesses is a prop; this follows immediately from the fact that $\alpha$ is a mono.

  abstract
    Witness-is-prop : ∀ {Γ} {α : Rel} {u : Hom Γ (α .src)} {x : Hom Γ (α .tgt)} → is-prop (Witness α u x)
    Witness-is-prop {α = α} w w' = path where
      im-path : w .im ≡ w' .im
      im-path = inj-mono α (w .im) (w' .im) (sym (w .related) ∙ w' .related)

      path : w ≡ w'
      path i .im = im-path i
      path i .related = is-prop→pathp (λ i → Hom-set _ _ _ (α .inj ∘ im-path i)) (w .related) (w' .related) i

  instance
    H-Level-Witness : ∀ {Γ} {α : Rel} {u : Hom Γ (α .src)} {x : Hom Γ (α .tgt)} {n : Nat} → H-Level (Witness α u x) (suc n)
    H-Level-Witness = prop-instance Witness-is-prop

We can transport a witness of $\alpha(u, x)$ to $\alpha(u', x')$ without actually invoking transport.

  wcast : ∀ {Γ} {α : Rel} {u u' : Hom Γ (α .src)} {x x' : Hom Γ (α .tgt)} → Witness α u x → u ≡ u' → x ≡ x' → Witness α u' x'
  wcast w p q .im = w .im
  wcast w p q .related =  ap₂ ⟨_,_⟩ (sym p) (sym q) ∙ w .related

Morphisms

  record Dia-hom (α β : Rel) : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      fwd : Hom (α .src) (β .src)
      bwd : Hom (α .src ⊗₀ β .tgt) (α .tgt)
      preserve : ∀ {Γ} (u : Hom Γ (α .src)) (y : Hom Γ (β .tgt)) →  Witness α u (bwd ∘ ⟨ u , y ⟩ → Witness β (fwd ∘ u) y )

  open Dia-hom

  abstract
    Dia-hom-is-set : ∀ {α β : Rel} → is-set (Dia-hom α β)
    Dia-hom-is-set = Iso→is-hlevel 2 eqv (hlevel 2)
      where unquoteDecl eqv = declare-record-iso eqv (quote Dia-hom)

  instance
    Extensional-Dia-hom
      : ∀ {α β : Rel} {ℓr}
      → ⦃ e : Extensional (Hom (α .src) (β .src) × Hom (α .src ⊗₀ β .tgt) (α .tgt)) ℓr ⦄
      → Extensional (Dia-hom α β) ℓr
    Extensional-Dia-hom {α = α} {β = β} ⦃ e ⦄ = injection→extensional! {f = λ f → f .fwd , f .bwd} ext-inj e
      where
        ext-inj : ∀ {f g : Dia-hom α β} → (f .fwd , f .bwd) ≡ (g .fwd , g .bwd) → f ≡ g
        ext-inj {f = f} {g = g} p i .fwd = fst (p i)
        ext-inj {f = f} {g = g} p i .bwd = snd (p i)
        ext-inj {f = f} {g = g} p i .preserve u y =
          is-prop→pathp (λ i → Π-is-hlevel {A = Witness β (fst (p i) ∘ u) y} 1 λ w → Witness-is-prop {u = u} {x = snd (p i) ∘ ⟨ u , y ⟩})
            (f .preserve u y)
            (g .preserve u y) i

Identities and Composition in Dialectica

  Dialectica : Precategory (o ⊔ ℓ) (o ⊔ ℓ)
  Dialectica .Precategory.Ob = Rel
  Dialectica .Precategory.Hom = Dia-hom
  Dialectica .Precategory.Hom-set _ _ = Dia-hom-is-set
  Dialectica .Precategory.id .fwd = id
  Dialectica .Precategory.id .bwd = π₂
  Dialectica .Precategory.id {α} .preserve u x w .im = w .im
  Dialectica .Precategory.id {α} .preserve u x w .related =
    ⟨ u , π₂ ∘ ⟨ u , x ⟩ ⟩ ≡⟨ ap₂ ⟨_,_⟩ (sym (idl _)) π₂∘⟨⟩ ⟩
    ⟨ id ∘ u , x ⟩         ≡⟨ w .related ⟩
    (α .inj ∘ w .im)       ∎
    
 # composition below?
 
  Precategory._∘_ Dialectica {α} {β} {γ} f g .fwd = f .fwd ∘ g .fwd
  Precategory._∘_ Dialectica {α} {β} {γ} f g .bwd = g .bwd ∘ ⟨ π₁ , f .bwd ∘ (g .fwd ⊗₁ id) ⟩
  Precategory._∘_ Dialectica {α} {β} {γ} f g .preserve u z w =
    let wβ = f .preserve (g .fwd ∘ u) z (wcast w (sym (assoc _ _ _)) refl)
    in wcast (g .preserve u (f .bwd ∘ ⟨ g .fwd ∘ u , z ⟩) wβ) refl $
      (g .bwd ∘ ⟨ u , f . bwd ∘ ⟨ g .fwd ∘ u , z ⟩ ⟩)                     ≡⟨ products! C cart ⟩
      (g .bwd ∘ ⟨ π₁ , f .bwd ∘  ⟨ g .fwd ∘ π₁ , id ∘ π₂ ⟩ ⟩) ∘ ⟨ u , z ⟩ ∎
  Dialectica .Precategory.idr f =
    ext (idr _ , (
      π₂ ∘ ⟨ π₁ , f .bwd ∘ (id ⊗₁ id) ⟩ ≡⟨ products! C cart ⟩
      f .bwd ∎))
  Dialectica .Precategory.idl f = ext (idl _ , (
    (f .bwd ∘ ⟨ π₁ , π₂ ∘ (f .fwd ⊗₁ id) ⟩) ≡⟨ products! C cart ⟩
    f .bwd ∎))
  Dialectica .Precategory.assoc f g h = ext (assoc _ _ _ , (
    (h .bwd ∘ ⟨ π₁ , g .bwd ∘ (h .fwd ⊗₁ id) ⟩) ∘ ⟨ π₁ , f .bwd ∘ ((g .fwd ∘ h .fwd) ⊗₁ id) ⟩ ≡⟨ products! C cart ⟩
    h .bwd ∘ ⟨ π₁ , (g .bwd ∘ ⟨ π₁ , f .bwd ∘ (g .fwd ⊗₁ id) ⟩) ∘ (h .fwd ⊗₁ id) ⟩ ∎))