proposition: Lemma ptd_mor_z_iso_from_underlying_mor {F G : Ptd} (α : ptd_mor C F G): is_nat_z_iso (pr1 α) -> is_z_isomorphism(C:=Ptd) α.
proof: Proof. intro Hyp. use tpair. - use tpair. apply nat_z_iso_to_trans_inv. + exact (pr1 α ,, Hyp). + abstract (cbn; red; intro c; cbn; apply pathsinv0; apply (z_iso_inv_on_left _ _ _ _ (make_z_iso _ _ (Hyp c))); cbn; apply pathsinv0; apply ptd_mor_commutes). - abstract (red; split; apply eq_ptd_mor; apply (nat_trans_eq (homset_property C)); intro c; cbn ; [ apply (z_iso_inv_after_z_iso (make_z_iso _ _ (Hyp c))) | apply (z_iso_after_z_iso_inv (make_z_iso _ _ (Hyp c))) ]). Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal