The decision to fork Mikan was not one taken lightly, by anyone involved with the project. Speaking personally, I know I would have rather continued to work with people whom I had looked up to in the past, whose writing was in many ways responsible for type theory being accessible and interesting to me in the first place, and indeed with some I had considered friends.

We're actually coming up to the fourth anniversary of my first commit to this repository; in this time, I had stepped up to maintain three completely orthogonal features, fixed bugs across literally every component other than the compilation backends, and implemented what is likely to be biggest performance improvement possible short of replacing the binary with exit(1); (parallel checking). All completely voluntarily, and, for the majority of that time, without making any demands. I was happy to do it! But when push came to shove, and I asked for what is ultimately a minor compromise for them weighed against explicit for what I believe to be an existential threat, the community landed somewhere between indifferent and getting chummy with self-admitted industry plants.

If the direction of the millenarian community effort is that of embracing whatever grift the soulless oligarchs in the Valley inflict on them, then far be it from me to jump in the way; there's only so many times I can get back up to keep working for the good of an academic pedigree and reputation whose supporting apparatus has taken every possible opportunity to reject my participation in any role beyond that of volunteer labourer, or perhaps "person who shows up to the pub". When standing in the golden halls of bird proof assistants, don't forget who was the janitor.

My ability to pressure anyone into switching implementations essentially ends with the 1Lab contributors, and it gives me great joy that they all stuck around, and even greater joy that a few heroes even stepped up to help with Mikan. They are also doing it voluntarily, and I am proud to have started projects that people can choose to contribute to, even despite my shortcomings.

The unfortunate reality, evidenced by the amount of correctness fixes we've done and performance wins we've pulled off, is that the bandwidth to maintain a proof assistant with seventeen hundred thousand different type theories does not exist anywhere on Earth. Dropping everything beyond what we use is not an attempt at hcomping my way into world domination. I simply believe formalisation is a joy, and I will not let that joy be taken away by people who believe in buying Thinking billed by the hour from the likes of Altman and Amodei.