proposition: Lemma MonicPullbackisMonic {a b c : C} (M : Monic _ b a) (g : c --> a) (PB : Pullback M g) : isMonic (PullbackPr2 PB).
proof: Proof. apply make_isMonic. intros x g0 h X. use (MorphismsIntoPullbackEqual (isPullback_Pullback PB) _ _ _ _ X). set (X0 := maponpaths (λ f, f · g) X); simpl in X0. rewrite <- assoc in X0. rewrite <- assoc in X0. rewrite <- (PullbackSqrCommutes PB) in X0. rewrite assoc in X0. rewrite assoc in X0. apply (pr2 M _ _ _) in X0. apply X0. 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