(0,1)-category

(0,1)-topos

# Contents

## Definition

Let $C$ be a category with finite limits. A coherent hyperdoctrine over $C$ is a functor

$P:{C}^{\mathrm{op}}\to \mathrm{DistLattice}$P : C^{op} \to DistLattice

from the opposite category of $C$ to the category of distributive lattices, such that for every morphism $f:A\to B$ in $C$, the functor $P\left(A\right)\to P\left(B\right)$ has a left adjoint ${\exists }_{f}$ satisfying

## Properties

The assignment (here) of a coherent hyperdoctrine $S\left(C\right)$ to a coherent category $C$ extends to a 2-adjunction

$\left(A⊣S\right):\mathrm{CoherentCat}\stackrel{\stackrel{A}{←}}{\underset{S}{↪}}\mathrm{CoherentHyperdoctrine}$(A \dashv S) : CoherentCat \stackrel{\overset{A}{\leftarrow}}{\underset{S}{\hookrightarrow}} CoherentHyperdoctrine

with the right adjoint being a full and faithful 2-functor, hence exhibiting $\mathrm{CoherentCat}$ as a reflective sub-2-category of $\mathrm{CoherentHyperdoctrine}$.

(Here $\mathrm{CoherentCat}$ has as 2-morphisms those natural transformations that preserve finite products.)

This appears as (Coumans, prop. 8).

Coherent hyperdoctrines are closed under canonical extension $\left(-{\right)}^{\delta }:\mathrm{DistLattice}\to \mathrm{DistLattice}$, in that for $P:{C}^{\mathrm{op}}\to \mathrm{DistLattic}$ a coherent hyperdoctrine, so is $\left(-{\right)}^{\delta }\circ P$.

This appears as (Coumans, prop. 9).

## Examples

### Powersets

The powerset functor

$P:=\left\{0,1{\right\}}^{\left(-\right)}:{\mathrm{Set}}^{\mathrm{op}}\to \mathrm{DistLattice}$P := \{0,1\}^{(-)} : Set^{op} \to DistLattice

(sending a set to its power set and a function to the preimage-assignment) is a coherent hyperdoctrine.

### Over a coherent category

Let $C$ be a coherent category. For every object $A\in C$ the poset of subobjects ${\mathrm{Sub}}_{C}\left(A\right)$ is a distributive lattice.

The corresponding functor

${C}^{\mathrm{op}}\to \mathrm{DistLattice}$C^{op} \to DistLattice

from the opposite category of $C$ to the category of distributive lattices is called the coherent hyperdoctrine of $C$.

### For a coherent theory

Accordingly, there is a coherent hyperdoctrine associated with any coherent theory, where the objects of $C$ are lists of free variables in the theory, and the lattice assigned to them is that of propositions of the theory in this context.

## References

• Dion Coumans, Generalizing canonical extensions to the categorical setting (Arxiv)

Revised on May 24, 2013 00:46:08 by David Corfield (87.113.28.17)