← Feed

Posts

• Post #4230143

  I have been trying to see how capable of GPT 5.5 (Business plan, $20 per month) is by implementing an experimental language server for Agda after work. So far, it kind of works but requires closer inspection and quite an intensive interaction between the agent / the chat mode to make the spec very detailed and to fix unexpected behaviour introduced when the spec is not clear enough. I am not sure if it counts as "vibe coding", as I still have to figure out what VS Code, LS...

• Post #4230142

  Today's episode is that I need to work in the internal language we just built to build another model internally. 🤯

• Post #4230141

  Is Agda the only implementation that supports (indexed) inductive-recursive types? Let’s forget about the extra flexibility of the recursion part allowed in Agda.

• Post #4230140

  I wish there were other implementations of 2-level type theory, not just MLTT (outer) / HoTT (inner) but rather OTT / MLTT, as it is quite hard to track down which is which... 😵

• Post #4230139

  I just learned that the strong J (the SProp-to-Type elimination for the strict identity type) is actually okay and it is discussed already in the paper on definitional proof-irrelevance. I should have read the paper more carefully..

• Post #4230138

  Strictness is fragile.

• Post #4230137

  Not assigning a specific topic directly for intern students always makes me excited about what students are capable of and the diversity of their interests. 🤩 Two years ago, one of interns proposed a research question about the equivalence of two fractal constructions as functional programs and it later becomes a cute paper (under revision) about the classic second duality theorem in program derivation. And today, my new intern proposes to do some recently developed math in Cubical Agda. (The...

• Post #4230136

  Playing with 2LTT in Agda leads me to wonder if some form of relative canonicity holds in particular that if context, types, and both sides of the outer identity are inner terms, then these term are actually judgementally equal. I’ve been very confused by the claim that the outer identity is the internalised judgemental equality, but IIUC this hold if the outer theory is extensional. 🤔

• Post #2121599

  https://lawrencecpaulson.github.io/2026/04/23/Why_not_Lean.html

• Post #952406

  Attending conferences is (perhaps) healthy for your mind but (definitely) unhealthy for your body – sleep deprivation, sitting still for hours and unlimited supply of food, sweet, and snacks during each break. I found I am not that young to enjoy it without worrying about my sugar intake etc., so this time I have brought my bike to do some exercise before and after. The side effect is that I have visited places where I couldn't with just the public transportation with the total of 150k...

• Post #952404

  I recently found that the term "setoid" is like domain -- there are more than one precise formulation of setoid (in various settings) and one should always check which setoid they actually talk about.

• Post #952400

  Thanks to @qbane and @banacorn, Agda now runs in *your browser* via VS Code for the Web — tested on Safari and Chrome, on both desktop and iPad! A pre-release is now available in the VS Code Marketplace (library management not yet supported, though). You can open a remote repository on GitHub by pressing '.' to give it a try yourself. A proper announcement will follow somewhere after a stable release — I’m just too excited not to share this now. This project began during AIM X...

• Post #952398

  My first accepted submission that I had no expectation to be accepted or rejected. See you at CPP.

• Post #952394

  Learned recently from Simon Boulier et al.’s paper on syntactic models and subsequent papers to give a model of type theory which refutes, for example, the function extensionality. The syntactic model is fairly easy to construct and instructive. I wonder if there are classical principles, such as LEM, that can be refuted easily this way. 🤔

• Post #952390

  Some experience about my on-going work: It is harder to get things done easily than in a complex way. We started with a naive construction in a stronger meta-theory, but it kept asking stronger assumptions and did not really solve our problem. Then, we retracted to a simpler setting with a more complicated construction (to replicate the intended construction in the previous step) and another even more complicated construction. It works but the construction consists of many mysterious steps....

• Post #952388

  RE: https://discuss.systems/@amoine/115900176355656326 lol

• Post #952386

• Post #952384

  RE: https://mathstodon.xyz/@fnf/115960729940528764 Very happy to have @fnf visiting us and we did have very productive and exciting (!?) weeks for research. 🥳