Commit 2024-07-03 10:14 5d74b273

View on Github →

feat: the Dialectica category (#14274) Co-authored with Valeria de Paiva. This defines the category Dial(C) which is a categorical interpretation of Gödel's "Dialectica interpretation" of higher order arithmetic.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Dialectica/Basic.lean

added structure CategoryTheory.Dial.Hom

added theorem CategoryTheory.Dial.comp_le_lemma

added theorem CategoryTheory.Dial.hom_ext

added def CategoryTheory.Dial.isoMk

added structure CategoryTheory.Dial

Created Mathlib/CategoryTheory/Dialectica/Monoidal.lean

added def CategoryTheory.Dial.associator

added theorem CategoryTheory.Dial.associator_naturality

added def CategoryTheory.Dial.braiding

added theorem CategoryTheory.Dial.braiding_naturality_left

added theorem CategoryTheory.Dial.braiding_naturality_right

added theorem CategoryTheory.Dial.hexagon_forward

added theorem CategoryTheory.Dial.hexagon_reverse

added def CategoryTheory.Dial.leftUnitor

added theorem CategoryTheory.Dial.leftUnitor_naturality

added theorem CategoryTheory.Dial.pentagon

added def CategoryTheory.Dial.rightUnitor

added theorem CategoryTheory.Dial.rightUnitor_naturality

added theorem CategoryTheory.Dial.symmetry

added def CategoryTheory.Dial.tensorHom

added def CategoryTheory.Dial.tensorObj

added def CategoryTheory.Dial.tensorUnit

added theorem CategoryTheory.Dial.tensor_comp

added theorem CategoryTheory.Dial.tensor_id

added theorem CategoryTheory.Dial.triangle

Modified docs/references.bib