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