proposition: Lemma coeqz_dotted_comp : forall a u v z, has_coequalizer a u v -> mor a z -> source z = target (coequalizer a u v) -> coeqz_dotted a u v (comp a z (coequalizer a u v)) = z.
proof: Proof. ir. cp H. rwi has_coeq_has_eq H. assert (coequalizer_hypothesis a u v (comp a z (coequalizer a u v))). app coequalizer_hypothesis_comp. app coequalizer_hypothesis_coequalizer. rwi coeq_hyp_eq_hyp H3. uf coeqz_dotted. assert (flip (comp a z (coequalizer a u v)) = comp (opp a) (equalizer (opp a) (flip u) (flip v)) (flip z)). rw comp_opp. sy; rw flip_flip. uf coequalizer. tv. app mor_equalizer. rww mor_opp. rww flip_flip. ufi coequalizer H1. rwi target_flip H1. wr H1. rww target_flip. alike. apply mor_arrow_like with (opp a). app mor_equalizer. rw H4. rw eqz_dotted_comp. rww flip_flip. am. rw mor_opp. rww flip_flip. ufi coequalizer H1. rwi target_flip H1. wr H1. rww target_flip. alike. apply mor_arrow_like with (opp a). app mor_equalizer. uh H0; ee; am. uh H0; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal