proposition: Lemma edge_nt_equalizer_cone : forall a u v y, edge_nt (equalizer_cone a u v y) = (twoarrow_nt a (id a (source y)) (id a (source y)) u v y (comp a u y)).
proof: Proof. ir. uf equalizer_cone. rw edge_nt_cone_create. tv. Qed.
imports: Arith colimits little_cat fc_limits cardinal