Type theory and category theory are the product of highly refined abstractions. Since every level of abstraction strips a layer of intuition, the final product is sometimes called abstract nonsense. The only way to navigate such vast halls of abstraction is to keep in mind where those abstractions come from, or how they can be modeled in more familiar surroundings, be it computer programs, logic, or set theory. When studying an elephant, it makes sense to occasionally focus on its trunk, legs, or ears,

Learning category theory is a little like reading a novel that has many hidden layers of meaning.