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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal.