nLab Heyting category

Redirected from "Heyting functors".
Contents

Context

Regular and Exact categories

∞-ary regular and exact categories

regularity

exactness

Category Theory

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Definition

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.

Examples

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

References

Last revised on September 13, 2024 at 22:43:36. See the history of this page for a list of all contributions to it.