Toots for cbaberle@mathstodon.xyz account

Written by C.B. Aberlé on 2025-01-21 at 02:16

you can pry the F on my passport from my cold, dead hands.

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2025-01-14 at 04:41

You might also notice that the website's had a bit of a makeover since I announced it, including some nifty features like an interactive graph and search functionality, thanks to now running on Obsidian! Check it out: https://hyrax.cbaberle.com/Hyrax/index.lagda

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2025-01-14 at 04:38

I've collected my thoughts on Synthetic Mathematics—as expressed in previous discussion with @chrisamaphone @jcreed @jonmsterling and @MartinEscardo, into a blog post on The Hyrax Project: https://hyrax.cbaberle.com/Hyrax/Philosophy/Synthetic+Mathematics

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2025-01-09 at 21:26

the set of all sets be like: “do i contradict myself? very well, i contradict myself. i am large. i contain multitudes.”

=> More informations about this toot | View the thread

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 | View the thread

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 | View the thread

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 | View the thread

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 | View the thread

Written by C.B. Aberlé on 2024-12-23 at 04:49

I'm curious: for other people here, what's the highest power of each prime you can recognize without having to check? For me it's:

2^16 = 65536

3^7 = 2187

5^5 = 3125

7^4 = 2401

11^4 = 14641 (last power of 11 that coincides with a row of Pascal's triangle)

13^2 = 169

17^2 = 289

19^1 = 19

23^1 = 23

...

and so on for primes below 100, most of which I can recognize as prime without having to check.

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-11-24 at 18:20

@chrisamaphone I'm sure other people have already made this joke, so sorry if you're sick of it, but I giggled like crazy when I made this and had to share.

=> View attached media

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-11-22 at 15:40

My best guess so far for what such a "fibrewise coverage" would look like is the following:

For each object (y \in E) and morphism (f : a \to p(y) \in B), a collection of covering families over (f), written ({f_i : y_i \to y \in E \mid p(f_i) = f }_{i \in I}), such that:

1. if (g : x \to y \in E) is a Cartesian morphism, then the singleton family ({g}) is a covering family of (y) over (p(g)).

2. If ({f_i : y_i \to x \in E \mid p(f_i) = f}{i \in I}) is a covering family of (x) over (f : a \to p(x) \in B), and for each (i \in I), ({g_j : z_j \to y_i \in E \mid p(g_j) = g}{j \in J_i}) is a covering family of (y_i) over (g : b \to a \in B), then ({f_i \circ g_j : z_j \to x \in E \mid p(f_i \circ g_j) = f \circ g }_{i \in I, j \in J_i}) is a covering family of (x) over (f \circ g).

3. If ({f_i : x_i \to x \in E \mid p(f_i) = p(g)}) is a covering family of (x) over (p(g)) for some (g : y \to x \in E), and (h : a \to p(y)) is a morphism in (B), then there exists a covering family ({h_j : y_j \to y \in E \mid p(h_j) = h}) of (y) over (h), such that for each (j \in J) there exists some (i \in I) and (k : y_j \to x_i) such that (p(k) = h) and (g \circ h_j = f_i \circ k).

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-11-22 at 15:35

Wondering if anyone here who knows some topos theory can help me out with something that's come up in my research lately. For (p : E \to B) a fibration, I'm interested in defining some additional structure on (p) which is equivalent to a pseudofunctor (P : B^{op} \to \mathbf{Site}), where (\mathbf{Site}) is the 2-category of categories equipped with coverages (i.e. sites) and morphisms of sites (i.e. functors which are covering-flat and preserve covering families) between them, such that postcomposing (P) with the forgetful 2-functor (\mathbf{Site} \to \mathbf{Cat}) yields the usual pseudofunctor given by taking fibres of (p). Essentially, such a structure should equip each fibre of (p) with a coverage in a manner compatible with the structure of (p) as a fibration. I'm wondering if anyone else has considered these sorts of things before, and if they have a name.

=> More informations about this toot | View the thread

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

@amy great talk by the way!

=> More informations about this toot | View the thread

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

@amy

=> View attached media

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-10-01 at 14:40

Abstract: "Awodey, later with Newstead, showed how polynomial pseudomonads (u,1,Σ) with extra structure (termed "natural models" by Awodey) hold within them the categorical semantics for dependent type theory. Their work presented these ideas clearly but ultimately led them outside of the category of polynomial functors in order to explain all of the structure possessed by such models of type theory.

This paper builds off that work – explicating the categorical semantics of dependent type theory by axiomatizing them entirely in the language of polynomial functors. In order to handle the higher-categorical coherences required for such an explanation, we work with polynomial functors internally in the language of Homotopy Type Theory, which allows for higher-dimensional structures such as pseudomonads, etc. to be expressed purely in terms of the structure of a suitably-chosen ∞-category of polynomial functors. The move from set theory to Homotopy Type Theory thus has a twofold effect of enabling a simpler exposition of natural models, which is at the same time amenable to formalization in a proof assistant, such as Agda.

Moreover, the choice to remain firmly within the setting of polynomial functors reveals many additional structures of natural models that were otherwise left implicit or not considered by Awodey & Newstead. Chief among these, we highlight the fact that every polynomial pseudomonad (u,1,Σ) as above that is also equipped with structure to interpret dependent product types gives rise to a self-distributive law u◃u→u◃u, which witnesses the usual distributive law of dependent products over dependent sums."

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-10-01 at 14:39

New preprint on the arXiv – "Polynomial Universes & Dependent Types," jww David Spivak @ the Topos Institute!

https://arxiv.org/abs/2409.19176

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-08-10 at 21:54

My blog post for the Applied Category Theory Adjoint School (jww Rubén Maldonado), is now up on the n-Category Café: https://golem.ph.utexas.edu/category/2024/08/prismatic_category_theory.html#more

In this blog post, we explore properties of Grothendieck fibrations, with an eye toward getting a better handle on higher-categorical notions such as double fibrations. For this purpose, we develop a graphical framework for displayed categories and fibrations, and subsequently show how this framework can be interpreted in the internal language of simplicial sets, which paves the way for using simplicial type theory as a tool in the study of double categories, double fibrations, etc!

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-08-07 at 17:37

Slides available here: https://cbaberle.com/files/Topos_Slides.pdf

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-08-07 at 17:37

Abstract: Lawvere's categorical formulation of algebraic theories enables one to study some of the most common structures found in mathematics – e.g. groups, rings, etc. – at a high level of precision and generality. However, many significant mathematical concepts, including categories, topological spaces, etc., turn out not to be algebraic, in this sense. Notably, the very framework used by Lawvere to describe algebraic theories and their models – categories with finite products and product-preserving functors between them – cannot be described as an algebraic theory, and so it seems that algebra alone cannot encompass the whole of mathematics (nor even itself). There is, however, a deeper sense in which all of mathematics is essentially algebraic. What is needed to reveal this fact is to adapt the classical notion of algebraic theories, which are fundamentally simply typed, to an appropriate notion of dependently typed algebraic theories. At this level of generality, one is capable of defining not only individual mathematical structures, but structures that themselves encompass whole universes of mathematics, including topoi, models of type theory, etc. In particular, the theory of dependently-typed algebraic theories is itself describable as a dependently-typed algebraic theory. This fact has many profound consequences, of which I shall highlight just one: using the framework of dependently-typed algebraic theories, one can construct a type theory whose types themselves correspond to type theories, with functions between these types corresponding to translations between the corresponding type theories.

=> More informations about this toot | View the thread

Written by C.B. Aberlé on 2024-08-07 at 17:36

My talk for the Berkeley Seminar at the Topos Institute, "All Concepts are Essentially Algebraic," is now live on YouTube! Check it out: https://www.youtube.com/watch?v=RmiTOa4b0bA

=> More informations about this toot | View the thread

=> This profile with reblog | Go to cbaberle@mathstodon.xyz account