So the coinvariant should just be the dependent sum, where the invariants is the dependent poduct.
In this sense: for a group object, types with -action are -dependent types.
The homotopy invariants are .
The homotopy co-invariants are .
]]>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.
]]>