Definition of transitive G-set

[pierrecagne]

I think our definition of transitive $G$-set is flawed.

Right now the definition of $X$ being a transitive $G$-set reduces to the propositional truncation of $$\sum_{b:X(shG)}\prod{a:X(shG)}\sum{g: UG}g\cdot b = a.$$

However, if we want (and we really do!) transitive $G$-sets to correspond to connected set bundles over $BG$, I think we really want the propositional truncation of $$\sum_{b:X(shG)}\prod{a:X(shG)}\exists{g: UG} g\cdot b = a.$$

And I don't see why the internal truncation of the $\exists$ could be omitted. Am I missing something?

[UlrikBuchholtz]

I agree. (For finite sets X, we can use finite choice to go the other way, but not in general.)

[marcbezem]

Does that mean that the proof of Lemma 4.7.13 now (implicitly and inadvertently) uses AC?

[UlrikBuchholtz]

Yes, exactly.

[UlrikBuchholtz]

I've pushed 67f2c79 which fixes the definition and the following remark, but touches nothing else. (It also illustrates the new scaling \exists.) Should we use \exists also for the outer truncation+sum?

[marcbezem]

Yes. I think the purpose of Remark 4.7.12 is to simplify Definition 4.7.11, and using \exists also for the outer truncation+sum is simpler. Another point is the use of "there (merely) is/exists" in Remark 4.7.12 and the proof of Lemma 4.7.13, several times, but not for the "g". Given my "Yes" above, they now all phrase \exists so we could perhaps use "there exists" (without "merely") for all of them?

[UlrikBuchholtz]

Done in bb573d7 – Can we now close this issue?

[pierrecagne]

I think so, looks good to me.