proposition: Lemma cone_compose_equalizer_cone : forall a u v y z, equalizer_hypothesis a u v y -> mor a z -> source y = target z -> cone_compose (equalizer_cone a u v y) z = equalizer_cone a u v (comp a y z).
proof: Proof. ir. assert (lem1: equalizer_hypothesis a u v (comp a y z)). uh H; uhg; ee. am. rww mor_comp. rww target_comp. wr assoc. rw H4. rww assoc. uh H; ee; am. uh H; ee. wr H6. am. uh H; ee; am. am. am. am. am. tv. assert (lem2 : cone_composable (equalizer_cone a u v y) z). uhg; ee. app is_cone_equalizer_cone. rww cone_target_equalizer_cone. rww vertex_equalizer_cone. sy; am. ap eqzmap_extensionality. rww is_cone_cone_compose. app is_cone_equalizer_cone. rw cone_source_cone_compose. rww cone_source_equalizer_cone. rw socle_cone_compose. rww socle_equalizer_cone. rww socle_equalizer_cone. rww eqzmap_cone_compose. rww cone_target_equalizer_cone. rww eqzmap_equalizer_cone. rww eqzmap_equalizer_cone. app is_cone_equalizer_cone. rww cone_source_equalizer_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal