proposition: Lemma cone_source_equalizer_cone : forall a u v y, cone_source (equalizer_cone a u v y) = twoarrow_cat.
proof: Proof. ir. uf cone_source. rw socle_equalizer_cone. rww source_twoarrow_functor. Qed.
imports: Arith colimits little_cat fc_limits cardinal