TOTBWF/Dialectica.lagda.md

## Dialectica.lagda.md

      
    Raw
  

              Dialectica.lagda.md
            
          
  description
  
  
  Dialectica categories, done representably.
June 4th, 2024 at the HIM trimester.

  
module wip.DialecticaRep where
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

Dialectica Categories, done representably

We begin by defining a representable relation on a category $\mathcal{C}$ as a
pair of objects $U, X : \mathcal{C}$ along with a sieve on $X \times U$.
  record Rel : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      src : Ob
      tgt : Ob
      rel : ∀ {Γ} → Hom Γ src → Hom Γ tgt → Ω
      rel-stable : ∀ {Δ Γ} {u : Hom Γ src} {x : Hom Γ tgt} → (σ : Hom Δ Γ) → ∣ rel u x ∣ → ∣ rel (u ∘ σ) (x ∘ σ) ∣

  open Rel
A dialectica morphism between two representable relations $\alpha \subseteq U \times X$ and $\beta \subseteq V \times Y$
consists of:

a morphism $f : U \to V$

a morphism $F : U \times Y \to X$

such that for all generalized objects $u, y$, $\alpha(u, F(u,y))$ entails $\beta(f(u), y)$.

  record Dia-hom (α β : Rel) : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      fwd : ∀ {Γ} → Hom Γ (α .src) → Hom Γ (β .src)
      bwd : ∀ {Γ} → Hom Γ (α .src) → Hom Γ (β .tgt) → Hom Γ (α .tgt)
      preserve : ∀ {Γ} {u : Hom Γ (α .src)} {y : Hom Γ (β .tgt)} → ∣ α .rel u (bwd u y) ∣ → ∣ β .rel (fwd u) y ∣
      fwd-stable : ∀ {Γ Δ} {u : Hom Γ (α .src)} → (σ : Hom Δ Γ) → (fwd u) ∘ σ ≡ fwd (u ∘ σ)
      bwd-stable : ∀ {Γ Δ} {u : Hom Γ (α .src)} {y : Hom Γ (β .tgt)} → (σ : Hom Δ Γ) → (bwd u y) ∘ σ ≡ bwd (u ∘ σ) (y ∘ σ)

  open Dia-hom

  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 u = u
  Dialectica .Precategory.id .bwd u y = y
  Dialectica .Precategory.id .preserve wα = wα
  Dialectica .Precategory.id .fwd-stable _ = refl
  Dialectica .Precategory.id .bwd-stable _ = refl
  Dialectica .Precategory._∘_ f g .fwd u = f .fwd (g .fwd u)
  Dialectica .Precategory._∘_ f g .bwd u z = g .bwd u (f .bwd (g .fwd u) z)
  Dialectica .Precategory._∘_ f g .preserve wα = f .preserve (g .preserve wα)
  Dialectica .Precategory._∘_ f g .fwd-stable σ = f .fwd-stable σ ∙ ap (f .fwd) (g .fwd-stable σ)
  Dialectica .Precategory._∘_ f g .bwd-stable {u = u} {y = y} σ =
    g .bwd-stable σ
    ∙ ap (g .bwd (u ∘ σ)) (f .bwd-stable σ ∙ ap (λ e → f .bwd e (y ∘ σ)) (g .fwd-stable σ))
  Dialectica .Precategory.idr f = trivial!
  Dialectica .Precategory.idl f = trivial!
  Dialectica .Precategory.assoc f g h = trivial!
Representability Kit

  proj1 : {Γ a b : Ob} → Hom Γ (a ⊗₀ b) → Hom Γ a
  proj1 = π₁ ∘_

  proj2 : {Γ a b : Ob} → Hom Γ (a ⊗₀ b) → Hom Γ b
  proj2 = π₂ ∘_
  _⇒_ : Ob → Ob → Ob
  a ⇒ b = Exp.B^A a b

  lam : {Γ a b : Ob} → (∀ {Δ} → Hom Δ Γ → Hom Δ a → Hom Δ b) → Hom Γ (a ⇒ b)
  lam k = ƛ (k π₁ π₂)

  _$$_ : {Γ a b : Ob} → Hom Γ (a ⇒ b) → Hom Γ a → Hom Γ b
  f $$ a = ev ∘ ⟨ f , a ⟩

  infixl -1 _$$_
Tensors

  Tensor : Rel → Rel → Rel
  Tensor α β .src = α .src ⊗₀ β .src
  Tensor α β .tgt = α .tgt ⊗₀ β .tgt
  Tensor α β .rel u y = α .rel (proj1 u) (proj1 y) ∧Ω β .rel (proj2 u) (proj2 y)
  Tensor α β .rel-stable σ (wα , wβ) =
    subst₂ (λ u y → ∣ α .rel u y ∣) (sym (assoc _ _ _)) (sym (assoc _ _ _)) (α .rel-stable σ wα) ,
    subst₂ (λ u y → ∣ β .rel u y ∣) (sym (assoc _ _ _)) (sym (assoc _ _ _)) (β .rel-stable σ wβ)