Anonymous Constructor Notation, AmIRight???

I wrote a proof to say the range of f under A intersect B subsets the range of f under A intersect the range of f under B. That makes sense, A intersect B subsets A and A intersect B subsets B, so why would a mapping change anything?

But man proofs are weird! Let’s look at this guys!

What in God’s green earth! Line by line we go:

Line 1) the claim i.e. “the range of f under A intersect B subsets the range of f under A intersect the range of f under B

Line 2) the first assumption. Implicit is the claim is the question what? The answer is “for everything!”. So we assume a trivial (nothin special object) to make the claim. Very good.

Line 3) the second assumption Y is in the range of f under A intersect B. Why assume it? Because anytime you prove a set subsets another, you just need to prove an arbitrary object does it. Not bad.

Line 4) what we need. That y is in the intersection of. the image of f under A and the image of f under B. Again, this is the general structure for any subset proof.

Line 4.5 and 5) This is where it gets juicey! Exists.elim?? What exists statement are we eliminating? I’m so confuded? Dan you lied, you have introduced an exists statement anywhere! Oh, joke’s on you. Implicit in line 4 is the fact “there exists a y s.t. it’s in the set”. Boom roasted! Anyway… on line 5 we introduce another arbitrary object a, which could be any atomic element of A or B? Why? Keep reading?

Line 6) Exists.elim don’t really “eliminate” so much as “use” and they use the exists statements by coupling them with a strong rule. The rule states that anything that matches the object in the exists follows a certain rule. Or, for all a who satisfy this thing something here goes nothing.. (coming back to it)

Line 7) Zooming out, my human brain makes sense. a exists, a in A, and f a = y, so how the hell could y not be in f ” A? The kicker here is what does it mean to be in the image of f under A? That gets into this whole convoulted thing … blah blah blah nobody cares you have to prove it with an exists.intro statement. And lean is like screw that! This is obvious! Here come my delightful curvy brackets to the rescue!

Line 8) similar

Line 9) hey! Isn’t this fun. An intersection is just like (you, guessed it) a conjunctive statement. So and.intro functions the same here. we combine the two points, get our resolution and go happily on our way, never wondering about images under functions again.


Theorem proving is a great exercise of the mind. It requires skill, determination, focus, and mentorship.

I’ve enjoyed my experience working thorough the content and it’s been important to realize what I don’t know. There’s a huge piece of evidence there.

For instance, I wanted to prove x = y after already having the statement 2x=2y. It’s one of those things that feels obvious on the surface but the intricacies of what’s going on is fascinating.

Investing in the Python Paradox

In 2004 Paul Graham coined the Python Paradox. The paradox, in its most generic form, states that if a company chooses an obscure tech stack, it will have better hiring outcomes, and conversely, if it chooses a well known tech stack, it will have worse outcomes.

This result is surprising on the surface. Normally hiring is analogous to sales: fill the funnel, move down it with phone calls, in person meetings and networking, and at the bottom of it there’s a transaction, in this case a job offer. 

As such, if a company has a more common tech stack then the top of the funnel should be bigger. If the top of funnel is bigger and the bottom stays the same, those that make it through should be higher quality. This is a linear relationship.

Unfortunately for our hiring model, the technology industry is predicated on exponential relationships, not linear.  People have called it a lot of things (10x Programmer, Power Law, 80/20) but a few inputs determine a lot of output. 

The python paradox is a specification of that generality where a few inputs (candidates) determine a lot of the output (developer productivity). Similarly, it isn’t shocking to notice that the venture industry operates the same way where a few inputs (portfolio companies) determine a lot of the output (return on investment). However, what is unusual is that there is no equivalent paradox for venture.


I believe the Python Paradox is real for venture and has its own analogous form: if a startup chooses an obscure tech stack, there’s a higher chance they’ll have a differentiated value proposition, and conversely, if it chooses a well known tech stack, it will have a less differentiated value proposition.

Now, obscure tech is not inherently a good thing to invest in (or hire for). I’m not saying invest in every new cryptocurrency, hire anyone who has made their own LISP dialect and disregard anyone who uses PHP.

I am saying follow the trends and be logical. Rust and TypeScript are soaring in popularity. Functional programming is discussed daily on HackerNews. Startups that use Haskell, Clojure or Scala might be more likely to solve modern distributed systems issues in a scalable way … and companies that are building another marketing automation platform can probably get away with Java …


In the coming months, I want to do a deep dive into commercial applications of programming languages, type theory, category theory and functional programming to show how young companies can leverage these tools. I believe in and enjoy working with programming languages and I think they’re the next heuristic for startups.

Also –

People think productivity is caused by time management. It is not. It is caused by attention management. Attention management is decreasing the number of unique tasks per unit time.