So, the overall question is in the title: Does a compact topological loop with the inverse property have a Haar measure that is simultaneously left and right invariant? (And we can restrict to Moufang loops if that's necessary but I don't think it ought to be.) But I want to break it down in to several parts.

For background: It's known, due to Stehlikova et al. 2011, that Haar measure generalizes from locally compact groups, to locally compact inverse-property loops (which includes Moufang loops), provided they meet a certain condition that I'll get to in a moment; that paper shows existence and a later paper of theirs shows uniqueness (up to the usual multiplicative constant).

I want to be able to talk about picking an element at random from a compact Moufang loop (or, more generally, a compact inverse-property loop, since I think that ought to be sufficient so we may as well be general). For compact groups this makes sense, because compact groups are unimodular. So I similarly want compact inverse-property loops to have bi-invariant Haar measure.

So we can break down the question as follows:

1. Do compact inverse-property loops always have Haar measure, with no other conditions necessary?
2. Provided they do, is that Haar measure bi-invariant?

I think I can prove the second, but I'm getting stuck on the first. I do suspect it's true though -- let's break this down further.

I mentioned that the Stehlikova paper assumes an extra condition beyond local compactness. That condition (assuming we're talking about a left Haar measure) is that the topology comes from a left-invariant uniformity. For a group that's automatic, but without associativity, it isn't! So I'm hoping that if we assume compactness that will make it automatic.

See, I initially thought this was obvious, on account of, a compact space only has one uniformity, so of course that uniformity is left-invariant, as if we translate it on the left, that has to yield the same uniformity again. The problem is, that's not actually what "left-invariant uniformity" means in the theory of topological loops; it means a uniformity with a basis of left-invariant entourages, a rather stronger requirement! So it's not obvious to me that the unique uniformity has that property. It seems to me it ought to, but I'm getting stuck on proving it. So that's the key sticking point right now: Is a compact inverse-property loop's unique uniformity left-invariant (and therefore also right-invariant)? (Again, in the particular sense defined here.)

That's the bulk of the question, but I should elaborate on why I'm pretty sure (2) is true, for completeness. Note we can't use the easy proof via the modular function, since as best I can tell you need associativity to show that the modular function is well-defined. But consider; with groups there's another proof, which goes that, any group with equivalent uniformities (aka a "balanced group" or "SIN group") is unimodular, and a compact group obviously is balanced on account of there's only one uniformity on a compact space, therefore a compact group is unimodular. So we can try to mimic that approach.

So now we can break things down into 3 steps:

1. Does a compact inverse-property loop have a left-invariant (and hence also a right-invariant) uniformity? (Again, in the particular sense described above.)
2. Supposing it does, are they the same uniformity? (Yes.)
3. Supposing they're the same, does that imply the same Haar measure works for both sides?

Part (1) is the question I asked about above. Part (2) is of course true because a compact space only has one uniformity. That leaves part (3).

By the same reasoning as in Proposition 4.14 in the paper linked above, we can conclude that such a loop $L$ has a base of neighborhoods $U$ of the identity such that $xU=Ux$ for all $x\in L$. If we were in a group we'd use the modular function, but, again, I don't think we can do that here. But -- and there may be an easier way that I'm missing, but oh well -- we can go through the whole construction, restricting to such sets as our sets to compare against instead of all neighborhoods of the identity; that should get us a Haar measure which is both left and right invariant.

So: Is step (1) true? (Is this easy and I'm just missing it?) And also, is there by any chance an easier way to do step (3)? (Alternatively, have I made a mistake in it...?)

Thanks all!