Post #1846818

@jeanas @MartinEscardo @carloangiuli I mean just what I said: some hypothetical presentation of type theory in combinators, analogous to the SKI calculus or similar things.