Ancestors

Written by C.B. Aberlé on 2024-12-31 at 18:10

Let’s end this year with a bang! I’m very pleased to announce something that’s been a long time in the works, but that I think is finally in a fit state to give a soft launch – Synthetic Agda: https://hyrax.cbaberle.com/Hyrax/Prelude/synthetic-agda.lagda

(Tagging people who I think might be interested: @jonmsterling @jcreed @carloangiuli @buchholtz @boarders @danielgratzer @ecavallo @andrejbauer @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz )

=> More informations about this toot | More toots from cbaberle@mathstodon.xyz

Written by C.B. Aberlé on 2024-12-31 at 18:11

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 | More toots from cbaberle@mathstodon.xyz

Written by C.B. Aberlé on 2024-12-31 at 18:12

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 | More toots from cbaberle@mathstodon.xyz

Toot

Written by C.B. Aberlé on 2024-12-31 at 18:12

It’s still early days for Synthetic Agda, but I’m excited about its potential to be used as a digital blackboard for synthetic mathematics! As such, I am also pleased to announce The Hyrax Project, an Agda library/personal wiki/digital garden focusing on synthetic mathematics, using Synthetic Agda: https://hyrax.cbaberle.com/Hyrax/index.lagda

@jonmsterling @jcreed @carloangiuli @buchholtz @boarders @danielgratzer @ecavallo @andrejbauer @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz

=> More informations about this toot | More toots from cbaberle@mathstodon.xyz

Descendants

Written by C.B. Aberlé on 2024-12-31 at 18:13

Some potential applications of Synthetic Agda I’m interested in exploring in the near future are:

• Embedding some/all of Simplicial Type Theory / Triangulated Type Theory for the synthetic study of higher categories,

• Studying Kolomatskaia-Shulman-type encodings of semisimplicial types and other higher structures in Simplicial Agda using the latter’s form of internal parametricity,

• Using Synthetic Agda to synthetically derive novel parametricity theorems for exotic type systems such as linear/substructural type theory, etc.

@jonmsterling @jcreed @carloangiuli @buchholtz @boarders @danielgratzer @ecavallo @andrejbauer @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz

=> More informations about this toot | More toots from cbaberle@mathstodon.xyz

Written by chris martens on 2025-01-01 at 15:22

@cbaberle thanks for tagging me here! i’m motivated to understand this, so i’m starting to dig into your blog and references therefrom. it will take me some time to get up to speed. are you ok with me asking you some (potentially naive) questions along the way?

=> More informations about this toot | More toots from chrisamaphone@hci.social

Written by C.B. Aberlé on 2025-01-01 at 20:53

@chrisamaphone thanks!! and yes, of course, feel free to run any questions you have by me :)

=> More informations about this toot | More toots from cbaberle@mathstodon.xyz