He interprets geometric morphisms as “Contrasts” between cohesion and non-cohesion and between variation and non-variation. There is also a distinction between cohesion and variation.
A full and faithful functor between extensive categories which is a Frobenius functor in that it is reflective and coreflective by the same functor (i.e. there is a s.t. ) by definition exhibits as a quality type over .
Short: A quality type is a full and faithful Frobenius pair/triple.
Let be cartesian-closed extensive categories. is called a category of cohesion relative to if
is an adjoint quadruple of functors such that
(a) preserves finite products and is full and faithful. Thus for toposes this would be phrased as is “connected surjective” and “local”, is a subtopos, and is an exponential ideal.
(b) preserves -parametrized powers in that
is a natural isomorphism for all and all . This “continuity” property follows from (a) if all hom sets in are finite; it also holds if the contrast with is determined as in IV below ba an infinitely divisible interval in .
(c) The canonical map in is epimorphic (Schreiber calls this “pieces have points”). This holds iff the other canonical map in is monomorphic (Schreiber calls this “discrete objects are concrete). Lawvere calls this property the ”Nullstellensatz“.
The functors directed “downwards” (i.e. and ) express the opposition between “points” and “pieces”.
The functors directed “upwards” (i.e. and ) express the opposition between “pure anti-cohesion” (discreteness) and “pure cohesion” (codiscreteness).
(c) implies that “mapping pieces of a product to the product of pieces” is an epimorphism.
If (c) is an isomorphism, this implies (a) and (b). In particular a cartesian closed quality type is a category of cohesion (in an extreme sense).
An extensive quality quality on a category of cohesion is defined to be a functor such that
preserves finite coproducts
the codomain of is a quality type
i.e. an extensive quality of has the same number of connected pieces as .
Any category of cohesion has a canonical extensive quality defined by where is the identity on objects and preserves finite products and exponentiation.
An intensive quality on a category of cohesion is a functor from to a quality type such that
preserves finite products and finite coproducts.