proposition: Lemma show_is_coequalizer : forall a u v y , Category.axioms a -> coequalizer_hypothesis a u v y -> (forall z z', mor a z -> mor a z' -> source z = target y -> source z' = target y -> comp a z y = comp a z' y -> z = z') -> (forall z, coequalizer_hypothesis a u v z -> (exists w, (mor a w & source w = target y & comp a w y = z))) -> is_coequalizer a u v y.
proof: Proof. ir. uhg; ee. am. ap show_is_equalizer. wr coeq_hyp_eq_hyp. am. am. ir. set (z1:=flip z). set (z2 := flip z'). assert (z1 = z2). ap H1. uf z1. rwi mor_opp H3. am. rwi mor_opp H4. am. uf z1. rw source_flip; try alike. wr H5. rww source_flip; try alike. uh H0; ee. alike. uf z2. rw source_flip; try alike. wr H6. rww source_flip; try alike. uh H0; ee. alike. rwi comp_opp H7. rwi flip_flip H7. rwi comp_opp H7. rwi flip_flip H7. ap flip_eq. am. rww mor_opp. rw flip_flip. uh H0; ee; am. am. am. rww mor_opp. rw flip_flip. uh H0; ee; am. am. am. ap flip_eq. am. ir. cp H3. set (z1 := flip z). assert (z= flip z1). uf z1; rww flip_flip. rwi H5 H4. wri coeq_hyp_eq_hyp H4. nin (H2 z1 H4). ee. sh (flip x). ee. rww mor_opp. rww flip_flip. rw source_flip. rw target_flip. sy; am. alike. uh H0; ee; alike. rw comp_opp. rw flip_flip. rw flip_flip. ap flip_eq. rw flip_flip. am. rww mor_opp. rw flip_flip. uh H0; ee; am. rww mor_opp. rww flip_flip. rw source_flip. rw target_flip. sy; am. alike. uh H0; ee; alike. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal