David Wärn

I rarely formalise things, so whenever I do get to be reminded of what it's like. My takeaway this time is how amazing it is that MLTT lets us reason about path algebra completely rigorously and with sol little friction.

@de_Jong_Tom @MartinEscardo I was reading some discussions started by Georg Lehner where Maxime Ramzi suggested that something like should be true, but I couldn't follow the arguments, so I looked for a simple argument that I could understand. First I found a very simple but broken argument that ignored basepoint issues (i.e. conjugation). Then a couple of days later I realised that the conjugation can be shown to be trivial. But in retrospect there is a systematic way of finding this proof. We start with a type A with a binary operation * and an element a₀ : A. Since a₀ * a₀ = a₀, the connected component at a₀ is closed under *. By replacing A with this connected component, we may as well assume that A is connected. Connected pointed types are meant to determined by their loop spaces viewed as higher groups. So really we should consider ΩA, and translate the given information into structure on ΩA. For example * is a pointed map A x A → A and so induces a group homomorphism *Ω : ΩA x ΩA → ΩA. Given two pointed maps f, g : A →. B, an unbased homotopy f(a) = g(a) induces a witness that Ωf and Ωg are conjugate. In this way commutativity tells us that p *Ω q is conjugate to q *Ω p, and associativity that p *Ω (q *Ω r) is conjugate to (p *Ω q) *Ω r. From here it's all just equational reasoning. My Agda formalisation doesn't exactly follow the structure above because I took a bunch of shortcuts. For example Agda doesn't consider it completely obvious that the action of f(x,g(y,z)) on loops is Ωf(p,Ωg(q,r)) and I didn't way to prove this type of thing.

A bunch of cool results on idempotents in a homotopical setting can be found in e.g. Kerodon, but the one above seems to have gone unnoticed. I gave a proof last year in response to a question from Georg Lehner at https://mathoverflow.net/q/496917 . Yesterday I took the time to formalise it in Agda: https://dwarn.se/agda/Idem.html . A weaker result appears in recent papers of Lehner and Antieau (Theorem 5.6 of https://arxiv.org/pdf/2507.00221 and https://arxiv.org/pdf/2508.13106 ).

@de_Jong_Tom @MartinEscardo Thank you both for taking the time to write these much more readable formalisations. I like the idea of separately considering the consequences of commutativity and associativity on loops.

@jakub_et_al Thanks for the reference. Indeed this seems closely related. I guess it's not exactly the same, since in the topological setting you get for free that the homotopies witnessing equations are based. But that's an reasonable assumption to add also in the homotopical setting.

@jdw I guess this is related to "Dickson's lemma" which has an intuitionistic proof according to [1], with the caveat that [1] talks about infinite sequences rather than well-founded induction. According to [2, Corollary 2.4], you can show that an ordering R is well-founded by showing that in the classifying topos of "an infinite R-decreasing chain", false holds. This *should* close the gap between your question and the claim in [1], but there is surely a more direct answer. There's quite a lot of literature on this type of "constructive Ramsey theory". [1] W. Veldman, An intuitionistic proof of Kruskal’s theorem [2] https://www.speicherleck.de/iblech/stuff/early-draft-modal-multiverse.pdf

@SamToth@mathstodon.xyz Maybe... So far I've been a bit more conservative, not allowing any kind of dependency on "category variables".

@jonmsterling@mathstodon.xyz Rewrite rules would probably work. Currently, we are experimenting with something like Licata's trick, relying on private modules. The idea is that Cat models simple type theory, and Agda already implements type checking for simple type theory (+ a lot more). So we privately define Cat to be Type, and expose only the intended operations. Here's an implementation: https://codeberg.org/dwarn/axcat/src/branch/main/src/Cat/Base.agda To be clear, I don't know if this is robust!

@iblech @jdw Do you mean these notes? https://felix-cherubini.de/proper.pdf From this repo: https://github.com/felixwellen/synthetic-zariski