iiinova — where your digital self keeps evolving

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 15/10/2026

Thinking "why don't I use setoids more often" until I realize there's no `subst` and that's exactly why I don't use them more often.

000 0

Reposted by 🇨🇦 Joey Eremondi

Omar Antolín @oantolin.mathstodon.xyz.ap.brid.gy · 08/10/2026

I did not realize until the Hodge retractions that OpenAI only had formalizations for about 42% of the claims they vomitted two nights ago. They don't have mathematicians that are experts on all those topics, do they? The unformalized 58% they were just praying (to ChatGPT, of course) that they […]

mathstodon.xyz

Original post on mathstodon.xyz

013 3

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 01/10/2026

Sending an email asking when a conference will start accepting submissions. Resisting the urge to make the subject line "ITP CFP ETA"

000 0

Reposted by 🇨🇦 Joey Eremondi

Prof. Sam Lawler @sundogplanets.mastodon.social.ap.brid.gy · 25/09/2026

Well, *someone* needs to post about this on Mastodon www.cbc.ca/news/canada/british-colu…

4866 66

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 24/09/2026

Does anybody have any nice Emacs commands/scripts for building/extending Agda equality reasoning proofs? I find them much easier to read, but a pain to type in.

000 0

Reposted by 🇨🇦 Joey Eremondi

Bastian Greshake Tzovaras @gedankenstuecke.scholar.social.ap.brid.gy · 23/09/2026

«They have mellowed out with age, but this fact remains engraved in their DNA: if no artists are stakeholders, you can’t produce a tool meant for artists. And given that they’re not purporting very hard to be making a tool for artists, it’s unfair to resent them for not making what they have not […]

scholar.social

Original post on scholar.social

001 1

Reposted by 🇨🇦 Joey Eremondi

Tamara Munzner @tamara.cosocial.ca.ap.brid.gy · 22/09/2026

We're hiring at UBC CS in our tenure-track teaching stream. We're in search of systems expertise: our greatest needs are in operating systems and computer architecture; also networking, distributed systems, database systems, cloud computing, and systems security […]

cosocial.ca

Original post on cosocial.ca

005 5

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 15/09/2026

RE: mathstodon.xyz/@joey/11705516034297… - Final Call - Applications are due Sep 16 at 1pm Pacific Time. Please apply, or forward this to undergrads you know who would be interested in applying.

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 14/09/2026

Is there a version of Agda's WellFounded induction which doesn't require FunExt to prove that it calculates an actual fixed point? Something like this, but without the f-ext premise: agda.github.io/agda-stdlib/v2.2/Ind…

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 11/09/2026

That said, the amount of suffering I experienced the one time I tried Cubical, just trying to do normal things with ordinary inductive types and propositional equality proofs, outweighs anything I'm fighting with now.

001 1

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 10/09/2026

No funExt. No univalence. Just suffering.

100 1

Reposted by 🇨🇦 Joey Eremondi

Adrianna Tan @skinnylatte.hachyderm.io.ap.brid.gy · 10/09/2026

The year is 2026. Nobody wants a gamified experience on a website. Don’t give me a badge. Don’t even perceive me

2547 47

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 09/09/2026

Suppose, *hypothetically*, someone had a paper that was ideal for CPP, but wasn't likely to have it done in time for the deadline. Where would you recommend submitting? Bonus points if submissions open in the next couple months. Something that's very much "Here's a literate Agda file […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 08/09/2026

Anyone have tricks for embedding Agda in LaTex /without/ using Literate Agda? Is there any way for the LaTeX backend to generate a file of definitions that I can refer to by name to put a code snippet in LaTeX? Or a way to make a call to agda from LaTeX to do the highlighting? I don't want to […]

mathstodon.xyz

Original post on mathstodon.xyz

100 1

Reposted by 🇨🇦 Joey Eremondi

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 02/09/2026

The real numbers are the friends we made along the way

012 2

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 31/08/2026

Degoogling, boosts welcome Has anyone used Typewire? Was interested because they're Canadian hosted, don't advertise any LLM stuff, and seem security focused. But I've never heard of them before today and for all I know they're full of crap.

100 1

Reposted by 🇨🇦 Joey Eremondi

Jean Abou Samra (new account) @jeanas.mathstodon.xyz.ap.brid.gy · 28/08/2026

I uploaded to my website some notes on descriptive set theory, adapted from lectures I followed last semester: jean.abou-samra.fr/notes/DST.pdf They are unfinished and not very much proofread, but I had to set myself a deadline for making a first version public, or it would just never […]

mathstodon.xyz

Original post on mathstodon.xyz

001 1

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 26/08/2026

Who's hiring functional programmers in 2026? I've got a recent graduate who has been doing really good work on error messages in dependent types, who's taken both my PLAI and PLFA classes. Sadly I haven't been at conferences for a while, so I don't know who's giving out shirts these days. Is […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0

Reposted by 🇨🇦 Joey Eremondi

Matt Boyd @3psboyd.mastodon.social.ap.brid.gy · 25/08/2026

I saw a pretty major contributor to Rust projects making the case for LLMs being used in programming, and one of the things they liked is that you can ask it all the technical questions you want without feeling embarrassed, and what an indictment of the work culture of software engineering that is.

31247 47

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 25/08/2026

Looks like I can do ``reduce (λ {x} pf → x , pf)``

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 25/08/2026

In the agda-stdlib, is there a version of Curry/Uncurry to convert between `(All P v)` for `(P : A -> Set)` and `(v : Vec A n)`, and `(Vec (Σ A P) n)`? I know it's basic induction but it also seems like something that would be there already.

200 2

Reposted by 🇨🇦 Joey Eremondi

Royce Williams @tychotithonus.infosec.exchange.ap.brid.gy · 22/08/2026

Having this printed out on the wall behind where I normally join calls, and being able to point to it when its bingo square comes up in discussion, continues to pay dividends, @mcc

Post from @mcc@mastodon.social:

According to our telemetry, 100% of our users have telemetry enabled

Aug 23, 2025,12:31 PM Tusky

04133 41

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 19/08/2026

Related to last toot, what's the precise sense that GATs and CwFs correspond? The barrier I'm having is that the types don't seem to mismatch: a specific GAT defines a theory, which will have a bunch of models. But CwFs are a specific theory. It's clear how the theory of CwFs is a GAT, but I […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 19/08/2026

Anyone have an Agda formalization of (the definition of) GATs lying around?

000 0

Reposted by 🇨🇦 Joey Eremondi

Anil Madhavapeddy @avsm.amok.recoil.org.ap.brid.gy · 19/08/2026

I'm delighted to announce that our formerly plain PDF ICFP 2026 paper (anil.recoil.org/papers/2026-package…) has been UPGRADED with advanced AI summaries (if you pay up for the premium ACM account) and is under impenetrable cybersecurity protection (if you click through […]

amok.recoil.org

Original post on amok.recoil.org

104 4

Reposted by 🇨🇦 Joey Eremondi

Prof. Sam Lawler @sundogplanets.mastodon.social.ap.brid.gy · 10/08/2026

[DarkSky donation link] I feel bad posting a donation link, because there are so very very many things worthy of donation. But, if you love the night sky, hate what Reflect Orbital and SpaceX are doing to it, and happen to have some spare cash, DarkSky International now has a fund specifically […]

mastodon.social

Original post on mastodon.social

1220 20

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 07/08/2026

Other than gradual typing, are there areas in type theory where we want types to be ordered or in some kind of lattice? Or even just pointed? I've got some stuff cooking and I'm trying to figure out if it's useful beyond the application to gradual types.

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 07/08/2026

Applicants must select 3-10 potential projects, from at least three different provinces. The projects listed here are the PL-focused ones, but students are welcome to apply to any projects that interest them. **Eligibility** •Applicants must be from one of the following partner countries […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 28/07/2026

Alright, suppose I want to mechanize some metatheory in Rocq. Nothing crazy, standard things like progress and preservation and confluence of some calculus. What's currently available for tools to manage definitions of syntax and capture-avoiding substitution, automatically derive the usual […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0

Reposted by 🇨🇦 Joey Eremondi

Jef Poskanzer @jef.mastodon.social.ap.brid.gy · 27/07/2026

What does closure mean to you? I can think of at least three different things. At least I think they are different. - A function plus the environment is executes in. - A special operator in a regular expression, such as *. - A set containing all possible results of applying a function to another […]

mastodon.social

Original post on mastodon.social

100 1

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 13/07/2026

Related to previous question, do (postulated) quotients play nicely with IR, with respect to termination? E.g. I'm in a situation where the only thing I need funext for is showing that something is proof-irrelevant. So I can instead get rid of funext and just use a Squash type to make my […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 13/07/2026

Are there any papers that show MLTT is strongly normalizing if you add Induction Recursion and funext? Or at least "has no infinitely reducing terms". I realize that there isn't canonicity (since there are now non-refl equality proofs), and I'm assuming it's consistent, since the standard […]

mathstodon.xyz

Original post on mathstodon.xyz

100 1

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 11/07/2026

I'm doing Well Founded Induction in Agda, but in my hypothesis, I need a proof that the proof of y < x is irrelevant. Is there a way to do this without resorting to Cubical/Quotients?

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 05/07/2026

My understanding is that Rosette and G2 both require you to rewrite code to avoid general recursion, but I could be wrong.

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 05/07/2026

Are there any symbolic execution/static analysis/abstract interpretation tools for functional programs that are already implemented and runnable? Specifically that support HOFs and recursion. Obviously a heavy amount of conservative approximation will be necessary. I'm aware of some papers […]

mathstodon.xyz

Original post on mathstodon.xyz

212 2

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 03/07/2026

Sanity check... with ordinals (specifically Brouwer trees), you can't prove (∀ x . P (x)) from ∀ x . (P(x) ⟹ P(↑ x)), right? E.g. in the induction principle, you get P(y) for all (y < x), but the property I'm proving is of the form Q(Σ[ a ∈ A](size a ≤ x)), e.g. I'm proving a property of the […]

mathstodon.xyz

Original post on mathstodon.xyz

100 1

Reposted by 🇨🇦 Joey Eremondi

Zach Weinersmith @zachweinersmith.bsky.social · 27/06/2026

Something I worry about a little with this Ai art stuff is I only *think* I can spot it, but actually it's toupee fallacy: en.wiktionary.org/wiki/toupee_... Like, by definition, when Ai art doesn't look like Ai art, you don't notice.

en.wiktionary.org

toupee fallacy - Wiktionary, the free dictionary

712110 121

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 22/06/2026

Every exam I invigilate I like to live dangerously by googling "Big Clock" on a computer hooked up to the projector

000 0

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 22/06/2026

Currently sitting in on a Homotopy Colimit Summer school. I'm guessing it's mostly going to be beyond my background knowledge, but I'm wondering if any of these topics are likely to show up / be useful for dependent type stuff? - Model categories - Equivariant homotopy theory - Functor calculus […]

mathstodon.xyz

Original post on mathstodon.xyz

000 0