Contents

(0,1)-category

(0,1)-topos

# Contents

## Idea

A regular hyperdoctrine, also called an elementary existential doctrine, is a version of a first-order hyperdoctrine that is appropriate for regular logic.

## Definition

Let $C$ be a category with finite limits. A regular hyperdoctrine, or elementary existential doctrine, over $C$ is a functor

$P \;\colon\; C^{op} \to InfSemiLattice$

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

###### Remark

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.

## References

• 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 August 19, 2021 at 05:30:06. See the history of this page for a list of all contributions to it.