proposition: Lemma pb_if_pointwise_pb : (∏ x, isPullback (Hcommx x)) -> isPullback Hcomm.
proof: Proof. intro T. use make_isPullback; intros E h k Hhk. use unique_exists. - use tpair. + intro x; apply (g T E h k Hhk). + apply is_nat_trans_g. - abstract (split; apply (nat_trans_eq D); intro x; [ apply (PullbackArrow_PullbackPr1 (make_Pullback (T x))) | apply (PullbackArrow_PullbackPr2 (make_Pullback (T x))) ]). - abstract (intro; apply isapropdirprod; apply functor_category_has_homsets). - abstract (intros t [h1 h2]; destruct h as [h Hh]; apply (nat_trans_eq D); intro x; apply PullbackArrowUnique; [ apply (nat_trans_eq_pointwise h1) | apply (nat_trans_eq_pointwise h2) ]). Defined.
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