Hi! I'm Amélia, a non-binary programmer & mathematician. This blog is mostly technical, concerned with type theory. Here are my latest posts:
Posts
-
Parsing Layout, or: Haskell's Syntax is a Mess September 3, 2021
-
Cubical Sets June 21, 2021
In which I try to write about semantics. This is not gonna go well, but I’m gonna try my best. I’ve heard it on good authority that the best way to learn something is to explain it to someone else, so in this post I’m going to use you, dear reader, as my rubber duck while I try to understand cubical sets. These are important (to me) because they provide a semantic model of cubical type theory (which I have written about previously), and since we have a semantic model, that theory is (semantically) consistent.
-
A quickie: Axiom J June 7, 2021
Hey y’all, it’s been three months since my last blog post! You know what that means.. or should mean, at least. Yes, I’d quite like to have another long blog post done, but… Life is kinda trash right now, no motivation for writing, whatever. So over the coming week(s) or so, as a coping mechanism for the chaos that is the end of the semester, I’m gonna write a couple of really short posts (like this one) that might not even be coherent at all—this sentence sure isn’t.
Today’s note is about what is perhaps the most confusing rule of Groupoid Martin-Löf’s dependent type theory, the J eliminator. For starters, its name means basically nothing: as far as I can tell its name comes from the fact that Identity is another word for equality and J is the letter that comes after I.
-
Cubical Type Theory March 7, 2021
Hello, everyone! It’s been a while, hasn’t it? Somehow, after every post, I manage to convince myself that I’m gonna be better and not let a whole season go by between posts, but it never happens. For the last two posts I’ve been going on at length about fancy type theories, and this post, as the title implies, is no exception. In fact, two posts ago I mentioned, offhand, cubical type theory as a possibility for realising HoTT in a constructive way, but 128 days ago I did not understand cubical type theory in the slightest.
-
On Induction January 15, 2021
Last time on this… thing… I update very occasionally, I talked about possible choices for representing equality in type theory. Equality is very important, since many properties of programs and mathematical operators are stated as equalities (e.g., in the definition of a group). However, expressing properties is useless if we can’t prove them, and this is where inductive types come in.
…or you can find more in the archives.