proposition: Lemma are_isomorphic_morphisms_catyd : forall (d:cat_type_data), catyd_property d -> are_isomorphic (morsy d) (morphisms (catyd d)).
proof: Proof. ir. uhg. sh (Function.tcreate (fun y :morsy d => catyd_arrow y)). uhg; dj. uhg; ee. ap tcreate_axioms. rww domain_tcreate. uhg; ir. rwi range_inc_rw H0. nin H0. ee. rwi domain_tcreate H0. assert (x0 = R (B H0)). rww B_eq. rwi H2 H1. rwi tcreate_value_type H1. rw H1. change (is_mor (catyd d) (catyd_arrow (B H0))). ap mor_is_mor. ap mor_catyd_catyd_arrow. am. ap tcreate_axioms. uhg; ee. am. uhg. ir. sh (arrow x). ee. assert (mor (catyd d) x). ap is_mor_mor. app catyd_axioms. am. rwi mor_catyd H2. nin H2. rw H2. rw arrow_catyd_arrow. ap R_inc. am. assert (mor (catyd d) x). ap is_mor_mor. app catyd_axioms. am. rwi mor_catyd H2. nin H2. rw H2. rw arrow_catyd_arrow. rw tcreate_value_type. tv. am. uhg. ee; try am. uhg. ir. cp (B_eq H2). cp (B_eq H3). wri H5 H4. wri H6 H4. rwi tcreate_value_type H4. rwi tcreate_value_type H4. transitivity (arrow (catyd_arrow (B H2))). rww arrow_catyd_arrow. sy; am. rw H4. rw arrow_catyd_arrow. am. Qed.
imports: Arith cat_examples cardinal fc_limits