It's all connected

Reading about dependent types led me to intuitionistic type theory, which led me to Heyting algebras, which led to point-free topology, which brought me back to higher-order functional programming.

I suppose it shouldn't be surprising that in a dependently typed world, the metatheory of a system starts looking a lot like the system itself, but it's still spooky. It's like seeing a series of small, incomplete glimpses of a colossal beast, and then one of those glimpses suddenly reveals that the monster is curling back and devouring itself. I assume there's a deeper intuition behind these connections, which I'm not quite grokking yet.