Lemma Pushouts_pw_epi (colimD : Graphs.Pushouts.Pushouts D) (A B : functor C D) (a: A ⟹ B) (epia:isEpi (C:=CD) a) : ∏ (x:C), isEpi (a x). Proof. intro x; simpl. apply (epi_to_pushout (C:=CD)) in epia. apply pushout_to_epi. simpl. apply equiv_isPushout1 in epia. apply equiv_isPushout2. red in epia. red. eapply isColimFunctor_is_pointwise_Colim in epia; cycle 1. { intro c. eapply eq_diag_liftcolimcocone. - apply eq_po_pw. - apply colimD. } apply (eq_diag_iscolimcocone _ (sym_eq_diag _ _ (eq_po_pw x)))in epia; cycle 1. set (CC := (make_ColimCocone _ _ _ epia)). eapply (is_z_iso_isColim _ CC). rewrite <- (colimArrowUnique CC _ _ (identity _)). apply identity_is_z_iso. use StandardFiniteSets.three_rec_dep; cbn beta; rewrite id_right; apply idpath. Qed.
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.