[fmap]

I think it's a nice analogy. It's a bit tongue in cheek, but it does give you the right idea when you compare it to programming languages.

Set theory is a reductionistic system. It's supposed to give a foundation which is as "small" as possible. In set theory you start with almost nothing and you have to encode all useful concepts into sets before you can start proving/programming.

Compare this to Turing machines, where you start with a very primitive model of computation. The first step in most treatments of Turing machines is similar to set theory, you show that some useful concepts (associative memory, high-level control flow, etc.) can be encoded into Turing machines. You then use this encoding to construct arbitrary programs.

Type theory starts out with a functional programming language and you derive new concepts from free constructions. In type theory you shouldn't be encoding things at all. You should be describing concepts (~adding an API) and possibly extending your model (~the compiler).

As analogies go, I'd say that this one is pretty accurate.