proposition: Lemma function_cat_property : forall z, From_Arrows.property z function_arrow_set fa_comp fa_id.
proof: Proof. ir. uhg; ee; ir. rwi inc_function_arrow_set H. ee; am. rwi inc_function_arrow_set H. ee; am. rwi inc_function_arrow_set H. ee; am. rwi inc_function_arrow_set H2. rwi inc_function_arrow_set H3. ee. rw inc_function_arrow_set. ee. uf fa_comp. rww Arrow.create_like. rww source_fa_comp. rww target_fa_comp. rw arrow_fa_comp. ap Function.compose_axioms. assert (Map.axioms a c (arrow (fa_comp u v))). rw arrow_fa_comp. apply Map.compose_axioms with b. am. am. uh H16; ee. am. assert (Map.axioms a c (arrow (fa_comp u v))). rw arrow_fa_comp. apply Map.compose_axioms with b. am. am. uh H16; ee. am. rw arrow_fa_comp. apply Map.compose_axioms with b. am. am. assert (Map.axioms a a (arrow (fa_id a))). rw arrow_fa_id. ap Map.identity_axioms. rw inc_function_arrow_set. ee. uf fa_id. rww Arrow.create_like. rww source_fa_id. rww target_fa_id. uh H0; ee. am. uh H0; ee; am. uh H0; ee; am. am. cp H1. rwi inc_function_arrow_set H2; ee. ap fa_extensionality. ap inc_fas_fa_comp. rw H3; rww H4. rw source_fa_id. rw target_fa_id. ap inc_fas_fa_id. rww target_fa_id. rww source_fa_comp. rww target_fa_comp. rw H3; rww H4. rw source_fa_comp. rww source_fa_id. sy; am. rww target_fa_comp. assert (inc (fa_comp u (fa_id a)) (function_arrow_set (source u) (target u))). ap inc_fas_fa_comp. rw H3; rww H4. rw source_fa_id. rw target_fa_id. ap inc_fas_fa_id. rww target_fa_id. rww source_fa_id. tv. cp H9. rwi inc_function_arrow_set H10; ee. ir. rw arrow_fa_comp. rw arrow_fa_id. rw compose_ev. uf Function.identity. rw create_V_rewrite. tv. rwi source_fa_comp H17. rwi source_fa_id H17. am. rwi source_fa_comp H17. rwi source_fa_id H17. rwi arrow_fa_comp H14. rwi arrow_fa_id H14. rw H14. rww H3. cp H1. rwi inc_function_arrow_set H2. ee. assert (inc (fa_comp (fa_id b) u) (function_arrow_set (source u) (target u))). ap inc_fas_fa_comp. rw source_fa_id. rw target_fa_id. ap inc_fas_fa_id. rw H3; rww H4. rw source_fa_id. sy; am. tv. rw target_fa_id. am. cp H9. rwi inc_function_arrow_set H10; ee. ap fa_extensionality. rw source_fa_comp. rw target_fa_comp. rw target_fa_id. ap inc_fas_fa_comp. rw source_fa_id. rw target_fa_id. ap inc_fas_fa_id. rw H3; rww H4. rww source_fa_id. sy; am. tv. sy; rww target_fa_id. rw H3; rww H4. rww source_fa_comp. rw target_fa_comp. rw target_fa_id. sy; am. ir. rw arrow_fa_comp. rw arrow_fa_id. rw compose_ev. uf Function.identity. rw create_V_rewrite. tv. rwi source_fa_comp H17. wr H4. ap map_V_inc. sh a. ee. rww H4. wrr H3. wr arrow_fa_id. wr arrow_fa_comp. rw H14. rwi source_fa_comp H17. am. cp H3; cp H4; cp H5. rwi inc_function_arrow_set H6. rwi inc_function_arrow_set H7. rwi inc_function_arrow_set H8. ee. wri H21 H3; wri H22 H3. wri H15 H4; wri H16 H4. wri H9 H5; wri H10 H5. assert (source u = target v). rw H21; rww H16. assert (source v = target w). rw H15; rww H10. assert (inc (fa_comp v w) (function_arrow_set a c)). app inc_fas_fa_comp. sy; am. sy; am. assert (inc (fa_comp u v) (function_arrow_set b d)). app inc_fas_fa_comp. sy; am. sy; am. ap fa_extensionality. ap inc_fas_fa_comp. am. app inc_fas_fa_comp. rww source_fa_comp. rww target_fa_comp. rww target_fa_comp. rw source_fa_comp. tv. rw target_fa_comp. tv. ap inc_fas_fa_comp. ap inc_fas_fa_comp. am. am. am. rww source_fa_comp. rww target_fa_comp. am. rww source_fa_comp. rww source_fa_comp. rww target_fa_comp. rw source_fa_comp. rw source_fa_comp. rw source_fa_comp. tv. rw target_fa_comp. rw target_fa_comp. rw target_fa_comp. tv. ir. rw V_fa_comp. rw V_fa_comp. rw V_fa_comp. rw V_fa_comp. tv. am. am. am. uh H14; ee. rw H15. ap H33. ap range_inc. am. sh x. ee. rwi source_fa_comp H31. rwi source_fa_comp H31. rw H12. wrr H9. tv. rw source_fa_comp. rw target_fa_comp. rw H15. rww H22. am. rww source_fa_comp. rwi source_fa_comp H31. rwi source_fa_comp H31. am. am. am. am. rwi source_fa_comp H31. rwi source_fa_comp H31. am. am. rw source_fa_comp. rw target_fa_comp. rw H9; rww H16. rww target_fa_comp. rwi source_fa_comp H31. am. Qed.
imports: Arith ordinal nat_trans