“A subway is just a hole in the ground, and that hole is a maze.”
“The map is the last vestige of the old system. If you can’t read the map, you can’t use the subway.”
Eddie Jabbour in Can he get there from here? (NYT)
Sometimes, lines between adjacent stations can be uni-directional (as in the Paris Metro map below in the right upper corner, 7bis). So, it is best to view a subway map as a directed graph, with vertices the different stations, and directed arrows when there’s a service connecting two adjacent stations.

Aha! But, directed graphs form a presheaf topos. So, each and every every subway in the world comes with its own logic, its own bi-Heyting algebra!
Come again…?
Let’s say Wally (or Waldo, or Charlie) is somewhere in the Paris metro, and we want to find him. One can make statements like:
Each sentence pinpoints Wally’s location to some directed subgraph of the full Paris metro digraph, let’s call this subgraph the ‘scope’ of the sentence.
We can connect such sentences with logical connectives
The scope of
The scope of
The scope of the negation
For example, the scope of
In the Paris metro logic the law of double negation does not hold.

So, although the scope of
The logical operations
Perhaps we were too drastic in removing all “problematic edges” from the scope of
We might have kept all problematic edges, and added the missing source and/or target stations to get the scope of another negation of
Whereas the scope of
The scope of
In general
The logical operations
There’s plenty more to say about all of this (and I may come back to it later). For the impatient, there’s the paper by Reyes and Zolfaghari: Bi-Heyting Algebras, Toposes and Modalities.
Right now, I’m more into exploring whether this setting can be used to revive an old project of mine: Heyting Smullyanesque problems (btw. the algebra in that post is not Heyting, oops!).