Added an expositional section *Examples – Discrete group actions on sets* which spells out in detail how the general abstract slicing perspective recovers ordinary permutation representations.

I should maybe copy this also to, or at least link to also from, *action groupoid* and *permutation representation*.

I have now written this (linearization of $\infty$-actions) out in more detail in section 3.10.5 of dcct (pdf).

In section 3.10.11 I use this to axiomatize Cartan geometry in differential cohesion, via the key example (3.10.45) of the canonical linearized $H$ action on $\mathfrak{g}/\mathfrak{h}$ .

(I have been fiddling with the axiomatization of Cartan geometry in homotopy-type theory a bit, as you may recall. My first versions were not so good, but I think now I am converging.)

]]>There is a nice formalization of linearization of $\infty$-actions in axiomatics of differential cohesion. I have added it to the entry here.

(The text deserves further polishing, but I am in a haste now as my battery is dying.)

]]>added a little observation – here – on how the automorphism action on an object in a slice is given by descending the corresponding map to the homotopy quotient of the induced action on the dependent sum.

(This innocent statement gives symplectic reduction for prequantum n-bundles)

]]>added now also a new section *References – For actions of topological groups* with the following text (which might also go into a Properties-section, admittedly):

[ text extracted from entry ]

That $G$-actions for $G$ a topological group in the sense of G-spaces in equivariant homotopy theory (and hence with $G$ *not* regarded as the geometrically discrete ∞-group of its underying homotopy type ) are equivalently objects in the slice (∞,1)-topos over $\mathbf{B}G$ is Elmendorf’s theorem together with the fact, highlighted in this context in

- {#Rezk14} Charles Rezk,
*Global Homotopy Theory and Cohesion*, 2014

that

$G Space \simeq PSh_\infty(Orb_G) \simeq PSh_\infty(Orb_{/\mathbf{B}G}) \simeq PSh_\infty(Orb)_{/\mathbf{B}G}$is therefore the slice of the $\infty$-topos over the slice of the global orbit category over $\mathbf{B}G$.

!include equivariant homotopy theory – table

See at *equivariant homotopy theory* for more references along these lines.

…

]]>added to *infinity-action* under a new section *References – For discrete geometry* pointers to articles that discuss $G Act_\infty \simeq \infty Grpd_{/ B G}$.

(copied the same also to the end of the citations at *principal infinity-bundle*).

Added at *infinity-action* brief remarks in new subsections

This is more to remind myself to come back to it later. No time right now.

]]>I have been expanding at *infinity-action* in an attempt to make the discussion more comprehensive and more coherent. But not done yet.

For instance I made explicit that for $\mathbf{c} : \mathbf{B}G \vdash V(\mathbf{c}) : Type$ an $\infty$-action we have

the dependent product

$\vdash \prod_{\mathbf{c} : \mathbf{B}G}V(\mathbf{c}) : Type$

is the type of

**invariants**of the action;the dependent sum

$\vdash \sum_{\mathbf{c} : \mathbf{B}G}V(\mathbf{c}) : Type$

is the

**quotient**of the action

And hence for $V_1$ and $V_2$ two actions we have that

$\vdash \prod_{\mathbf{c} : \mathbf{B}G} V_1(\mathbf{c}) \to V_2(\mathbf{c}) : Type$

is the type of $G$-homomorphisms (of $G$-equivariant maps);

$\vdash \sum_{\mathbf{c} : \mathbf{B}G} V_1(\mathbf{c}) \to V_2(\mathbf{c}) : Type$

is the quotient of all maps by the $G$-cojugation action.

started an entry *infinity-action*