Pinned toot

Are you tired of maintaining two lists of publications, one for your LaTeX CV and one for your homepage? Then my latest project might be for you.

Simpy upload your Bib(La)TeX file, tweak the template to your liking and download HTML code for your homepage.

When you update your LaTeX resumé, simply upload it again and get new HTML.

Pinned toot

I handed in my thesis!

They've set up for a very predictable twist, so hopefully there's none lol

Show thread

The Night Agent is a bit shit ain't it? Maybe it gets better

In Mario Maker, creators sometimes put hidden exits in their levels because they have to beat them before they are allowed to upload them. These are called "dev routes", which is, like, routes for @dev

Few technologies disappoint me as much as the phone speech assistants.

It's cool that it understands me saying "connect to the argon speakers" but it's shit that it means nothing to it.

_Functional Programming in Lean_ is now done and out the door!

It's a free online book that describes using the interactive theorem prover Lean 4 as a programming language, without assuming any background in functional programming. You don't need to already know Haskell, OCaml, Rust, Scala, or Racket to read this book.

You can read it at .

Thank you to everyone who's carefully read prereleases - it's much, much better than it otherwise would have been. The Lean Zulip is a great place to hang out.

Also, thanks to MSR for supporting this project, and to Leonardo de Moura for initiating it. It's been a lot of fun!

I'm starting to think I don't like story in platformer games

I enjoyed Celeste until there were too many mechanics and it got too hard for me. Maybe I should try to play the easy parts of Strawberry Jam 😅

Girlfriend, petting cat: She wants head pats!
Me: Is she a trans girl on the internet?
Girlfriend: I think they got it from cats, not the other way around

"If Bre has a problem with me bringing up her personal life at the office, she can come talk to me herself."

I love these people.

@JadeMasterMath @mc

It's subtler than that. Each type has its own identity type.

But the identity type is defined in a uniform way for all types, by the data (Id, refl, J, +conversion rules).

But then, you can *prove* characterizations of the identity types for different types.

For the type of natural numbers, for example, the identity type gives the notion of equality you would expect, which you can define by induction on natural numbers.

For a type universe (a larger type of small types), univalence says that identifications are in 1-1 correspondence with bijections.

For the type of groups, you can prove that identifications are in 1-1 correspondence with group isomorphisms.

For the type of subgroups of a given ambient group, you can prove that equality of two subgroups is "having the same elements of the ambient group" (not isomorphism!).

Now what is common about *all* identity types of any type, is that you can "transport".

Let's write Id x y for the type of identifications of x and y (rather than x=y). Then the transport theorem is that

Id x y and P x together imply P y.

Here P x can be a property of x, but it can also be data on x.

So, for example, if you have two types X and Y and P X is "group structure on X", then, because of the above characterization of identities in the type of types, the transport theorem says that from a group structure on X you get a group structure on Y.

But the point is that transport can be applied not only to isomorphism, but to any kind of identification.

"I live at the beach so I'm used to beach living."

My girlfriend is watching Selling Sunset again and it remains extremely funny to me how much these women pay to look like sex workers.

What I usually say holds true: people are always nice to me and things always work out for me 🥰

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.