§ 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,AP, A, PAP \subseteq A. Now, given a function f:AXf: A \rightarrow X, we can restrict this function to AP:PX A_P: P \rightarrow X . So, we get to invert the direction :
(PA)    (f:AX)(fP:PX) (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).