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.
Again, I think it’s worth considering creating a separate page for this other notion you’re referring to. See my earlier comment in the other thread.
removing query box from article
+–{: .query} Mike Shulman: Are the first two the same? If not, why are they given the same name?
Peter LeFanu Lumsdaine: Yes, they are equivalent. For any , given a collection family including , then the family ” is an inhabited collection family equipped with surjections to . Conversely, given an inhabited collection family equipped with surjections to , throwing into the family gives a collection family including . =–
Anonymous
1 to 3 of 3