Amélia Liao 🍊

Main author of the 1Lab and spooky cubical ghost haunting your citrus trees. Charitably describable as "hinged"

Public Key

npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnw

NIP-05 Address

[email protected]

Profile Code

nprofile1qqs86xe9mkfupg4acdtvcl8260zkhsqd54var9jslp2tc7jq8h9s0qcpzpmhxue69uhkummnw3ezuamfdejsf735lw

Publishing to

nostr.wine

Author Public Key

npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnw

Show more details

Last Notes

2026-06-26 12:22:17 GMT

For a long time my birthday has been a pretty depressing time: even here in the tropics 🏖️🌴💃 June is a cold and dry and dreary month with short ass days where nothing gets done, and this does not help process the previous year in an objective light. For, like, a decade running, it has only felt like I'm tallying up another year spent stagnating.
But this year, for a change, I do have a project that feels meaningful. However small its impact may turn out to be, I feel like I am doing something that matters, and that I am doing the right thing. And even through my depression I can be proud of that

2026-06-15 00:50:10 GMT

something the physicists won't tell you is that if you add enough bodies it becomes real easy to calculate their orbits as the entire system decays into a black hole

2026-05-27 23:54:01 GMT

beware: your consequences might have carequences and cdrequences

2026-05-05 13:40:43 GMT

We're announcing Mikan: a proof assistant for cubical type theory, forked from the Agda codebase.
Note: you can also read this announcement as a Gist.
The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are "concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet", but refuse to take any concrete action to address their own contribution to these. They have judged the hypothetical future usefulness of the slop generators as outweighing the present, very real harm being caused by the AI industry.
We understand that, over its 20 years of Git history, Agda's implementation has evolved to cater to subsets of its user-base with very diverse, and often conflicting, needs. However, the attempts to bridge these divides (e.g. --without-K vs. --cubical-compatible) present a significant maintainership cost, and are often resented by both camps, since they present one camp with substantial performance costs, while offering the other camp no clear benefit, since code across the divide is written with very different formalisation sensibilities.
Other extensions to the type theory are kept despite known inconsistencies (sized types), or being impossible to adopt without complete vertical buy-in (cumulativity, erased cubical), or simply for backwards compatibility (--guarded/@lock). In the best cases, these features are championed by a single maintainer, and keeping them well-tested against the continuous adoption of new features is a struggle when very little code uses them.
Our plan is to focus on exactly one variant of the language ("full --cubical"), and to drop support for all the language features which are explicitly deprecated, inconsistent, or simply ill-understood in conjunction with this fragment. This will give us a solid base from which we can work to improve the experience of working on the Mikan codebase, to attack the existing correctness and usability issues with features like termination and positivity checking, and to pursue breaking improvements to the core type theory and its user interface.
Signed:
Amélia Liao (@nprofile…ktlj)
Naïm Favier (@nprofile…2p65)
Reed Mullanix (@nprofile…pkkx)

2026-04-20 08:51:56 GMT

gasp. i'm shocked. this is my shocked face: 😐
#nevent1q…5385

2026-03-22 11:42:18 GMT

here's a cursed trick that i should probably write up as a blog post but writing for my blog is super hard for reasons i don't comprehend (probably having to use uppercase letters).
if you've tried to do anything with monoidal categories or (as pictured) bicategories in Agda you will probably be aware that getting the goals to print nicely is. an uphill battle. for example, attached is the inferred type of the pentagon axiom. setting aside that the variable B has been renamed in the telescope (i already have a B in scope), there are several problems:
all types of 1-cells are printed as Hom.Ob, with no indication of whence or where they're going. also, the associator is printed as associator.from .η instead of α←.
the 1-cell composition and horizontal 2-cell compositions are printed as compose.F₀ (f , g) and compose.F₁ (f , g).
problem one is actually very easy to address without changing the definition at all. the relevant feature here is something called display forms. agda definitions (including, as in this case, projections) can have bits of metadata attached, consisting of a pattern and a right-hand-side term, which cause the reification pass to print a neutral headed by that definition as something other than an application of that definition.
when you have a module application module Y = X α in scope, agda automatically attaches display forms to (the normal forms of) definitions x from X saying that, if they are applied to the parameter(s) α, they should be printed asY.x, instead ofX.x α, and this applies *regardless* of how you got your hands onX.x α`. for example:
module X (A : Type) where postulate foo : Type
open X Bool renaming (foo to bar)
_ = {! X.foo Nat !} -- normal form prints: X.foo Nat
_ = {! X.foo Bool !} -- normal form prints: bar
so now if you look at the 1lab definition of Bicategory as it was last week, you can spot the problem: the type a ↦ b of 1-cells was just defined as a function, which does not get automatic display forms, and there was a module application of Hom in scope through which you could access Ob without parameters. the first part of the fix is to prevent Ob from being accessible through the copy without parameters:
module Hom {A B} = Precategory (Hom A B)
hiding (Ob)
for the second we need a cursed incantation to work around record definitions allowing module copies but not module bodies before the last field:
private
open module ↦ A B = Precategory (Hom A B)
public using () renaming (Ob to _↦_)
the private declaration applies to the definition of module ↦, but not to the open … public, so the definition _↦_ is still exported. we've now defined _↦_ : Ob → Ob → Type _ entirely through the module system, so we get a display form saying that B .Prebicategory.Hom X Y .Precategory.Ob should be printed as Prebicategory._↦_ B X Y, which doesn't look like an immediate improvement, but this rule "stacks", so if you have a local module B = Prebicategory B, you'll see X B.↦ Y instead. if we apply this trick also to the coherence maps, you get the second version, which is a marked improvement.
but even in the second version, the composition operator(s) print prefix: ⊗.F₁ (Hom.id , α← (g , h , i)). unfortunately, there is no way to uncurry a function (here the F₁ field of the composition functor) using the module system only, and user-written display forms can't match on neutral projections, so this is as far as the improvements go without changing the types of the fields that go into a bicategory.
for the longest time i have known what the solution was: change the definition of Bicategory to be in terms of an "atomic" definition of bifunctor, instead of having composition have type [ Hom B C × Hom A B , Hom A C ]. but this sucks, for a variety of reasons, so i didn't want to do it. however. if you have a friend whose brain is in the "on" position more often than mine (for me, that was @nprofile…pkkx), they might point out that if you transpose that to [ Hom B C , [ Hom A B , Hom A C) ] ], the actions of the composition functor basically take two arguments. so you might wonder: can we define those entirely with the module system? and the answer is yes!
if you have a Functor C Cat[ D , E ], these arcane sigils project out the action on objects as a two-argument function, and the actions on morphisms in each side as a pair of whiskerings that take both the morphism to act with and the object that isn't changing: A ▶ f and g ◀ B, as written there, but you can use another symbol. and by redefining bicategories to take one of these instead, we can get the normal form(!!) of the inferred type of pentagon to print as written (modulo the renaming to avoid B again, sigh).
this isn't a completely painless refactor, since it changes the primitive 2-dimensional operator from horizontal composition to a pair of whiskerings, but it is super doable (we're in the process of doing it), and also super worth it. it also breaks less than you might expect: just this last week we got a drive-by pull request adding a solver for equations in bicategories, basically a practical version of the coherence theorem, which feels like something that would have to be completely rewritten to account for this change, right? not right! it was a ± 30 diff to get it working, and most of that was from having to split the whiskerings in the syntax.
https://pool.jortage.com/typespl/media_attachments/files/116/272/460/646/539/146/original/063dc6bd68dc851d.png
https://pool.jortage.com/typespl/media_attachments/files/116/272/564/238/409/216/original/a506f3863a16d76c.png
https://pool.jortage.com/typespl/media_attachments/files/116/272/592/433/552/145/original/5aba89128f5ef8b2.png

2026-03-10 09:37:30 GMT

look at my stupidly photogenic cat
https://pool.jortage.com/typespl/media_attachments/files/116/204/203/717/798/588/original/481d45f590383113.jpg

2026-01-26 07:47:59 GMT

my Agda 2.9.0 features: record where, qualified do, qualified idiom brackets, new conversion checking errors, info buffer go-to-definition, parallel type checking

2025-12-20 12:36:42 GMT

- reply

@nprofile…w8t5 @nprofile…rrqe Actually, it is MLTT! See, like, §4.1.3 in Jesper's thesis. It shows how to automatically construct an equivalence between true ≡ true and ⊤, without K, and then §4.3 shows you how to deploy that equivalence to translate the pattern-matching function you wrote to one in terms of nothing but eliminators while preserving all the clauses you wrote as definitional computation rules. There is no bug here. There's barely even a feature request here, since you've already lobbied for --no-pattern-matching in the past. I don't want to commit to supporting twelve other feature flags for whatever unification step you feel unhappy with on a given day. You know these functions all rely on the exact same behaviour, right? Why isn't this file called MLTT.Wrong-Vector?

2025-12-13 22:39:01 GMT

- reply

@nprofile…rrqe make sure NOT to tell any of the developers and conspiracypost on maths reddit

2025-12-13 16:08:06 GMT

- reply

@nprofile…rrqe it's the only thing i've written that people, unprompted, thank me for 😆

2025-11-15 14:59:23 GMT

definition. an anaesthetic is a substance which has the function of negating aesthetics

2025-11-15 11:48:05 GMT

if i were implementing an elaborator it would be completely stateless outside of metavariables which are ofc local to a binding-group

2025-09-30 10:31:15 GMT

it's annoying that reversals are presently problematic because honestly i'm down to drop the connections but having the reversals makes everything so much easier

2025-08-11 17:08:55 GMT

https://preview.1lab.dev/538/Cat.CartesianClosed.Free.html wowie the 1lab formalisation of nbe-by-gluing has grown Text

2025-08-06 21:14:27 GMT

I did nbe for free CCCs the right way but theres like a billion things to write up still so this module has like no text yet

2025-04-03 06:52:10 GMT

i don't know where to ask this question but like what happened after the k-pg extinction to select for mammals instead of like another clade of lizards

2025-02-13 22:23:25 GMT

uh oh so apparently the us senate released its database of woke grants onh one of emily riehl's higher category theory grants is on there

2024-07-13 07:25:40 GMT

the purpose of a system is what it does and what war thunder does is convince nerds to leak military intelligence when they're malding

2024-05-10 20:48:53 GMT

Love walking half way down the terminal 2 buy a can of coke for thrice its normal price