proposition: Lemma induced_precategory_reflects_pushouts {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) : isPushout (# (induced_precategory_incl j) f) (# (induced_precategory_incl j) g) (# (induced_precategory_incl j) p1) (# (induced_precategory_incl j) p2) H -> isPushout f g p1 p2 H.
proof: Proof. exact (λ pb T, pb (j T)). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors