proposition: Lemma is_uni_equalizer_cone : forall a u v y, equalizer_hypothesis a u v y -> is_uni (equalizer_cone a u v y) = (forall z z', mor a z -> mor a z' -> source y = target z -> source y = target z' -> comp a y z = comp a y z' -> z = z').
proof: Proof. ir. ap iff_eq; ir. uh H0. ee. ap H6. app cone_composable_equalizer_cone. app cone_composable_equalizer_cone. rw cone_compose_equalizer_cone. sy; rw cone_compose_equalizer_cone. rww H5. am. am. am. am. am. am. uhg. ee. app is_cone_equalizer_cone. ir. cp H1; cp H2. uh H4; uh H5; ee. rwi cone_target_equalizer_cone H8. rwi cone_target_equalizer_cone H6. rwi vertex_equalizer_cone H9. rwi vertex_equalizer_cone H7. app H0. sy; am. sy; am. rwi cone_compose_equalizer_cone H3. transitivity (eqzmap (equalizer_cone a u v (comp a y u0))). rw eqzmap_equalizer_cone. tv. uh H; ee. uhg; ee; try am. rww mor_comp. sy; am. rww target_comp. sy; am. wr assoc. rw H12. rww assoc. uh H; ee; am. uh H; ee. sy; wrr H14. sy; am. uh H; ee; sy; am. uh H; ee; am. am. am. am. sy; am. tv. rw H3. rw cone_compose_equalizer_cone. rw eqzmap_equalizer_cone. tv. uh H; ee. uh H; ee. uhg; ee; try am. uhg; ee; am. rww mor_comp. sy; am. rww target_comp. sy; am. wr assoc. rw H12. rww assoc. wr H14. am. sy; am. am. am. am. am. sy; am. tv. am. am. sy; am. am. am. sy; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal