proposition: Lemma is_finite_catyd : forall (d:cat_type_data), catyd_property d -> is_finite (obsy d) -> is_finite (morsy d) -> is_finite_cat (catyd d).
proof: Proof. ir. uhg. ee. app catyd_axioms. rww objects_catyd. ap finite_invariant. sh (morsy d). ee. ap are_isomorphic_morphisms_catyd. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits