proposition: Lemma eq_po_pw {X Y Z :functor C D} {a: X ⟹ Y } {b: X ⟹ Z} x : eq_diag (pushout_diagram D (a x) (b x)) (diagram_pointwise (pushout_diagram CD a b) x).
proof: Proof. use tpair. use StandardFiniteSets.three_rec_dep; apply idpath. use StandardFiniteSets.three_rec_dep; use StandardFiniteSets.three_rec_dep; exact (empty_rect _ )||exact (λ _, idpath _). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Pushouts UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coequalizers