∞-ary regular and exact categories
arity class: unary, finitary, infinitary
regularity
regular category = unary regular
coherent category = finitary regular
geometric category = infinitary regular
exactness
exact category = unary exact
A Heyting category (called a logos in Freyd-Scedrov) is a coherent category in which each base change functor $f^*:Sub(Y)\to Sub(X)$ has a right adjoint $\forall_f$ (the universal quantifier, in addition to the left adjoint existential quantifier that exists in any regular category). Thus, every Heyting category $\mathcal{C}$ is a first-order hyperdoctrine given by the subobject poset functor $\mathrm{Sub}:\mathcal{C}^{op} \to HeytAlg$.
It follows that each poset of subobjects $Sub(X)$ is a Heyting algebra and the base-change functors $f^*$ are Heyting algebra homomorphisms. The Heyting implication can be defined as follows: if $A$ and $B$ are subobjects of $X$, then we can define $(A\Rightarrow B) \in Sub(X)$ as $\forall_i(A\cap B) \hookrightarrow X$, where $i\colon A\hookrightarrow X$ is the subobject inclusion and we take $A \cap B\in Sub(A)$. Any Heyting category has an internal logic which is full (typed) first-order intuitionistic logic. The extra right adjoint $\forall_f$ provided by the above axiom gives the universal quantifier in this logic. On the other hand, any category defined in intuitionistic logic which satisfies bounded separation is a Heyting category.
A Heyting functor is a coherent functor between Heyting categories which additionally preserves the right adjoints $\forall_f$. Such functors also preserve the internal interpretation of first-order logic.
Any topos, and in fact any well-powered infinitary coherent category, is a Heyting category. Any Boolean category is also a Heyting category.
Every locally cartesian closed coherent category is a Heyting category, because the dependent product functors preserve monomorphisms. This implies that every Pi-pretopos is a Heyting pretopos.
In particular, the h-sets in Martin-Löf type theory with propositional truncations form a Heyting category.
Last revised on November 5, 2023 at 02:40:40. See the history of this page for a list of all contributions to it.