nLab homotopy exact completion

 Idea

A generalization of exact completion from finitely complete categories to categories with path objects, which turns a category with path objects into an exact category.

Examples

• Let $\mathcal{C}$ be the syntactic category of a dependent type theory. Then the category of setoids in $\mathcal{C}$ is the homotopy exact completion of $\mathcal{C}$.

 See also

• categories with path objects

• exact completion

• setoid

References

• Benno van den Berg, Ieke Moerdijk, Exact completion of path categories and algebraic set theory: Part I: Exact completion of path categories, Journal of Pure and Applied Algebra 222 10 (2018) 3137-3181 [doi:10.1016/j.jpaa.2017.11.017, arXiv:1603.02456]