Bodil Biering

An Analysis of Cartesian 
Closure in Dialectica Categories

Abstract:

When the Dialectica categories were presented by V. de Paiva they were 
found to have a symmetric, monoidal closed structure and Cartesian 
products, but the Dialectica categories did  not seem to have exponents. 
It was therefore very surprising when Birkedal et.al. presented a 
Dialectica-like category (the Dialectica tripos) that did have a 
Cartesian closed structure. We analyse this interesting fact, and at 
first sight it looks like Dialectica categories have a weak exponential, 
if we just require the objects to have a point. It turns out that this 
picture is not exactly right. We need to consider a variation of a 
Dialectica category, which comes about as the Kleisli category for a 
certain comonad on a Dialectica category. It is this Dialectica-Kleisli 
category that has a weak exponential, and we show that the Dialectica 
tripos is a (indexed) preordered reflection of such a Dialectica-Kleisli 
category.