proposition: Lemma edge_equalizer_cone_R : forall a u v y (x:obsy twoarrow_data), edge (equalizer_cone a u v y) (R x) = match x with o1 => y | o2 => (comp a u y) end.
proof: Proof. ir. uf edge. rw edge_nt_equalizer_cone. rw ntrans_twoarrow_nt_R. tv. Qed.
imports: Arith colimits little_cat fc_limits cardinal