proposition: Lemma localization_is_idempotent {C : category} (R : reflective_subcategory C) (d : ob R) : z_iso (localization R (precategory_object_from_sub_precategory_object _ _ d)) d.
proof: Proof. exists ((counit_from_left_adjoint (pr2 (pr2 R))) d). abstract ( apply (@counit_is_z_iso_if_right_adjoint_is_fully_faithful C (subcategory C (full_sub_precategory R)) _ _ (pr2 (pr2 R))), fully_faithful_sub_precategory_inclusion). Defined.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Subcategory.Full UniMath.CategoryTheory.Adjunctions.Core