Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
One must be careful with transitive action about the empty set, but all is fine here? I guess any group acting on the empty set is a free action.
What’s the HoTT version of freeness? Something like .
I would probably state it as: for any , the type of such that is contractible (or, equivalently, a proposition, since it’s always inhabited by ).
Typed up in the Sandbox the observation/proof that infinity-quotients of infinity-free actions in an infinity-topos are 0-truncated. But need to go offline right now. Will port and polish tomorrow.
[ thought I could weaken the assumptions of the prop, but maybe I can’t ]
What I was after in #7 does work, after all, one has to appeal to the groupoidal Segal conditions:
I have stepped back and added a Definition-subsection
with the declaration that an -action is free if its shear map “in degree 1” is (-1)-truncated, and a proof that this implies that also all “higher shear maps” are (-1)-truncated.
WIth this, the Prop. from #6 above (here) now says that as soon as the shear map of an -action is -truncated, the homotopy quotient of the -action is the plain quotient of its 0-truncated version.
I should add a commentary to the entry on the following point, which can be confusing:
The -action on a principal -bundle is always fiber-wise free, but not globally so unless it’s base space is 0-truncated. Partially-conversely, every -action is fiberwise free (in fact principal) over its homotopy quotient. (all internal to some -topos).
1 to 9 of 9