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 X, given a collection family {Dc}c∈C including X, then the family {Dc}(c∈C,f:Dc↠X)” is an inhabited collection family equipped with surjections to X. Conversely, given an inhabited collection family equipped with surjections to X, throwing X into the family gives a collection family including X. =–
Anonymous
1 to 3 of 3