proposition: Lemma fob_twoarrow_functor_R : forall a u v (x:obsy twoarrow_data), twoarrow_hypothesis a u v -> fob (twoarrow_functor a u v) (R x) = match x with o1 => (source u) | o2 => (target u) end.
proof: Proof. ir. cp (twoarrow_fun_data_property H). uf twoarrow_functor. nin x; rww fob_funtyd_R. Qed.
imports: Arith cat_examples cardinal fc_limits