Documentation

Mathlib.CategoryTheory.Dialectica.Basic

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 #

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.

Instances For
    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.fx.F = y.Fx = y

    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)}.

    Instances For

      This says {(u, y) | α(u, F(u, y))} ⊆ {(u, y) | β(f(u), y)} using subobject pullbacks

      @[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

      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.
      Instances For