fact: Definition isweq_functor_on_iso_pseudomonic {C₁ C₂ : category} {F : C₁ ⟶ C₂} (HF : pseudomonic F) (x y : C₁) : isweq (@functor_on_z_iso _ _ F x y).
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence