Dialectica category

We define the category Dial of the Dialectica interpretation, after [DP89].

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. (pdf)

structure CategoryTheory.Dial (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] : Type (max u v)

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)

  A subobject of src ⨯ tgt, interpreted as a relation

theorem CategoryTheory.Dial.Hom.ext_iff {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasFiniteProducts C} {inst_2 : CategoryTheory.Limits.HasPullbacks C} {X Y : CategoryTheory.Dial C} (x y : X.Hom Y), x = y ↔ x.f = y.f ∧ x.F = y.F

theorem CategoryTheory.Dial.Hom.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasFiniteProducts C} {inst_2 : CategoryTheory.Limits.HasPullbacks C} {X Y : CategoryTheory.Dial C} (x y : X.Hom Y), x.f = y.f → x.F = y.F → x = y

structure CategoryTheory.Dial.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) : Type v

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

• F : X.src ⨯ Y.tgt ⟶ X.tgt

  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

theorem CategoryTheory.Dial.Hom.le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (self : X.Hom Y) : (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

theorem CategoryTheory.Dial.comp_le_lemma {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} {Z : CategoryTheory.Dial C} (F : X.Hom Y) (G : Y.Hom Z) : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id Z.tgt)) G.F)) F.F))).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp F.f G.f) (CategoryTheory.CategoryStruct.id Z.tgt))).obj Z.rel

@[simp]

theorem CategoryTheory.Dial.instCategory_comp_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} {Z : CategoryTheory.Dial C} (F : X.Hom Y) (G : Y.Hom Z) : (CategoryTheory.CategoryStruct.comp F G).f = CategoryTheory.CategoryStruct.comp F.f G.f

@[simp]

theorem CategoryTheory.Dial.instCategory_id_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) : (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.src

@[simp]

theorem CategoryTheory.Dial.instCategory_id_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) : (CategoryTheory.CategoryStruct.id X).F = CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.Dial.instCategory_comp_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} {Z : CategoryTheory.Dial C} (F : X.Hom Y) (G : Y.Hom Z) : (CategoryTheory.CategoryStruct.comp F G).F = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id Z.tgt)) G.F)) F.F

instance CategoryTheory.Dial.instCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Category.{v, max u v} (CategoryTheory.Dial C)

Equations

• CategoryTheory.Dial.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

theorem CategoryTheory.Dial.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} {x : X ⟶ Y} {y : X ⟶ Y} (hf : x.f = y.f) (hF : x.F = y.F) : x = y

@[simp]

theorem CategoryTheory.Dial.isoMk_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.f = e₁.inv

@[simp]

theorem CategoryTheory.Dial.isoMk_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.hom

@[simp]

theorem CategoryTheory.Dial.isoMk_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.inv

@[simp]

theorem CategoryTheory.Dial.isoMk_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.f = e₁.hom

def CategoryTheory.Dial.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : X ≅ Y

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.