Post #1816237

2026-02-27 12:10 UTC

@dwarn Here's a question that I can't answer: how did you come up with this?! Now that I've finished my file, I can explain the result and why it holds, but this is relatively easy because it's post-fact. It only worked because I knew it was true and could look up critical steps in your formalization. @MartinEscardo

Replies (1)

@dwarn@mathstodon.xyz 2026-02-27 13:05

@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.

Open ##1816238