@ncf @jonmsterling I was looking for some notes like this recently and couldn't really find any. I wanted a reference for the deduction rules when the free variables have their types explicitly declared in the context. The best I could find were the notes on categorical logic by Mike Shulman and by Steve Awodey and @andrejbauer.
=> More informations about this toot | View the thread | More toots from OscarCunningham@mathstodon.xyz
=> View ncf@types.pl profile | View jonmsterling@mathstodon.xyz profile | View andrejbauer@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).