proposition: Lemma umorphism_cat_property : forall z, From_Arrows.property z umorphism_set Umorphism.compose Umorphism.identity.
proof: Proof. ir. uhg; ee; ir. rwi inc_umorphism_set H; ee. am. rwi inc_umorphism_set H; ee. am. rwi inc_umorphism_set H; ee. uh H; ee. uh H2. wr H2. uf Umorphism.create. rww Arrow.create_like. rwi inc_umorphism_set H2; rwi inc_umorphism_set H3; ee. rw inc_umorphism_set. ee. ap Umorphism.compose_strong_axioms. uhg; ee. uh H2; ee; am. uh H3; ee; am. rw H6. rww H5. rw Umorphism.source_compose. am. rww Umorphism.target_compose. rw inc_umorphism_set. ee. ap Umorphism.identity_strong_axioms. rww Umorphism.source_identity. rww Umorphism.target_identity. assert (a = source u). rwi inc_umorphism_set H1. ee; sy; am. rw H2. rww Umorphism.right_identity. rwi inc_umorphism_set H1. ee; am. assert (b = target u). rwi inc_umorphism_set H1. ee; sy; am. rw H2. rww Umorphism.left_identity. rwi inc_umorphism_set H1. ee; am. rwi inc_umorphism_set H3; rwi inc_umorphism_set H4; rwi inc_umorphism_set H5; ee. rww Umorphism.associativity. uhg; ee. lu. lu. rw H10; rww H9. uhg; ee. lu. lu. rw H8; rww H7. Qed.
imports: Arith ordinal nat_trans