@ncf @jonmsterling What do you mean by "type-theoretic syntax"? I think you just need to annotate sequents by their free variables right?
=> More informations about this toot | View the thread | More toots from tito@sciences.re
=> View ncf@types.pl profile | View jonmsterling@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).