nLab Adjointness in Foundations

This page collects links related to the text

  • William Lawvere,

    Adjointness in Foundations,

    Dialectica 23 (1969), 281-296,

    Reprints in Theory and Applications of Categories, No. 16 (2006), pp 1-16 (revised 2006-10-30)

    (TAC)

on foundations of mathematics in categorical logic and the role of adjoints in the formalization of quantifiers (base change). The main point is that the logical operations on propositions

existential quantifier⊣\dashv context extension ⊣\dashv universal quantifier

constitute an adjoint triple. In type theory this is lifted from operations on propositions to operations on types, where it becomes

dependent sum⊣\dashv context extension ⊣\dashv dependent product.

In topos theory and geometry this adjoint triple is often known as base change.

category: reference

Last revised on May 24, 2023 at 21:11:01. See the history of this page for a list of all contributions to it.