4 ms·
> if there is a function p : A -> (A -> B) that has a left-inverse, i.e., e : (A -> B) -> A with p o e = id_(A -> B) then B has a fixed point combinator I thin
by 3PS 4y ago
> if there is a function p : A -> (A -> B) that has a left-inverse, i.e., e : (A -> B) -> A with p o e = id_(A -> B) then B has a fixed point combinator
I think you meant to write "right inverse" here.
Agreed that Lawvere's theorem is very cool. It helps that Cartesian closed categories are basically just categories where you can do typed lambda calculus, so the underlying link is already very close.