nLab Heyting category



Regular and Exact categories

∞-ary regular and exact categories



Category Theory

Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




A Heyting category (called a logos in Freyd-Scedrov) is a coherent category in which each base change functor f *:Sub(Y)Sub(X)f^*:Sub(Y)\to Sub(X) has a right adjoint f\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 Sub:𝒞 opHeytAlg\mathrm{Sub}:\mathcal{C}^{op} \to HeytAlg.

It follows that each poset of subobjects Sub(X)Sub(X) is a Heyting algebra and the base-change functors f *f^* are Heyting algebra homomorphisms. The Heyting implication can be defined as follows: if AA and BB are subobjects of XX, then we can define (AB)Sub(X)(A\Rightarrow B) \in Sub(X) as i(AB)X\forall_i(A\cap B) \hookrightarrow X, where i:AXi\colon A\hookrightarrow X is the subobject inclusion and we take ABSub(A)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 f\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 f\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.

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus


Last revised on November 5, 2023 at 02:40:40. See the history of this page for a list of all contributions to it.