C.B. Aberlé

New blog post up on my website: How Algebraic is Algebraic Geometry? https://cbaberle.com/Blog/How+Algebraic+is+Algebraic+Geometry%3F

This post was the result of me trying to wrap my head around some of the central concepts of modern algebraic geometry and its generalizations from the perspective of someone more at home in type theory, category theory, programming languages, etc. In particular, I've been watching much of the recent work on "synthetic algebraic geometry" with some interest, and also have had a passing interest in the programme of trying to develop geometry over "the field with one element," due to my longstanding interest in the Riemann Hypothesis and the various research programmes it has spawned. If any of that sounds interesting to you, then I hope that this blog post can be as illuminating for you to read as it was for me to write :)

Tagging a few people who I think might find this interesting and/or whose writings on these and related topics have been stimulating to my thinking on this subject: @jcreed@mastodon.social @johncarlosbaez@mathstodon.xyz @thosgood@mathstodon.xyz @dwarn@mathstodon.xyz

Comments, feedback, and criticism are much welcomed! In particular, please do let me know if I got anything wrong! Like I said, I'm very much an outsider to these subjects trying to understand them better for myself.

RE: @arXiv_csLO_bot@mastoxiv.page

New preprint up on the arXiv, applying the theory of polynomial functors in dependent type theory to program verification:

coimage of a map in an exact sequence: i'm going to become the coker

My Topos Institute Berkeley Seminar talk "Synthetic Mathematics, Logical Frameworks & Categorical Algebra" that I gave during my internship there this Summer is now up on YouTube! Check it out: https://youtu.be/MjkWT6GkISI

Hyperdoctrine? I hardly know ‘er doctrine!

i am updating my priors. pray i do not update them further.

RE: @mc@mathstodon.xyz

Just watched this video all the way through, and it does a very good job of capturing my general thoughts on AI and the discourse around it. Highly recommend to those who have the time/interest to watch! Thanks @mc@mathstodon.xyz for the recommendation!

Abstract: Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.