This is definitely an interesting musing and comparison. I feel like its relevance to programmers could use some explanation or context, but I don’t know what knowledge to presume in giving that… Unfortunately true for a lot of type-theory topics, since they affect computing profoundly but have been developed mostly by mathematicians.