proposition: 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: 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.
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