proposition: Lemma coequalizer_hypothesis_comp : forall a u v y z, coequalizer_hypothesis a u v y -> mor a z -> source z = target y -> coequalizer_hypothesis a u v (comp a z y).
proof: Proof. ir. rw coeq_hyp_eq_hyp. rwi coeq_hyp_eq_hyp H. assert (flip (comp a z y) = comp (opp a) (flip y) (flip z)). rw comp_opp. rw flip_flip. rww flip_flip. uh H; ee; am. rww mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip. sy; am. alike. uh H; ee. rwi mor_opp H2. rwi flip_flip H2; alike. rw H2. ap equalizer_hypothesis_comp. am. rww mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip. sy; am. alike. uh H; ee. rwi mor_opp H3. rwi flip_flip H3; alike. uh H0; ee; am. uh H0; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal