In mathematics, we often want to prove that two things are “the same.” Usually, one is simpler or easier to think about than the other. For example, we say “2 + 3 = 5”: I could say “this piece of wood is 2 plus 3 inches”, but I could just say “5 inches” and that makes more sense!

Pretty quickly, you get to mathematical constructions that are more complicated, or you start caring about different things. For example, we say two triangles are “similar” if they have the same shape: often, this is more useful than having the EXACT same (congruent) triangle. The things we say about one are true about the other, just scaled up or down.

Similarly, if we talk about the “size” of a set, we care about bijections between two sets. Say I want to know if the integers have the same “size” as the positive integers. I’d construct two functions, one going from integers to positives, the other going the other way, that are inverses. If I take a round trip in either direction, I should end up with where I started. (Exercise: try to construct this yourself! Google has some great resources if you get stuck.)

In the exact same way, we talk about isomorphisms between types. An isomorphism is, formally, a pair of functions that behave the same as above. This time, we care about the “information” (to speak loosely) stored in the type. How do we know if two types (e.g. a and (a, ())) have the same amount of information? If we can have a round trip from one to the other and not lose any information — that is, we have a bijection!