Same with the other article; 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.
]]>Changed “homotopy fiber product” to “(∞,1)-fiber product”
]]>The properties and references were for a different sense of “exact” than the idea and definition, so I created an “other notions”.
In my opinion, the (∞,1) content on nLab should mimic the 1-category versions when feasible, so this page should be reserved for the version that was defined here (generalizing “effective regular”) and a separate page should be made for the other version.
I have zero knowledge about it, though, so I’m not actually certain it would be appropriate to create a page titled “Quillen exact (infinity,1)-category” and fill it with the stub that was originally at this page.
]]>