Explaining Gabriel-Zisman localization to the computer
We explain a computer formulation of Gabriel-Zisman's localization of categories in the proof assistant Coq. This includes the general localization construction with the proof of Lemma 1.2 of Gabriel and Zisman, as well as the construction using calculus of fractions.
localization category proof assistant calculus of fractions functor computer proof verification