Synthetic Agda aims to be a type-theoretic playground for experimenting with advanced forms of synthetic mathematics. For this purpose, it extends Agda with various constructs that allow it to be customized to reflect the internal language of any Grothendieck topos/∞-topos. Perhaps surprisingly, this can all be done using some of Agda’s modal features along with postulates and rewrite rules. Hence Synthetic Agda can be (and has been) implemented as an Agda module, such that making use of its features requires merely importing it.
@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).