proposition: Lemma isEffectivePw : (∏ (x:C), isEffective (a x)) -> isEffective (C:=CD) a.
proof: 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.
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