---
description: |
  Dialectica categories, done representably.
  June 4th, 2024 at the HIM trimester.

---
<!--
```agda
open import Cat.Prelude
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Diagram.Product.Solver
open import Cat.Diagram.Exponential
import Cat.Reasoning
```
-->
```agda
module wip.DialecticaRep where
```

```agda
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$.

```agda
  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)$.

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

<!--
```agda
  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
    H-Level-Dia-hom : ∀ {n : Nat} {α β : Rel} → H-Level (Dia-hom α β) (2 + n)
    H-Level-Dia-hom = basic-instance 2 Dia-hom-is-set

  instance
    Extensional-Dia-hom
      : ∀ {α β : Rel} {ℓr}
      → ⦃ e : Extensional ((∀ {Γ} → Hom Γ (α .src) → Hom Γ (β .src)) × (∀ {Γ} → Hom Γ (α .src) → Hom Γ (β .tgt) → Hom Γ (α .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 u = fst (p i) u
        ext-inj {f = f} {g = g} p i .bwd u y = snd (p i) u y
        ext-inj {f = f} {g = g} p i .preserve {u = u} {y = y} =
          is-prop→pathp (λ i → Π-is-hlevel {A = ∣ α .rel u (snd (p i) u y) ∣} 1 λ w → β .rel (fst (p i) u) y .is-tr)
            (f .preserve) (g .preserve) i
        ext-inj {f = f} {g = g} p i .fwd-stable {Δ = Δ} {u = u} σ =
          is-prop→pathp (λ i → Hom-set Δ (β .src) (fst (p i) u ∘ σ) (fst (p i) (u ∘ σ)))
            (f .fwd-stable σ) (g .fwd-stable σ) i
        ext-inj {f = f} {g = g} p i .bwd-stable {Δ = Δ} {u = u} {y = y} σ =
          is-prop→pathp (λ i → Hom-set Δ (α .tgt) (snd (p i) u y ∘ σ) (snd (p i) (u ∘ σ) (y ∘ σ)))
            (f .bwd-stable σ) (g .bwd-stable σ) i
```
-->

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

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

  proj2 : {Γ a b : Ob} → Hom Γ (a ⊗₀ b) → Hom Γ b
  proj2 = π₂ ∘_
```

```agda
  _⇒_ : 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

```agda
  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β)
```