# nLab Heyting category

### Context

#### Regular and Exact categories

κ-ary regular and exact categories

regularity

exactness

category theory

## Applications

#### Topos Theory

Could not include topos theory - contents

# Contents

## Definition

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

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

A Heyting functor is a coherent functor betwen Heyting categories which additionally preserves the right adjoints $\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)