natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A regular hyperdoctrine, also called an elementary existential doctrine or a regular fibration, is a version of a first-order hyperdoctrine that is appropriate for regular logic.
Let be a category with finite limits. A regular hyperdoctrine, or elementary existential doctrine, over is a functor
from the opposite category of to the category of inf-semilattices, such that for every morphism in , the functor has a left adjoint satisfying
The original definition of Lawvere did not include the last two conditions and allowed the values of the functor to be arbitrary categories with finite products. Other references sometimes require the adjoints to be defined only along projections (corresponding to ordinary existential quantification in logic) and diagonals (corresponding to equality); Lawvere showed that in the presence of Frobenius and Beck-Chevalley more general quantifiers can be constructed in terms of these.
William Lawvere, Equality in hyperdoctrines and comprehension schema as an adjoint functor
Davide Trotta, The existential completion, 2021 (arxiv:2108.03416)
Davide Trotta, An algebraic approach to the completions of elementary doctrines, 2021 (arxiv:2108.03415)
Bart Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf, webpage]
Last revised on February 19, 2024 at 22:43:15. See the history of this page for a list of all contributions to it.