A notable consequence of the approach taken by Synthetic Agda to embedding the internal languages of various topoi is that it equips the type theory of Synthetic Agda with a particularly elegant form of internal parametricity, which makes it additionally an ideal framework for studying type-theoretic constructions that rely on such parametricity, such as impredicative encodings of (higher) inductive types, etc.
@jonmsterling @jcreed @carloangiuli @buchholtz @boarders @danielgratzer @ecavallo @andrejbauer @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz
=> More informations about this toot | View the thread | More toots from cbaberle@mathstodon.xyz
=> View jonmsterling@mathstodon.xyz profile | View jcreed@mastodon.social profile | View carloangiuli@mathstodon.xyz profile | View buchholtz@mathstodon.xyz profile | View boarders@mathstodon.xyz profile | View danielgratzer@mathstodon.xyz profile | View ecavallo@mathstodon.xyz profile | View andrejbauer@mathstodon.xyz profile | View anuytstt@fosstodon.org profile | View totbwf@types.pl profile | View amy@types.pl profile | View ncf@types.pl profile | View jesper@agda.club profile | View chrisamaphone@hci.social profile | View MartinEscardo@mathstodon.xyz profile | View jonasfrey@mathstodon.xyz profile | View DavidJaz@mathstodon.xyz profile
text/geminiThis content has been proxied by September (ba2dc).