proposition: Lemma induced_precategory_reflects_pullbacks {M : category} {X:Type} (j : X -> ob M) {a b c d : induced_category M j} (f : b --> a) (g : c --> a) (p1 : d --> b) (p2 : d --> c) (H : p1 · f = p2 · g) : @isPullback _ _ _ _ _ (# (induced_precategory_incl j) f) (# (induced_precategory_incl j) g) (# (induced_precategory_incl j) p1) (# (induced_precategory_incl j) p2) H -> isPullback H.
proof: Proof. exact (λ pb T, pb (j T)). 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