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.
I noticed by accident that we have an entry coinvariant. Then I noticed that we also have an entry homotopy coinvariant functor.
I have now added cross-links between these entries and with invariant and orbit, so that they no longer remain hidden.
I also edited the first case of group representation coinvariants at coinvariant a little.
Is there a HoTT formulation as for invariants?
So the coinvariant should just be the dependent sum, where the invariants is the dependent poduct.
In this sense: for $G$ a group object, types $V$ with $G$-action $\rho_V$ are $\mathbf{B}G$-dependent types.
The homotopy invariants are $\underset{\mathbf{B}G}{\prod} \rho_V \simeq H_{Grp}(G,V)$.
The homotopy co-invariants are $\underset{\mathbf{B}G}{\sum} \rho_V \simeq V//G$.
1 to 3 of 3