I've been struggling with the proof of Lawvere's fixed point theorem. It doesn't type-check because it's missing a unitor or a diagonal somewhere. In three sources: original paper, nLab, and Qiaochu Yuan's blog post, one side of an equation takes two units, the other one unit.
-
Here g : X -> Y, but the left side takes 1 x X (because x : 1 -> X). It needs the inverse left unitor to type check.pic.twitter.com/HrqPGNbQHV
you're right, i omitted the unitor. it would never have occurred to me to make unitors explicit in a cartesian category honestly
-
-
I'm trying to explain it to programmers, so it must type check. So does the definition of (weak) pointwise surjections require unitors? I'm trying to figure out where the best place to insert them is.
-
You don’t need unitors for the definition of point-surjective; in fact, point-surjective as a concept makes sense in a bare category with no extra structure.
- 4 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.