nLab
Heyting category

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).

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, where the subobject monomorphism from AA to XX is mm, (AB):= m(AB)(A\Rightarrow B) := \forall_m(A\wedge B), where ABA\wedge B is considered as a subobject of AA. 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.

A Heyting functor is a coherent functor betwen 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.

References

Revised on October 10, 2013 07:11:21 by Urs Schreiber (82.113.121.201)