# User:Michiexile/MATH198/Lecture 10

### From HaskellWiki

(Difference between revisions)
|                                        |                                                                                                                                                                |                                                         |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|----------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
|                                        |                                                                                                                                                                | Current revision (18:21, 2 December 2009) (edit) (undo) |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| (11 intermediate revisions not shown.) |                                                                                                                                                                |                                                         |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| Line 1:                                |                                                                                                                                                                | Line 1:                                                 |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| -                                      | IMPORTANT NOTE: THESE NOTES ARE STILL UNDER DEVELOPMENT. PLEASE WAIT UNTIL AFTER THE LECTURE WITH HANDING ANYTHING IN, OR TREATING THE NOTES AS READY TO READ. | +                                                       | This lecture will be shallow, and leave many things undefined, hinted at, and is mostly meant as an appetizer, enticing the audience to go forth and seek out the literature on topos theory for further studies.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ===Subobject classifier===                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | One very useful property of the category <math>Set</math> is that the powerset of a given set is still a set; we have an internal concept of ''object of all subobjects''. Certainly, for any category (small enough) <math>C</math>, we have a contravariant functor <math>Sub(-): C\to Set</math> taking an object to the set of all equivalence classes of monomorphisms into that object; with the image <math>Sub(f)</math> given by the pullback diagram                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:SubobjectFunctorMorphismPullback.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | If the functor <math>Sub(-)</math> is ''representable'' - meaning that there is some object <math>X\in C_0</math> such that <math>Sub(-) = hom(-,X)</math> - then the theory surrounding representable functors, connected to the Yoneda lemma - give us a number of good properties.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | One of them is that every representable functor has a ''universal element''; a generalization of the kind of universal mapping properties we've seen in definitions over and over again during this course; all the definitions that posit the unique existence of some arrow in some diagram given all other arrows.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Thus, in a category with a representable subobject functor, we can pick a representing object <math>\Omega\in C_0</math>, such that <math>Sub(X) = hom(X,\Omega)</math>. Furthermore, picking a universal element corresponds to picking a subobject <math>\Omega_0\hookrightarrow\Omega</math> such that for any object <math>A</math> and subobject <math>A_0\hookrightarrow A</math>, there is a unique arrow <math>\chi: A\to\Omega</math> such that there is a pullback diagram                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:SubobjectClassifierPullback.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | One can prove that <math>\Omega_0</math> is terminal in <math>C</math>, and we shall call <math>\Omega</math> the ''subobject classifier'', and this arrow <math>\Omega_0=1\to\Omega</math> ''true''. The arrow <math>\chi</math> is called the characteristic arrow of the subobject.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | In Set, all this takes on a familiar tone: the subobject classifier is a 2-element set, with a ''true'' element distinguished; and a characteristic function of a subset takes on the ''true'' value for every element in the subset, and the other (false) value for every element not in the subset.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ===Defining topoi===                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Definition''' A ''topos'' is a cartesian closed category with all finite limits and with a subobject classifier.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | It is worth noting that this is a far stronger condition than anything we can even hope to fulfill for the category of Haskell types and functions. The functional programming relevance will take a back seat in this lecture, in favour of usefulness in logic and set theory replacements.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ===Properties of topoi===                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | The meat is in the properties we can prove about topoi, and in the things that turn out to be topoi.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Theorem''' Let <math>E</math> be a topos.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       | * <math>E</math> has finite colimits.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ====Power object====                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Since a topos is closed, we can take exponentials. Specifically, we can consider <math>[A\to\Omega]</math>. This is an object such that <math>hom(B,[A\to\Omega]) = hom(A\times B, \Omega) = Sub(A\times B)</math>. Hence, we get an internal version of the subobject functor. (pick <math>B</math> to be the terminal object to get a sense for how global elements of <math>[A\to\Omega]</math> correspond to subobjects of <math>A</math>)                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ====Internal logic====                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We can use the properties of a topos to develop a logic theory - mimicking the development of logic by considering operations on subsets in a given universe:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Classically, in Set, and predicate logic, we would say that a ''predicate'' is some function from a universe to a set of truth values. So a predicate takes some sort of objects, and returns either True or False.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Furthermore, we allow the definition of sets using predicates:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | :<math>\{x\in U: P(x)\}</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Looking back, though, there is no essential difference between this, and defining the predicate as the subset of the universe directly; the predicate-as-function appears, then, as the characteristic function of the subset. And types are added as easily - we specify each variable, each object, to have a set it belongs to.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | This way, predicates really are subsets. Type annotations decide which set the predicate lives in. And we have everything set up in a way that opens up for the topos language above.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We'd define, for predicates <math>P, Q</math> acting on the same type:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | :<math>\{x\in A : \top\} = A</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | :<math>\{x\in A : \bot\} = \emptyset</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       | :<math>\{x : (P \wedge Q)(x)\} = \{x : P(x)\} \cap \{x : Q(x)\}</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | :<math>\{x : (P \vee Q)(x)\} = \{x : P(x)\} \cup \{x : Q(x)\}</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       | :<math>\{x\in A : (\neg P)(x) \} = A \setminus \{x\in A : P(x)\}</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We could then start to define primitive logic connectives as set operations; the intersection of two sets is the set on which '''both''' the corresponding predicates hold true, so <math>\wedge = \cap</math>. Similarily, the union of two sets is the set on which either of the corresponding predicates holds true, so <math>\vee = \cup</math>. The complement of a set, in the universe, is the negation of the predicate, and all other propositional connectives (implication, equivalence, ...) can be built with conjunction (and), disjunction (or) and negation (not).                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | So we can mimic all these in a given topos:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We say that a ''universe'' <math>U</math> is just an object in a given topos. (Note that by admitting several universes, we arrive at a ''typed'' predicate logic, with basically no extra work.)                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | A ''predicate'' is a subobject of the universe.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We can now proceed to define all the familiar logic connectives one by one, using the topos setting. While doing this, we shall introduce the notation <math>t_A: A\to\Omega</math> for the morphism <math>t_A = A\to 1\to^{true}\Omega</math> that takes on the value ''true'' on all of A. We note that with this convention, <math>\chi_{A_0}</math>, the characteristic morphism of a subobject, is the arrow such that <math>\chi_{A_0}\circ i = t_{A_0}</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Conjunction''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | Given predicates <math>P, Q</math>, we need to define the ''conjunction'' <math>P\wedge Q</math> as some <math>P\wedge Q: U\to\Omega</math> that corresponds to both <math>P</math> and <math>Q</math> simultaneously.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We may define <math>true\times true: 1\to\Omega\times\Omega</math>, a subobject of <math>\Omega\times\Omega</math>. Being a subobject, this has a characteristic arrow <math>\wedge:\Omega\times\Omega\to\Omega</math>, that we call the ''conjunction arrow''.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Now, we may define <math>\chi_P\times\chi_Q:U\to\Omega\times\Omega</math> for subobjects <math>P,Q\subseteq U</math> - and we take their composition <math>\wedge\circ\chi_P\times\chi_Q</math> to be the characteristic arrow of the subobject <math>P\wedge Q</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | And, indeed, this results in a topoidal version of intersection of subobjects.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Implication''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | Next we define <math>\leq_1: \Omega_1\to\Omega\times\Omega</math> to be the equalizer of <math>\wedge</math> and <math>proj_1</math>. Given <math>v, w: U\to\Omega</math>, we write <math>v\leq_1 w</math> if <math>v\times w</math> factors through <math>\leq_1</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Using the definition of an equalizer we arrive at <math>v\leq_1 w</math> iff <math>v = v\wedge w</math>. From this, we can deduce                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | :<math>u\leq_1 true</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | :<math>u\leq_1 u</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | :If <math>u\leq_1 v</math> and <math>v\leq_1 w</math> then <math>u\leq_1 w</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | :If <math>u\leq_1 v</math> and <math>v\leq_1 u</math> then <math>u=v</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       | and thus, <math>\leq_1</math> is a partial order on <math>[U\to\Omega]</math>. Intuitively, <math>u\leq_1 v</math> if <math>v</math> is at least as true as <math>u</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | This relation corresponds to inclusion on subobjects. Note that <math>\leq_1:\Omega_1\to\Omega\times\Omega</math>, given from the equalizer, gives us <math>\Omega_1</math> as a ''relation'' on <math>\Omega</math> - a subobject of <math>\Omega\times\Omega</math>. Specifically, it has a classifying arrow <math>\Rightarrow:\Omega\times\Omega\to\Omega</math>. We write <math>h\Rightarrow k = (\Rightarrow)\circ h\times k</math>. And for subobjects <math>P,Q\subseteq A</math>, we write <math>P\Rightarrow Q</math> for the subobject classified by <math>\chi_P\Rightarrow\chi_Q</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | It turns out, without much work, that this <math>P\Rightarrow Q</math> behaves just like classical implication in its relationship to <math>\wedge</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Membership''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | We can internalize the notion of ''membership'' as a subobject <math>\in^U\subseteq U\times\Omega^U</math>, and thus get the membership relation from a pullback:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposMembershipPullback.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | For elements <math>x\times h: 1\to U\times\Omega^U</math>, we write <math>x\in^U h</math> for <math>x\times h\in\in^U</math>. Yielding a subset of the product <math>U\times\Omega^U</math>, this is readily interpretable as a relation relating things in <math>U</math> with subsets of <math>U</math>, so that for any <math>x,h</math> we can answer whether <math>x\in^Uh</math>. Both notations indicate <math>ev_A\circ h\times x = true</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Universal quantification''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | For any object <math>U</math>, the maximal subobject of <math>U</math> is <math>U</math> itself, embedded with <math>1_U</math> into itself. There is an arrow <math>\tau_U:1\to\Omega^U</math> represents this subobject. Being a map from <math>1</math>, it is specifically monic, so it has a classifying arrow <math>\forall_U:\Omega^U\to\Omega</math> that takes a given subobject of <math>U</math> to <math>true</math> precisely if it is in fact the maximal subobject.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Now, with a relation <math>r:R\to B\times A</math>, we define <math>\forall a. R</math> by the following pullback:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposForallPullback.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | where <math>\lambda\chi_R</math> comes from the universal property of the exponential.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Theorem''' For any <math>s:S\to B</math> monic, <math>S\subseteq \forall a.R</math> iff <math>S\times A\subseteq R</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | This theorem tells us that the subobject given by <math>\forall a.R</math> is the largest subobject of <math>B</math> that is related by <math>R</math> to all of <math>A</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Falsum''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | We can define the ''false'' truth value using these tools as <math>\forall w\in\Omega.w</math>. This might be familiar to the more advanced Haskell type hackers - as the type                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | <haskell>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | x :: forall a. a                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | </haskell>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | which has to be able to give us an element of any type, regardless of the type itself. And in Haskell, the only element that inhabits all types is <hask>undefined</hask>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | From a logical perspective, we use a few basic inference rules:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposTrivialSequent.png]] [[Image:ToposForallConnective.png]] [[Image:ToposSubstitution.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | and connect them up to derive                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposFalsumDerivation.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       | for any <math>\phi</math> not involving <math>w</math> - and we can always adjust any <math>\phi</math> to avoid <math>w</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Thus, the formula <math>\forall w.w</math> has the property that it implies everything - and thus is a good candidate for the ''false'' truth value; since the inference                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposExFalsoQuodlibet.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       | is the defining introduction rule for false.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Negation''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | We define negation the same way as in classical logic: <math>\neg \phi = \phi \Rightarrow false</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Disjunction''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | We can define                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | :<math>P\vee Q = \forall w. ((\phi\Rightarrow w)\wedge(\psi\Rightarrow w))\Rightarrow w</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Note that this definition uses one of our primary inference rules:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposDisjunctionConnective.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | as the defining property for the disjunction, and we may derive any properties we like from these.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Existential quantifier''':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | Finally, the existential quantifier is derived similarly to the disjunction - by figuring out a rule we want it to obey, and using that as a definition for it:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | :<math>\exists x.\phi = \forall w. (\forall x. \phi \Rightarrow w)\Rightarrow w</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Here, the rule we use as defining property is                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:ToposExistsConnective.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Before we leave this exploration of logic, some properties worth knowing about:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | While we can prove <math>\neg(\phi\wedge\neg\phi)</math> and <math>\phi\Rightarrow\neg\neg\phi</math>, we cannot, in just topos logic, prove things like                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       | :<math>\neg(\phi\wedge\psi)\Rightarrow(\neg\phi\vee\neg\psi)</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | :<math>\neg\neg\phi\Rightarrow\phi</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | nor any statements like                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | :<math>\neg(\forall x.\neg\phi)\Rightarrow(\exists x.\phi)</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | :<math>\neg(\forall x.\phi)\Rightarrow(\exists x.\neg\phi)</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | :<math>\neg(\exists x.\neg\phi)\Rightarrow(\forall x.\phi)</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | We can, though, prove                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       | :<math>\neg(\exists x.\phi)\Rightarrow(\forall x.\neg\phi)</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | If we include, extra, an additional inference rule (called the ''Boolean negation rule'') given by                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:BooleanNegation.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | then suddenly we're back in classical logic, and can prove <math>\neg\neg\phi\Rightarrow\phi</math> and <math>\phi\or\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ====Examples: Sheaves, topology and time sheaves====                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | The first interesting example of a topos is the category of (small enough) sets; in some sense clear already since we've been modelling our axioms and workflows pretty closely on the theory of sets.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Generating logic and set theory in the topos of sets, we get a theory that captures several properties of ''intuitionistic logic''; such as the lack of Boolean negation, of exclusion of the third, and of double negation rules.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | For the more interesting examples, however, we shall introduce the concepts of ''topology'' and of ''sheaf'':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Definition''' A (set-valued) ''presheaf'' on a category <math>C</math> is a contravariant functor <math>E: C^{op}\to Set</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Presheaves occur all over the place in geometry and topology - and occasionally in computer science too: There is a construction in which a functor <math>A\to Set</math> for a discrete small category <math>A</math> identified with its underlying set of objects as a set, corresponds to the data type of ''bags'' of elements from <math>A</math> - for <math>a\in A</math>, the image <math>F(a)</math> denotes the multiplicity of <math>a</math> in the bag.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Theorem''' The category of all presheaves (with natural transformations as the morphisms) on a category <math>C</math> form a topos.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Example''' Pick a category on the shape                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:GraphsAsPresheaves.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | A contravariant functor on this category is given by a pair of sets <math>G_0, G_1</math> and a pair of function <math>source, target: G_1\to G_0</math>. Identities are sent to identities.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | The category of presheaves on this category, thus, is the category of graphs. Thus graphs form a topos.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | The subobject classifier in the category of graphs is a graph with two nodes: in and out, and five arrows:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | :<math>in \to^{all} in</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | :<math>in \to^{both} in</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | :<math>in \to^{source} out</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | :<math>out \to^{target} in</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | :<math>out \to^{neither} out</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | Now, given a subgraph <math>H \leq G</math>, we define a function <math>\chi_H:G\to\Omega</math> by sending nodes to in or out dependent on their membership. For an arrow <math>a</math>, we send it to all if the arrow is in <math>H</math>, and otherwise we send it to both/source/target/neither according to where its source and target reside.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | To really get into sheaves, though, we introduce more structure - specifically, we define what we mean by a ''topology'':                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Definition''' Suppose <math>P</math> is a partially ordered set. We call <math>P</math> a ''complete Heyting algebra'' if                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       | * There is a top element <math>1</math> such that <math>x\leq 1 \forall x\in P</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | * Any two elements <math>x, y</math> have an infimum (greatest lower bound) <math>x\wedge y</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | * Every subset <math>Q\subseteq P</math> has a supremum (least upper bound) <math>\bigvee_{p\in P} p</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       | * <math>x\wedge(\bigvee y_i) = \bigvee x\wedge y_i</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Note that for the partial order by inclusion of a family of subsets of a given set, being a complete Heyting algebra is the same as being a topology in the classical sense - you can take finite unions and any intersections of open sets and still get an open set.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | If <math>\{x_i\}</math> is a subset with supremum <math>x</math>, and <math>E</math> is a presheaf, we get functions <math>e_i:E(x)\to E(x_i)</math> from functoriality. We can summarize all these <math>e_i</math> into <math>e = \prod_i e_i: E(x)\to\prod_i E(x_i)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Furthermore, functoriality gives us families of functions <math>c_{ij}: E(x_i)\to E(x_i\wedge x_j)</math> and <math>d_{ij}: E(x_j)\to E(x_i\wedge x_j)</math>. These can be collected into <math>c: \prod_i E(x_i)\to\prod_{ij}E(x_i\wedge x_j)</math> and <math>d:\prod_j E(x_j)\to\prod_{ij}E(x_i\wedge x_j)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Definition''' A presheaf <math>E</math> on a Heyting algebra is called a ''sheaf'' if it satisfies:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | :<math>x = \bigvee x_i</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | implies that                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       | :[[Image:SheafEqualizer.png]]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       | is an equalizer. If you have seen sheaves before, you may recognize this as the covering axiom.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | In other words, <math>E</math> is a sheaf if whenever <math>x=\bigvee x_i</math> and <math>c(\alpha) = d(\alpha)</math>, then there is some <math>\bar\alpha</math> such that <math>\alpha = e(\bar\alpha)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Theorem''' The category of sheaves on a Heyting algebra is a topos.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | For context, we can think of sheaves over Heyting algebras as sets in a logic with an expanded notion of truth. Our Heyting algebra is the collection of truth values, and the sheaves are the fuzzy sets with fuzziness introduced by the Heyting algebra.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | Recalling that subsets and predicates are viewed as the same thing, we can view the set <math>E(p)</math> as the part of the fuzzy set <math>E</math> that is at least <math>p</math> true.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | As it turns out, to really make sense of this approach, we realize that ''equality'' is a predicate as well - and thus can hold or not depending on the truth value we use.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Definition''' Let <math>P</math> be a complete Heyting algebra. A ''<math>P</math>-valued set'' is a pair <math>(S,\sigma)</math> of a set <math>S</math> and a function <math>\sigma: S\to P</math>. A ''category of fuzzy sets'' is a category of <math>P</math>-valued sets. A morphism <math>f:(S,\sigma)\to(T,\tau)</math> of <math>P</math>-valued sets is a function <math>f:S\to T</math> such that <math>\tau\circ f = \sigma</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | From these definitions emerges a fuzzy set theory where all components of it being a kind of set theory emerges from the topoidal approach above. Thus, say, subsets in a fuzzy sense are just monics, thus are injective on the set part, and such that the valuation, on the image of the injection, increases from the previous valuation: <math>(T,\tau)\subseteq(S,\sigma)</math> if <math>T\subseteq S</math> and <math>\sigma|_T = \tau</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | To get to topoi, though, there are a few matters we need to consider. First, we may well have several versions of the empty set - either a bona fide empty set, or just a set where every element is never actually there. This issue is minor. Much more significant though, is that while we can easily make <math>(S,\sigma)</math> give rise to a presheaf, by defining                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       | :<math>E(x) = \{s\in S: \sigma(s)\geq x\}</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | this definition will not yield a sheaf. The reason for this boils down to <math>E(0) = S \neq 1</math>. We can fix this, though, by adjoining another element - <math>\bot</math> - to <math>P</math> giving <math>P^+</math>. The new element <math>\bot</math> is imbued with two properties: it is smaller, in <math>P^+</math>, than any other element, and it is mapped, by <math>E</math> to <math>1</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Theorem''' The construction above gives a fuzzy set <math>(S,\sigma)</math> the structure of a sheaf on the augmented Heyting algebra.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Corollary''' The category of fuzzy sets for a Heyting algebra <math>P</math> forms a topos.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | '''Final note''' While this construction allows us to make ''membership'' a fuzzy concept, we're not really done fuzzy-izing sets. There are two fundamental predicates on sets: equality and membership. While fuzzy set theory, classically, only allows us to make one of these fuzzy, topos theory allows us - rather easily - to make both these predicates fuzzy. Not only that, but membership reduces - with the power object construction - to equality testing, by which the fuzzy set theory ends up somewhat inconsistent in its treatment of the predicates.                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ===Literature===                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | At this point, I would warmly recommend the interested reader to pick up one, or more, of:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | * Steve Awodey: Category Theory                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | * Michael Barr & Charles Wells: Categories for Computing Science                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | * Colin McLarty: Elementary Categories, Elementary Toposes                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | or for more chewy books                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | * Peter T. Johnstone: Sketches of an Elephant: a Topos Theory compendium                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       | * Michael Barr & Charles Wells: Toposes, Triples and Theories                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ===Exercises===                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | No homework at this point. However, if you want something to think about, a few questions and exercises:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | # Prove the relations showing that <math>\leq_1</math> is indeed a partial order on <math>[U\to\Omega]</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | # Prove the universal quantifier theorem.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | # The ''extension'' of a formula <math>\phi</math> over a list of variables <math>x</math> is the sub-object of the product of domains <math>A_1\times\dots\times A_n</math> for the variables <math>x_1,\dots,x_n=x</math> classified by the interpretation of <math>\phi</math> as a morphism <math>A_1\times\dots\times A_n\to\Omega</math>. A formula is ''true'' if it classifies the entire product. A ''sequent'', written <math>\Gamma:\phi</math> is the statement that using the set of formulae <math>\Gamma</math> we may prove <math>\phi</math>, or in other words that the intersection of the extensions of the formulae in <math>\Gamma</math> is contained in the extension of <math>\phi</math>. If a sequent <math>\Gamma:\phi</math> is true, we say that <math>\Gamma</math> ''entails'' <math>\phi</math>. (some of the questions below are almost embarrassingly immediate from the definitions given above. I include them anyway, so that a ''catalogue'' of sorts of topoidal logic inferences is included here) |
|                                        |                                                                                                                                                                | +                                                       | ## Prove the following entailments:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | ### Trivial sequent: <math>\phi:\phi</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       | ### True: <math>:true</math> (note that true classifies the entire object)                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | ### False: <math>false:\phi</math> (note that false classifies the global minimum in thepreorder of subobjects)                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ## Prove the following inference rules:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | ### Implication: <math>\Gamma,\phi:\psi</math> is equivalent to <math>\Gamma:\phi\Rightarrow\psi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       | ### Thinning: <math>\Gamma:\phi</math> implies <math>\Gamma,\psi:\phi</math>                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       | ### Cut: <math>\Gamma,\psi:\phi</math> and <math>\Gamma:\psi</math> imply <math>\Gamma:\phi</math> if every variable free in <math>\psi</math> is free in <math>\Gamma</math> or in <math>\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | ### Negation: <math>\Gamma, \phi: false</math> is equivalent (implications both ways) to <math>\Gamma: \neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | ### Conjunction: <math>\Gamma:\phi</math> and <math>\Gamma:\psi</math> together are equivalent to <math>\Gamma:\phi\wedge\psi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       | ### Disjunction: <math>\Gamma,\phi:\theta</math> and <math>\Gamma,\psi:\theta</math> together imply <math>\Gamma, \phi\vee\psi: \theta</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | ### Universal: <math>\Gamma:\phi</math> is equivalent to <math>\Gamma:\forall x.\phi</math> if <math>x</math> is not free in <math>\Gamma</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | ### Existential: <math>\Gamma,\phi: \psi</math> is equivalent to <math>\Gamma,\exists x.\phi:\psi</math> if <math>x</math> is not free in <math>\Gamma</math> or <math>\psi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | ### Equality: <math>:q=q</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | ### Biconditional: <math>(v\Rightarrow w)\wedge(w\Rightarrow v):v=w</math>. We usually write <math>v\Leftrightarrow w</math> for <math>v=w</math> if <math>v,w:A\to\Omega</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | ### Product: <math>p_1u = p_1u', p_2u = p_2u' : u = u'</math> for <math>u,u'\in A\times B</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | ### Product revisited: <math>:(p_1(s\times s')=s)\wedge(p_2(s\times s')=s')</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | ### Extensionality: <math>\forall x\in A. f(x) = g(x) : f = g</math> for <math>f,g\in[A\to B]</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       | ### Comprehension: <math>(\lambda x\in A. s)x = s</math> for <math>x\in A</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | ## Prove the following results from the above entailments and inferences -- or directly from the topoidal logic mindset:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       | ### <math>:\neg(\phi\wedge\neg\phi)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
|                                        |                                                                                                                                                                | +                                                       | ### <math>:\phi\Rightarrow\neg\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | ### <math>:\neg(\phi\vee\psi)\Rightarrow(\neg\phi\wedge\neg\psi)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|                                        |                                                                                                                                                                | +                                                       | ### <math>:(\neg\phi\wedge\neg\psi)\Rightarrow\neg(\phi\wedge\psi)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | ### <math>:(\neg\phi\vee\neg\psi)\Rightarrow\neg(\phi\vee\psi)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\phi\wedge(\theta\vee\psi)</math> is equivalent to <math>(\phi\wedge\theta)\vee(\phi\wedge\psi)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\forall x.\neg\phi</math> is equivalent to <math>\neg\exists x.\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\exists x\phi\Rightarrow\neg\forall x.\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\exists x\neg\phi\Rightarrow\neg\forall x.\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\forall x\phi\Rightarrow\neg\exists x.\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\phi:\psi</math> implies <math>\neg\psi:\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\phi:\psi\Rightarrow\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\phi\Rightarrow\not\phi:\not\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\not\phi\vee\psi:\phi\Rightarrow\psi</math> (but not the converse!).                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\neg\neg\neg\phi</math> is equivalent to <math>\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | ### <math>(\phi\wedge\psi)\Rightarrow\theta</math> is equivalent to <math>\phi\Rightarrow(\psi\Rightarrow\theta)</math> (currying!).                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        |
|                                        |                                                                                                                                                                | +                                                       | ## Using the Boolean negation rule: <math>\Gamma,\neg\phi:false</math> is equivalent to <math>\Gamma:\phi</math>, prove the following additional results:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\neg\neg\phi:\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | ### <math>:\phi\vee\neg\phi</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                        |                                                                                                                                                                | +                                                       | ## Show that either of the three rules above, together with the original negation rule, implies the Boolean negation rule.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | ### The converses of the three existential/universal/negation implications above.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |
|                                        |                                                                                                                                                                | +                                                       | ## The restrictions introduced for the cut rule above block the deduction of an entailment <math>:\forall x.\phi\Rightarrow\exists x.\phi</math>. The issue at hand is that <math>A</math> might not actually have members; so choosing one is not a sound move. Show that this entailment can be deduced from the premise <math>\exists x\in A. x=x</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
|                                        |                                                                                                                                                                | +                                                       | ## Show that if we extend our ruleset by the quantifier negation rule <math>\forall x\Leftrightarrow \neg\exists x.\neg</math>, then we can derive the entailment <math>:\forall w: w=t \vee w = false</math>. From this derive <math>:\phi\vee\neg\phi</math> and hence conclude that this extension gets us Boolean logic again.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | # A ''topology'' on a topos <math>E</math> is an arrow <math>j:\Omega\to\Omega</math> such that <math>j\circ true=true</math>, <math>j\circ j=j<math> and <math>j\circ\wedge = \wedge\circ j\times j</math>. For a subobject <math>S\subseteq A</math> with characteristic arrow <math>\chi_S:A\to\Omega</math>, we define its <math>j</math>-closure as the subobject <math>\bar S\subseteq A</math> classified by <math>j\circ\chi_S</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | ## Prove:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | ### <math>S\subseteq\bar S</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\bar S = \bar{\bar S}</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\bar{S\cap T} = \bar S\cap\bar T</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | ### <math>S\subseteq T</math> implies <math>\bar S\subseteq\bar T</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\bar{f^{-1}(S)} = f^{-1}(\bar S)</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
|                                        |                                                                                                                                                                | +                                                       | ## We define <math>S</math> to be <math>j</math>-closed if <math>S=\bar S</math>. It is <math>j</math>-dense if <math>\bar S=A</math>. These terms are chosen due to correspondences to classical pointset topology for the topos of sheaves over some space. For a logical standpoint, it is more helpful to look at <math>j</math> as a modality operator: "''it is <math>j</math>-locally true that''" Given any <math>u:1\to\Omega</math>, prove that the following are topologies:                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | ### <math>(u\to -): \Omega\to\Omega</math> (the ''open topology'', where such a <math>u</math> in a sheaf topos ends up corresponding to an open subset of the underlying space, and the formulae picked out are true on at least all of that subset).                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | ### <math>u\vee -): \Omega\to\Omega</math> (the closed topology, where a formula is true if its disjunction with <math>u</math> is true -- corresponding to formulae holding over at least the closed set complementing the subset picked out)                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
|                                        |                                                                                                                                                                | +                                                       | ### <math>\neg\neg: \Omega\to\Omega</math>. This may, depending on the topos, end up being interpreted as ''true so far as global elements are concerned'', or ''not false on any open set'', or other interpretations.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     |
|                                        |                                                                                                                                                                | +                                                       | ### <math>1_\Omega</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
|                                        |                                                                                                                                                                | +                                                       | ## For a topos <math>E</math> with a topology <math>j</math>, we define an object <math>A</math> to be a ''sheaf'' iff for every <math>X</math> and every <math>j</math>-dense subobject <math>S\subseteq X</math> and every <math>f:S\to A</math> there is a unique <math>g:X\to A</math> with <math>f=g\circ s</math>. In other words, <math>A</math> is an object that cannot see the difference between <math>j</math>-dense subobjects and objects. We write <math>E_j</math> for the full subcategory of <math>j</math>-sheaves.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
|                                        |                                                                                                                                                                | +                                                       | ### Prove that any object is a sheaf for <math>1_\Omega</math>.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
|                                        |                                                                                                                                                                | +                                                       | ### Prove that a subobject is dense for <math>\neg\neg</math> iff its negation is empty. Show that <math>true+false:1+1\to\Omega</math> is dense for this topology. Conclude that <math>1+1</math> is dense in <math>\Omega_{\neg\neg}</math> and thus that <math>E_{\neg\neg}</math> is Boolean.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           |

## Current revision

This lecture will be shallow, and leave many things undefined, hinted at, and is mostly meant as an appetizer, enticing the audience to go forth and seek out the literature on topos theory for further studies.

## Contents

### 1 Subobject classifier

One very useful property of the category Set is that the powerset of a given set is still a set; we have an internal concept of object of all subobjects. Certainly, for any category (small enough) C, we have a contravariant functor $Sub(-): C\to Set$ taking an object to the set of all equivalence classes of monomorphisms into that object; with the image Sub(f) given by the pullback diagram

If the functor Sub( − ) is representable - meaning that there is some object $X\in C_0$ such that Sub( − ) = hom( − ,X) - then the theory surrounding representable functors, connected to the Yoneda lemma - give us a number of good properties.

One of them is that every representable functor has a universal element; a generalization of the kind of universal mapping properties we've seen in definitions over and over again during this course; all the definitions that posit the unique existence of some arrow in some diagram given all other arrows.

Thus, in a category with a representable subobject functor, we can pick a representing object $\Omega\in C_0$, such that Sub(X) = hom(X,Ω). Furthermore, picking a universal element corresponds to picking a subobject $\Omega_0\hookrightarrow\Omega$ such that for any object A and subobject $A_0\hookrightarrow A$, there is a unique arrow $\chi: A\to\Omega$ such that there is a pullback diagram

One can prove that Ω0 is terminal in C, and we shall call Ω the subobject classifier, and this arrow $\Omega_0=1\to\Omega$ true. The arrow χ is called the characteristic arrow of the subobject.

In Set, all this takes on a familiar tone: the subobject classifier is a 2-element set, with a true element distinguished; and a characteristic function of a subset takes on the true value for every element in the subset, and the other (false) value for every element not in the subset.

### 2 Defining topoi

Definition A topos is a cartesian closed category with all finite limits and with a subobject classifier.

It is worth noting that this is a far stronger condition than anything we can even hope to fulfill for the category of Haskell types and functions. The functional programming relevance will take a back seat in this lecture, in favour of usefulness in logic and set theory replacements.

### 3 Properties of topoi

The meat is in the properties we can prove about topoi, and in the things that turn out to be topoi.

Theorem Let E be a topos.

• E has finite colimits.

#### 3.1 Power object

Since a topos is closed, we can take exponentials. Specifically, we can consider $[A\to\Omega]$. This is an object such that $hom(B,[A\to\Omega]) = hom(A\times B, \Omega) = Sub(A\times B)$. Hence, we get an internal version of the subobject functor. (pick B to be the terminal object to get a sense for how global elements of $[A\to\Omega]$ correspond to subobjects of A)

#### 3.2 Internal logic

We can use the properties of a topos to develop a logic theory - mimicking the development of logic by considering operations on subsets in a given universe:

Classically, in Set, and predicate logic, we would say that a predicate is some function from a universe to a set of truth values. So a predicate takes some sort of objects, and returns either True or False.

Furthermore, we allow the definition of sets using predicates:

$\{x\in U: P(x)\}$

Looking back, though, there is no essential difference between this, and defining the predicate as the subset of the universe directly; the predicate-as-function appears, then, as the characteristic function of the subset. And types are added as easily - we specify each variable, each object, to have a set it belongs to.

This way, predicates really are subsets. Type annotations decide which set the predicate lives in. And we have everything set up in a way that opens up for the topos language above.

We'd define, for predicates P,Q acting on the same type:

$\{x\in A : \top\} = A$
$\{x\in A : \bot\} = \emptyset$
$\{x : (P \wedge Q)(x)\} = \{x : P(x)\} \cap \{x : Q(x)\}$
$\{x : (P \vee Q)(x)\} = \{x : P(x)\} \cup \{x : Q(x)\}$
$\{x\in A : (\neg P)(x) \} = A \setminus \{x\in A : P(x)\}$

We could then start to define primitive logic connectives as set operations; the intersection of two sets is the set on which both the corresponding predicates hold true, so $\wedge = \cap$. Similarily, the union of two sets is the set on which either of the corresponding predicates holds true, so $\vee = \cup$. The complement of a set, in the universe, is the negation of the predicate, and all other propositional connectives (implication, equivalence, ...) can be built with conjunction (and), disjunction (or) and negation (not).

So we can mimic all these in a given topos:

We say that a universe U is just an object in a given topos. (Note that by admitting several universes, we arrive at a typed predicate logic, with basically no extra work.)

A predicate is a subobject of the universe.

We can now proceed to define all the familiar logic connectives one by one, using the topos setting. While doing this, we shall introduce the notation $t_A: A\to\Omega$ for the morphism $t_A = A\to 1\to^{true}\Omega$ that takes on the value true on all of A. We note that with this convention, $\chi_{A_0}$, the characteristic morphism of a subobject, is the arrow such that $\chi_{A_0}\circ i = t_{A_0}$.

Conjunction: Given predicates P,Q, we need to define the conjunction $P\wedge Q$ as some $P\wedge Q: U\to\Omega$ that corresponds to both P and Q simultaneously.

We may define $true\times true: 1\to\Omega\times\Omega$, a subobject of $\Omega\times\Omega$. Being a subobject, this has a characteristic arrow $\wedge:\Omega\times\Omega\to\Omega$, that we call the conjunction arrow.

Now, we may define $\chi_P\times\chi_Q:U\to\Omega\times\Omega$ for subobjects $P,Q\subseteq U$ - and we take their composition $\wedge\circ\chi_P\times\chi_Q$ to be the characteristic arrow of the subobject $P\wedge Q$.

And, indeed, this results in a topoidal version of intersection of subobjects.

Implication: Next we define $\leq_1: \Omega_1\to\Omega\times\Omega$ to be the equalizer of $\wedge$ and proj1. Given $v, w: U\to\Omega$, we write $v\leq_1 w$ if $v\times w$ factors through $\leq_1$.

Using the definition of an equalizer we arrive at $v\leq_1 w$ iff $v = v\wedge w$. From this, we can deduce

$u\leq_1 true$
$u\leq_1 u$
If $u\leq_1 v$ and $v\leq_1 w$ then $u\leq_1 w$.
If $u\leq_1 v$ and $v\leq_1 u$ then u = v

and thus, $\leq_1$ is a partial order on $[U\to\Omega]$. Intuitively, $u\leq_1 v$ if v is at least as true as u.

This relation corresponds to inclusion on subobjects. Note that $\leq_1:\Omega_1\to\Omega\times\Omega$, given from the equalizer, gives us Ω1 as a relation on Ω - a subobject of $\Omega\times\Omega$. Specifically, it has a classifying arrow $\Rightarrow:\Omega\times\Omega\to\Omega$. We write $h\Rightarrow k = (\Rightarrow)\circ h\times k$. And for subobjects $P,Q\subseteq A$, we write $P\Rightarrow Q$ for the subobject classified by $\chi_P\Rightarrow\chi_Q$.

It turns out, without much work, that this $P\Rightarrow Q$ behaves just like classical implication in its relationship to $\wedge$.

Membership: We can internalize the notion of membership as a subobject $\in^U\subseteq U\times\Omega^U$, and thus get the membership relation from a pullback:

For elements $x\times h: 1\to U\times\Omega^U$, we write $x\in^U h$ for $x\times h\in\in^U$. Yielding a subset of the product $U\times\Omega^U$, this is readily interpretable as a relation relating things in U with subsets of U, so that for any x,h we can answer whether $x\in^Uh$. Both notations indicate $ev_A\circ h\times x = true$.

Universal quantification: For any object U, the maximal subobject of U is U itself, embedded with 1U into itself. There is an arrow $\tau_U:1\to\Omega^U$ represents this subobject. Being a map from 1, it is specifically monic, so it has a classifying arrow $\forall_U:\Omega^U\to\Omega$ that takes a given subobject of U to true precisely if it is in fact the maximal subobject.

Now, with a relation $r:R\to B\times A$, we define $\forall a. R$ by the following pullback:

where λχR comes from the universal property of the exponential.

Theorem For any $s:S\to B$ monic, $S\subseteq \forall a.R$ iff $S\times A\subseteq R$.

This theorem tells us that the subobject given by $\forall a.R$ is the largest subobject of B that is related by R to all of A.

Falsum: We can define the false truth value using these tools as $\forall w\in\Omega.w$. This might be familiar to the more advanced Haskell type hackers - as the type

`x :: forall a. a`
which has to be able to give us an element of any type, regardless of the type itself. And in Haskell, the only element that inhabits all types is
undefined
.

From a logical perspective, we use a few basic inference rules:

and connect them up to derive

for any φ not involving w - and we can always adjust any φ to avoid w.

Thus, the formula $\forall w.w$ has the property that it implies everything - and thus is a good candidate for the false truth value; since the inference

is the defining introduction rule for false.

Negation: We define negation the same way as in classical logic: $\neg \phi = \phi \Rightarrow false$.

Disjunction: We can define

$P\vee Q = \forall w. ((\phi\Rightarrow w)\wedge(\psi\Rightarrow w))\Rightarrow w$

Note that this definition uses one of our primary inference rules:

as the defining property for the disjunction, and we may derive any properties we like from these.

Existential quantifier: Finally, the existential quantifier is derived similarly to the disjunction - by figuring out a rule we want it to obey, and using that as a definition for it:

$\exists x.\phi = \forall w. (\forall x. \phi \Rightarrow w)\Rightarrow w$

Here, the rule we use as defining property is

Before we leave this exploration of logic, some properties worth knowing about: While we can prove $\neg(\phi\wedge\neg\phi)$ and $\phi\Rightarrow\neg\neg\phi$, we cannot, in just topos logic, prove things like

$\neg(\phi\wedge\psi)\Rightarrow(\neg\phi\vee\neg\psi)$
$\neg\neg\phi\Rightarrow\phi$

nor any statements like

$\neg(\forall x.\neg\phi)\Rightarrow(\exists x.\phi)$
$\neg(\forall x.\phi)\Rightarrow(\exists x.\neg\phi)$
$\neg(\exists x.\neg\phi)\Rightarrow(\forall x.\phi)$

We can, though, prove

$\neg(\exists x.\phi)\Rightarrow(\forall x.\neg\phi)$

If we include, extra, an additional inference rule (called the Boolean negation rule) given by

then suddenly we're back in classical logic, and can prove $\neg\neg\phi\Rightarrow\phi$ and $\phi\or\neg\phi$.

#### 3.3 Examples: Sheaves, topology and time sheaves

The first interesting example of a topos is the category of (small enough) sets; in some sense clear already since we've been modelling our axioms and workflows pretty closely on the theory of sets.

Generating logic and set theory in the topos of sets, we get a theory that captures several properties of intuitionistic logic; such as the lack of Boolean negation, of exclusion of the third, and of double negation rules.

For the more interesting examples, however, we shall introduce the concepts of topology and of sheaf:

Definition A (set-valued) presheaf on a category C is a contravariant functor $E: C^{op}\to Set$.

Presheaves occur all over the place in geometry and topology - and occasionally in computer science too: There is a construction in which a functor $A\to Set$ for a discrete small category A identified with its underlying set of objects as a set, corresponds to the data type of bags of elements from A - for $a\in A$, the image F(a) denotes the multiplicity of a in the bag.

Theorem The category of all presheaves (with natural transformations as the morphisms) on a category C form a topos.

Example Pick a category on the shape

A contravariant functor on this category is given by a pair of sets G0,G1 and a pair of function $source, target: G_1\to G_0$. Identities are sent to identities.

The category of presheaves on this category, thus, is the category of graphs. Thus graphs form a topos.

The subobject classifier in the category of graphs is a graph with two nodes: in and out, and five arrows:

$in \to^{all} in$
$in \to^{both} in$
$in \to^{source} out$
$out \to^{target} in$
$out \to^{neither} out$

Now, given a subgraph $H \leq G$, we define a function $\chi_H:G\to\Omega$ by sending nodes to in or out dependent on their membership. For an arrow a, we send it to all if the arrow is in H, and otherwise we send it to both/source/target/neither according to where its source and target reside.

To really get into sheaves, though, we introduce more structure - specifically, we define what we mean by a topology:

Definition Suppose P is a partially ordered set. We call P a complete Heyting algebra if

• There is a top element 1 such that $x\leq 1 \forall x\in P$.
• Any two elements x,y have an infimum (greatest lower bound) $x\wedge y$.
• Every subset $Q\subseteq P$ has a supremum (least upper bound) $\bigvee_{p\in P} p$.
• $x\wedge(\bigvee y_i) = \bigvee x\wedge y_i$

Note that for the partial order by inclusion of a family of subsets of a given set, being a complete Heyting algebra is the same as being a topology in the classical sense - you can take finite unions and any intersections of open sets and still get an open set.

If {xi} is a subset with supremum x, and E is a presheaf, we get functions $e_i:E(x)\to E(x_i)$ from functoriality. We can summarize all these ei into $e = \prod_i e_i: E(x)\to\prod_i E(x_i)$.

Furthermore, functoriality gives us families of functions $c_{ij}: E(x_i)\to E(x_i\wedge x_j)$ and $d_{ij}: E(x_j)\to E(x_i\wedge x_j)$. These can be collected into $c: \prod_i E(x_i)\to\prod_{ij}E(x_i\wedge x_j)$ and $d:\prod_j E(x_j)\to\prod_{ij}E(x_i\wedge x_j)$.

Definition A presheaf E on a Heyting algebra is called a sheaf if it satisfies:

$x = \bigvee x_i$

implies that

is an equalizer. If you have seen sheaves before, you may recognize this as the covering axiom.

In other words, E is a sheaf if whenever $x=\bigvee x_i$ and c(α) = d(α), then there is some $\bar\alpha$ such that $\alpha = e(\bar\alpha)$.

Theorem The category of sheaves on a Heyting algebra is a topos.

For context, we can think of sheaves over Heyting algebras as sets in a logic with an expanded notion of truth. Our Heyting algebra is the collection of truth values, and the sheaves are the fuzzy sets with fuzziness introduced by the Heyting algebra.

Recalling that subsets and predicates are viewed as the same thing, we can view the set E(p) as the part of the fuzzy set E that is at least p true.

As it turns out, to really make sense of this approach, we realize that equality is a predicate as well - and thus can hold or not depending on the truth value we use.

Definition Let P be a complete Heyting algebra. A P-valued set is a pair (S,σ) of a set S and a function $\sigma: S\to P$. A category of fuzzy sets is a category of P-valued sets. A morphism $f:(S,\sigma)\to(T,\tau)$ of P-valued sets is a function $f:S\to T$ such that $\tau\circ f = \sigma$.

From these definitions emerges a fuzzy set theory where all components of it being a kind of set theory emerges from the topoidal approach above. Thus, say, subsets in a fuzzy sense are just monics, thus are injective on the set part, and such that the valuation, on the image of the injection, increases from the previous valuation: $(T,\tau)\subseteq(S,\sigma)$ if $T\subseteq S$ and σ | T = τ.

To get to topoi, though, there are a few matters we need to consider. First, we may well have several versions of the empty set - either a bona fide empty set, or just a set where every element is never actually there. This issue is minor. Much more significant though, is that while we can easily make (S,σ) give rise to a presheaf, by defining

$E(x) = \{s\in S: \sigma(s)\geq x\}$

this definition will not yield a sheaf. The reason for this boils down to $E(0) = S \neq 1$. We can fix this, though, by adjoining another element - $\bot$ - to P giving P + . The new element $\bot$ is imbued with two properties: it is smaller, in P + , than any other element, and it is mapped, by E to 1.

Theorem The construction above gives a fuzzy set (S,σ) the structure of a sheaf on the augmented Heyting algebra.

Corollary The category of fuzzy sets for a Heyting algebra P forms a topos.

Final note While this construction allows us to make membership a fuzzy concept, we're not really done fuzzy-izing sets. There are two fundamental predicates on sets: equality and membership. While fuzzy set theory, classically, only allows us to make one of these fuzzy, topos theory allows us - rather easily - to make both these predicates fuzzy. Not only that, but membership reduces - with the power object construction - to equality testing, by which the fuzzy set theory ends up somewhat inconsistent in its treatment of the predicates.

### 4 Literature

At this point, I would warmly recommend the interested reader to pick up one, or more, of:

• Steve Awodey: Category Theory
• Michael Barr & Charles Wells: Categories for Computing Science
• Colin McLarty: Elementary Categories, Elementary Toposes

or for more chewy books

• Peter T. Johnstone: Sketches of an Elephant: a Topos Theory compendium
• Michael Barr & Charles Wells: Toposes, Triples and Theories

### 5 Exercises

No homework at this point. However, if you want something to think about, a few questions and exercises:

1. Prove the relations showing that $\leq_1$ is indeed a partial order on $[U\to\Omega]$.
2. Prove the universal quantifier theorem.
3. The extension of a formula φ over a list of variables x is the sub-object of the product of domains $A_1\times\dots\times A_n$ for the variables $x_1,\dots,x_n=x$ classified by the interpretation of φ as a morphism $A_1\times\dots\times A_n\to\Omega$. A formula is true if it classifies the entire product. A sequent, written Γ:φ is the statement that using the set of formulae Γ we may prove φ, or in other words that the intersection of the extensions of the formulae in Γ is contained in the extension of φ. If a sequent Γ:φ is true, we say that Γ entails φ. (some of the questions below are almost embarrassingly immediate from the definitions given above. I include them anyway, so that a catalogue of sorts of topoidal logic inferences is included here)
1. Prove the following entailments:
1. Trivial sequent: φ:φ
2. True: :true (note that true classifies the entire object)
3. False: false:φ (note that false classifies the global minimum in thepreorder of subobjects)
2. Prove the following inference rules:
1. Implication: Γ,φ:ψ is equivalent to $\Gamma:\phi\Rightarrow\psi$.
2. Thinning: Γ:φ implies Γ,ψ:φ
3. Cut: Γ,ψ:φ and Γ:ψ imply Γ:φ if every variable free in ψ is free in Γ or in φ.
4. Negation: Γ,φ:false is equivalent (implications both ways) to $\Gamma: \neg\phi$.
5. Conjunction: Γ:φ and Γ:ψ together are equivalent to $\Gamma:\phi\wedge\psi$.
6. Disjunction: Γ,φ:θ and Γ,ψ:θ together imply $\Gamma, \phi\vee\psi: \theta$.
7. Universal: Γ:φ is equivalent to $\Gamma:\forall x.\phi$ if x is not free in Γ.
8. Existential: Γ,φ:ψ is equivalent to $\Gamma,\exists x.\phi:\psi$ if x is not free in Γ or ψ.
9. Equality: :q = q.
10. Biconditional: $(v\Rightarrow w)\wedge(w\Rightarrow v):v=w$. We usually write $v\Leftrightarrow w$ for v = w if $v,w:A\to\Omega$.
11. Product: p1u = p1u',p2u = p2u':u = u' for $u,u'\in A\times B$.
12. Product revisited: $:(p_1(s\times s')=s)\wedge(p_2(s\times s')=s')$.
13. Extensionality: $\forall x\in A. f(x) = g(x) : f = g$ for $f,g\in[A\to B]$.
14. Comprehension: $(\lambda x\in A. s)x = s$ for $x\in A$.
3. Prove the following results from the above entailments and inferences -- or directly from the topoidal logic mindset:
1. $:\neg(\phi\wedge\neg\phi)$.
2. $:\phi\Rightarrow\neg\neg\phi$.
3. $:\neg(\phi\vee\psi)\Rightarrow(\neg\phi\wedge\neg\psi)$.
4. $:(\neg\phi\wedge\neg\psi)\Rightarrow\neg(\phi\wedge\psi)$.
5. $:(\neg\phi\vee\neg\psi)\Rightarrow\neg(\phi\vee\psi)$.
6. $\phi\wedge(\theta\vee\psi)$ is equivalent to $(\phi\wedge\theta)\vee(\phi\wedge\psi)$.
7. $\forall x.\neg\phi$ is equivalent to $\neg\exists x.\phi$.
8. $\exists x\phi\Rightarrow\neg\forall x.\neg\phi$.
9. $\exists x\neg\phi\Rightarrow\neg\forall x.\phi$.
10. $\forall x\phi\Rightarrow\neg\exists x.\neg\phi$.
11. φ:ψ implies $\neg\psi:\neg\phi$.
12. $\phi:\psi\Rightarrow\phi$.
13. $\phi\Rightarrow\not\phi:\not\phi$.
14. $\not\phi\vee\psi:\phi\Rightarrow\psi$ (but not the converse!).
15. $\neg\neg\neg\phi$ is equivalent to $\neg\phi$.
16. $(\phi\wedge\psi)\Rightarrow\theta$ is equivalent to $\phi\Rightarrow(\psi\Rightarrow\theta)$ (currying!).
4. Using the Boolean negation rule: $\Gamma,\neg\phi:false$ is equivalent to Γ:φ, prove the following additional results:
1. $\neg\neg\phi:\phi$.
2. $:\phi\vee\neg\phi$.
5. Show that either of the three rules above, together with the original negation rule, implies the Boolean negation rule.
1. The converses of the three existential/universal/negation implications above.
6. The restrictions introduced for the cut rule above block the deduction of an entailment $:\forall x.\phi\Rightarrow\exists x.\phi$. The issue at hand is that A might not actually have members; so choosing one is not a sound move. Show that this entailment can be deduced from the premise $\exists x\in A. x=x$.
7. Show that if we extend our ruleset by the quantifier negation rule $\forall x\Leftrightarrow \neg\exists x.\neg$, then we can derive the entailment $:\forall w: w=t \vee w = false$. From this derive $:\phi\vee\neg\phi$ and hence conclude that this extension gets us Boolean logic again.
4. A topology on a topos E is an arrow $j:\Omega\to\Omega$ such that $j\circ true=true$, $j\circ j=j<math> and <math>j\circ\wedge = \wedge\circ j\times j$. For a subobject $S\subseteq A$ with characteristic arrow $\chi_S:A\to\Omega$, we define its j-closure as the subobject $\bar S\subseteq A$ classified by $j\circ\chi_S$.
1. Prove:
1. $S\subseteq\bar S$.
2. $\bar S = \bar{\bar S}$.
3. $\bar{S\cap T} = \bar S\cap\bar T$.
4. $S\subseteq T$ implies $\bar S\subseteq\bar T$.
5. $\bar{f^{-1}(S)} = f^{-1}(\bar S)$.
2. We define S to be j-closed if $S=\bar S$. It is j-dense if $\bar S=A$. These terms are chosen due to correspondences to classical pointset topology for the topos of sheaves over some space. For a logical standpoint, it is more helpful to look at j as a modality operator: "it is j-locally true that" Given any $u:1\to\Omega$, prove that the following are topologies:
1. $(u\to -): \Omega\to\Omega$ (the open topology, where such a u in a sheaf topos ends up corresponding to an open subset of the underlying space, and the formulae picked out are true on at least all of that subset).
2. $u\vee -): \Omega\to\Omega$ (the closed topology, where a formula is true if its disjunction with u is true -- corresponding to formulae holding over at least the closed set complementing the subset picked out)
3. $\neg\neg: \Omega\to\Omega$. This may, depending on the topos, end up being interpreted as true so far as global elements are concerned, or not false on any open set, or other interpretations.
4. 1Ω.
3. For a topos E with a topology j, we define an object A to be a sheaf iff for every X and every j-dense subobject $S\subseteq X$ and every $f:S\to A$ there is a unique $g:X\to A$ with $f=g\circ s$. In other words, A is an object that cannot see the difference between j-dense subobjects and objects. We write Ej for the full subcategory of j-sheaves.
1. Prove that any object is a sheaf for 1Ω.
2. Prove that a subobject is dense for $\neg\neg$ iff its negation is empty. Show that $true+false:1+1\to\Omega$ is dense for this topology. Conclude that 1 + 1 is dense in $\Omega_{\neg\neg}$ and thus that $E_{\neg\neg}$ is Boolean.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 199, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.8057393431663513, "perplexity_flag": "middle"}