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$.

]]>Is there a HoTT formulation as for invariants?

]]>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.