§ Topology is really about computation --- part 2

Here, we're going to describe whatever I've picked up of sheaves in the past couple of weeks. I'm trying to understand the relationship between sheaves, topoi, geometry, and logic. I currently see how topoi allows us to model logic, and how sheaves allow us to model geometry, but I see nothing about the relationship! I'm hoping that writing this down will allow me to gain some perspective on this.

§ What is a sheaf?

Let's consider two sets $P, A$, $P \subseteq A$. Now, given a function $f: A \rightarrow X$, we can restrict this function to $A_P: P \rightarrow X$. So, we get to invert the direction :

$$(P \subseteq A) \iff (f: A \rightarrow X) \rightarrow (f_P: P \rightarrow X)$$

We should now try to discover some sort of structure to this "reversal" business. Perhaps we will discover a contravariant functor! (Spoiler: we will).