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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Coequalizers.