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, is a version of a first-order hyperdoctrine that is appropriate for regular logic.
Let $C$ be a category with finite limits. A regular hyperdoctrine, or elementary existential doctrine, over $C$ is a functor
from the opposite category of $C$ to the category of inf-semilattices, such that for every morphism $f : A \to B$ in $C$, the functor $P(A) \to P(B)$ has a left adjoint $\exists_f$ 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 $\exists_f$ 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)
Last revised on November 16, 2022 at 06:02:17. See the history of this page for a list of all contributions to it.