proposition: Lemma iso_between_pullbacks_are_inv : is_inverse_in_precat iso_between_pullbacks_map iso_between_pullbacks_inv.
proof: Proof. split ; unfold iso_between_pullbacks_map, iso_between_pullbacks_inv. - use (MorphismsIntoPullbackEqual H). + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr1 P). rewrite !assoc. rewrite (PullbackArrow_PullbackPr1 P'). rewrite !assoc'. rewrite z_iso_inv_after_z_iso. rewrite id_left, id_right. apply idpath. + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr2 P). rewrite !assoc. rewrite (PullbackArrow_PullbackPr2 P'). rewrite !assoc'. rewrite z_iso_inv_after_z_iso. rewrite id_left, id_right. apply idpath. - use (MorphismsIntoPullbackEqual H'). + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr1 P'). rewrite !assoc. rewrite (PullbackArrow_PullbackPr1 P). rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_left, id_right. apply idpath. + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr2 P'). rewrite !assoc. rewrite (PullbackArrow_PullbackPr2 P). rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_left, id_right. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monics