proposition: Lemma is_cone_equalizer_cone : forall a u v y, equalizer_hypothesis a u v y -> is_cone (equalizer_cone a u v y).
proof: Proof. ir. uhg; ee. uf equalizer_cone. ap cone_like_cone_create. rw edge_nt_equalizer_cone. ap twoarrow_nt_axioms. app equalizer_twoarrow_nt_hypothesis. rw cone_target_equalizer_cone. rw vertex_equalizer_cone. uh H; ee. rww ob_source. rw edge_nt_equalizer_cone. rw source_twoarrow_nt. rw cone_source_equalizer_cone. rw cone_target_equalizer_cone. rw vertex_equalizer_cone. sy; rw constant_functor_twoarrow_functor. tv. tv. uh H; ee. rww ob_source. Qed.
imports: Arith colimits little_cat fc_limits cardinal