Dialectica Category

There are a couple of versions of dialectica categories: we shall start with the most general first. Let $\mathcal{E}\to\mathcal{D}\to\mathcal{C}$ be a tower of Cartesian Fibrations. The dialectica category $\mathrm{Dia}(\mathcal{E},\mathcal{D})\to\mathcal{C}$ is defined as $(\mathcal{D}\circ\mathcal{E}^{\mathrm{op}})^{\mathrm{op}}$, where $\circ$ denotes the Composition of Displayed Categories, and $(-)^{\mathrm{op}}$ denotes the Fibrewise Opposite of a Cartesian Fibration.

If we unfold this, the objects over $U:\mathcal{C}$ consist of a pair of a $X:\mathcal{D}_{X}$ and an $\alpha:\mathcal{E}_{U,X}$. Morphisms are a bit involved because of all the fibrewise ops: A map over $f:U\to V$ between $(X,\alpha)$ and $(Y,\beta)$ consists of:

• A $U$ vertical map $f^{\sharp}:\mathcal{D}_{U}(f^{*}(Y),X)$
• A $(U,f^{*}(Y))$ vertical map $f^{\flat}:\mathcal{E}_{(U,f^{*}(Y))}((f^{\sharp})^{*}(\alpha),\pi^{*}(\beta))$

This is somewhat bonkers to read in categorical notation; here's what happens when we specialize to iterated Family Fibrations over the Category of Sets:

{-# NO_UNIVERSE_CHECK #-}
record Dia : Type where
  field
    Ix : Type
    Shape : Ix → Type
    Pos : ∀ (i : Ix) → Shape i → Type

open Dia

record Dia-hom (P Q : Dia) : Type where
  field
    ix : P .Ix → Q .Ix
    shape : ∀ (i : P .Ix) → Q .Shape (ix i) → P .Shape i
    pos : ∀ (i : P .Ix) (q : Q .Shape (ix i)) → P .Pos i (shape i q) → Q .Pos (ix i) q

open Dia-hom

References

• Dialectica Models of Type Theory gives a presentation of the basic setup
• Hyland is the first source of this presentation