Ancestors

Toot

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

Descendants

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

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

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

Written by Andrej Bauer on 2025-01-01 at 10:38

@cbaberle @jonmsterling @jcreed @carloangiuli @buchholtz @boarders @danielgratzer @ecavallo @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz (That's a long list of mentions...)

This looks very nice. It's a topic that I care about, and whenever I contemplated it, I thought I'd end up inventing Isabelle or some such, but with dependently-typed metatheory. These thoughts lead to Andromeda, which was not executed well, unfortunately.

Also, it seems like there is a significant difference in terms of engineering between having a system that can reason about synthetic worlds, and having a system in which users can formulate their own synthetic worlds and use them, If anyone knows how to combine these two, we have a winner.

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

Written by Chuck Darwin on 2025-01-01 at 16:48

@cbaberle

https://c.im/@cdarwin/113754017879640245

=> More informations about this toot | More toots from cdarwin@c.im

Written by Ulrik Buchholtz on 2025-01-01 at 23:01

@cbaberle @jonmsterling @jcreed @carloangiuli @boarders @danielgratzer @ecavallo @andrejbauer @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz Thanks, this looks very promising. Could you say a bit more about how the interleaved STele… definitions and Sort… postulates work, and the intended model thereof? And Happy New Year!

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

Written by C.B. Aberlé on 2025-01-01 at 23:39

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

Happy new year! Thank you so much for your kind words!

To answer your question, STele and Sort are used to encode the structure of a Generalized Algebraic Theory where the only term constructors are constants. The intended model for the type theory as a whole is then the classifying topos for models of this GAT, i.e. presheaves on the syntactic category of the GAT.

(For added context, the restriction to GATs of this form is partially pragmatic, since implementing bridge types for arbitrary GATs would require solving arbitrary equational theories and make typechecking intractable/undecidable. However, as mentioned in the module, every geometric theory is a geometric quotient of a GAT of this form, hence every Grothendieck topos is a subtopos of one of these presheaf topoi).

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

Written by Ulrik Buchholtz on 2025-01-01 at 23:54

@cbaberle (removing some tags to reduce clutter). Thanks, I get the general idea, but I was hoping to hear a bit more about how exactly it corresponds to these GATs, and how the postulates are interpreted in the model. It’s late here, so I’ll have a closer look tomorrow.

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

Written by Jesper Agdakx 🔸 on 2025-01-04 at 20:09

@cbaberle That looks awesome! It will never cease to amaze me what people manage to do with rewrite rules (which were at first just a way to implement slightly less hacky HITs back when we didn't yet have Cubical Agda).

=> More informations about this toot | More toots from jesper@agda.club