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.
It would be nice if the entry were a little more explicit about the slicing theorem
(here)
In the special case that the small -category happens to be a small -groupoid and that is constant on an object , it ought to be true that an explicit form of this equivalence is given in semi-HoTT notation by
This must be an easy theorem in HoTT?
How would you describe from inside ? I don’t get how this is supposed to be done in HoTT.
Edit: Nevermind I haven’t read this properly.
1 to 2 of 2