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 know as base change.

category: reference

Last revised on July 3, 2018 at 04:51:03. See the history of this page for a list of all contributions to it.