proposition: Lemma is_finite_twoarrow_cat : is_finite_cat twoarrow_cat.
proof: Proof. uf twoarrow_cat. ap is_finite_catyd. ap twoarrow_data_property. exact (is_finite_ta_obs). exact (is_finite_ta_maps). Qed.
imports: Arith cat_examples cardinal fc_limits