Post #1846817
2026-04-27 22:16 UTC
@jonmsterling What do you mean by a “combinatorial presentation of the type theory”? @MartinEscardo @carloangiuli
Replies (2)
-
@jonmsterling@mathstodon.xyz 2026-04-27 22:31
@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.
-
@dgb37@mathstodon.xyz 2026-04-28 15:20
@jeanas This is one of Ambrus' long-term problems of interest. He even has a potential solution technique which is yet to be fully tested (the process may not terminate). @jonmsterling @MartinEscardo @carloangiuli