proposition: Lemma is_versal_equalizer_cone : forall a u v y, equalizer_hypothesis a u v y -> is_versal (equalizer_cone a u v y) = (forall z, equalizer_hypothesis a u v z -> (exists w, (mor a w & source y = target w & comp a y w = z))).
proof: Proof. ir. ap iff_eq; ir. uh H0; ee. util (H2 (equalizer_cone a u v z)). app is_cone_equalizer_cone. rww socle_equalizer_cone; sy; rww socle_equalizer_cone. nin H3. ee. cp H3. uh H5; ee. rwi cone_target_equalizer_cone H6. rwi vertex_equalizer_cone H7. rwi cone_compose_equalizer_cone H4. sh x; ee. am. sy; am. transitivity (eqzmap (equalizer_cone a u v (comp a y x))). rw eqzmap_equalizer_cone. tv. uh H; uhg; ee; try am. rww mor_comp. sy; am. rww target_comp. sy; am. uh H; ee. wrr assoc. rw H10; rww assoc. wr H12. am. sy; am. sy; am. rw H4. rww eqzmap_equalizer_cone. am. am. sy; am. uhg; ee. app is_cone_equalizer_cone. ir. rwi socle_equalizer_cone H2. cp H. uh H3. ee. cp (equalizer_cone_eq H3 H1 H2). cp (equalizer_hypothesis_eqzmap H3 H1 H2). util (H0 (eqzmap b)). am. nin H9. ee. sh x; ee. app cone_composable_equalizer_cone. rww cone_compose_equalizer_cone. rw H11. sy; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal