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.
What is a “setoid object” in an (∞,1)-category? In this context and without checking the details, I would expect that groupoid object in an (∞,1)-category would be the relevant notion here, since equivalence groupoids are the analog of equivalence relations.
The setoid stuff is on the wrong page. When people talk about setoids being the (homotopy) exact completion of types in type theory, they are referring to path categories, i.e. as defined in van der Berg & Moerdijk, not -categories.
1 to 4 of 4