proposition: Lemma eqz_dotted_comp : forall a u v z, has_equalizer a u v -> mor a z -> source (equalizer a u v) = target z -> eqz_dotted a u v (comp a (equalizer a u v) z) = z.
proof: Proof. ir. assert (equalizer_hypothesis a u v (equalizer a u v)). app equalizer_hypothesis_equalizer. ap eqz_dotted_uni. am. app equalizer_hypothesis_comp. uhg; ee. app is_cone_equalizer_cone. rww cone_target_equalizer_cone. rww vertex_equalizer_cone. sy; am. rw cone_compose_equalizer_cone. tv. am. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal