Dialectica category #
We define the category Dial of the Dialectica interpretation, after [dialectica1989].
Background #
Dialectica categories are important models of linear type theory. They satisfy most of the distinctions that linear logic was meant to introduce and many models do not satisfy, like the independence of constants. Many linear type theories are being used at the moment--nLab describes some of them: for quantum systems, for effects in programming, for linear dependent types. In particular, dialectica categories are connected to polynomial functors, being a slightly more sophisticated version of polynomial types, as discussed, for instance, in Moss and von Glehn's Dialectica models of type theory. As such they are related to the polynomial constructions being developed by Awodey, Riehl, and Hazratpour. For the non-dependent version developed here several applications are known to Petri Nets, small cardinals in Set Theory, state in imperative programming, and others, see Dialectica Categories.
References #
- [Valeria de Paiva, The Dialectica Categories.][dialectica1989] (pdf)
The Dialectica category. An object of the category is a triple ⟨U, X, α ⊆ U × X⟩,
and a morphism from ⟨U, X, α⟩ to ⟨V, Y, β⟩ is a pair (f : U ⟶ V, F : U ⨯ Y ⟶ X) such that
{(u,y) | α(u, F(u, y))} ⊆ {(u,y) | β(f(u), y)}. The subset α is actually encoded as an element
of Subobject (U × X), and the above inequality is expressed using pullbacks.
- src : C
The source object
- tgt : C
The target object
- rel : CategoryTheory.Subobject (self.src ⨯ self.tgt)
Instances For
A morphism in the Dial C category from ⟨U, X, α⟩ to ⟨V, Y, β⟩ is a pair
(f : U ⟶ V, F : U ⨯ Y ⟶ X) such that {(u,y) | α(u, F(u, y))} ≤ {(u,y) | β(f(u), y)}.
- f : X.src ⟶ Y.src
Maps the sources
Maps the targets (contravariantly)
- le : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst self.F)).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map self.f (CategoryTheory.CategoryStruct.id Y.tgt))).obj Y.rel
This says
{(u, y) | α(u, F(u, y))} ⊆ {(u, y) | β(f(u), y)}using subobject pullbacks
Instances For
This says {(u, y) | α(u, F(u, y))} ⊆ {(u, y) | β(f(u), y)} using subobject pullbacks
Equations
- CategoryTheory.Dial.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
An isomorphism in Dial C can be induced by isomorphisms on the source and target,
which respect the respective relations on X and Y.
Equations
- One or more equations did not get rendered due to their size.