Lemma isEffectivePw : (∏ (x:C), isEffective (a x)) -> isEffective (C:=CD) a. Proof. intros h. red. transparent assert (f:(kernel_pair (C:=CD) a)). { apply equiv_Pullback_2. apply LimFunctorCone. intro c. specialize (h c). set (f := pr1 h). apply equiv_Pullback_1 in f. use (eq_diag_liftlimcone _ _ f). apply eq_pb_pw. } exists f. apply equiv_isCoequalizer2. apply pointwise_Colim_is_isColimFunctor. intro x. set (g:= f). assert (hf := (pr2 (h x))); simpl in hf. apply equiv_isCoequalizer1 in hf. set (eqd := eq_coeq_pw (PullbackPr1 g) (PullbackPr2 g) x). set (z:= (eq_diag_iscolimcocone _ eqd hf)). set (CC := (make_ColimCocone _ _ _ z)). apply (is_z_iso_isColim _ CC). rewrite <- (colimArrowUnique CC _ _ (identity _)). apply identity_is_z_iso. use StandardFiniteSets.two_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.