proposition: Lemma socle_equalizer_cone : forall a u v y, socle (equalizer_cone a u v y) = twoarrow_functor a u v.
proof: Proof. ir. uf socle. rw edge_nt_equalizer_cone. rw target_twoarrow_nt. tv. Qed.
imports: Arith colimits little_cat fc_limits cardinal