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). Proof. intro g. use (factor_through_squash _ _ (pr2 HF x y g)). { apply isapropiscontr. } intro inv. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isaset_z_iso ; apply homset_property | ] ; use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ; use (maponpaths pr1 (proofirrelevance _ (pr1 HF x y g) (_ ,, _) (_ ,, _))) ; [ exact (maponpaths pr1 (pr2 φ₁)) | exact (maponpaths pr1 (pr2 φ₂)) ]). - exact inv. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.