proposition: Lemma eq_pb_pw {X Y Z:functor C D} (a: X ⟹ Z) (b: Y ⟹ Z) (c:C) : eq_diag (pullback_diagram D (a c) (b c)) (diagram_pointwise (pullback_diagram CD a b) c).
proof: Proof. intros. 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