proposition: Lemma comp_coequalizer_coeqz_dotted : forall a u v y, has_coequalizer a u v -> coequalizer_hypothesis a u v y -> comp a (coeqz_dotted a u v y) (coequalizer a u v) = y.
proof: Proof. ir. rwi has_coeq_has_eq H. rwi coeq_hyp_eq_hyp H0. uf coeqz_dotted. uf coequalizer. ap flip_eq. wr comp_opp. ap comp_equalizer_eqz_dotted. am. am. app mor_equalizer. app mor_eqz_dotted. rw target_eqz_dotted. tv. am. am. uh H0; ee. uh H1; ee; am. uh H0; ee. uh H1; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal