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. exact (λ pb T, pb (j T)). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors.