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 ).
1 to 3 of 3