[mkckto]

Here's a write-up I did on deriving the Y combinator from Lawvere's fixed-point theorem: https://emarzion.github.io/Y-Comb/