fact: Definition pseudomonic_weq_fully_faithful_locally_grpd {B : bicat} (inv_B : locally_groupoid B) {a b : B} (f : a --> b) : pseudomonic_1cell f ≃ fully_faithful_1cell f.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells