proposition: Lemma comp_equalizer_eqz_dotted : forall a u v y, has_equalizer a u v -> equalizer_hypothesis a u v y -> comp a (equalizer a u v) (eqz_dotted a u v y) = y.
proof: Proof. ir. cp (cone_compose_eqz_dotted H H0). transitivity (eqzmap (equalizer_cone a u v y)). wr H1. rw eqzmap_cone_compose. rw cone_target_equalizer_cone. rw eqzmap_equalizer_cone. tv. ap equalizer_hypothesis_equalizer. am. ap is_cone_equalizer_cone. app equalizer_hypothesis_equalizer. rww cone_source_equalizer_cone. app cone_composable_eqz_dotted. rww eqzmap_equalizer_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal