proposition: Lemma from_arrows_axioms : Category.axioms from_arrows.
proof: Proof. uhg; ee; ir. ap iff_eq; ir. uhg; ee. am. app is_mor_id_from_arrows. rww source_id_from_arrows. rww target_id_from_arrows. ir. wr H1. rww right_id_from_arrows. ir. wr H1. rww left_id_from_arrows. uh H; ee; am. ap iff_eq; ir. uhg; ee. am. rwi is_mor_from_arrows H. ee; am. rwi is_mor_from_arrows H. ee; am. rww left_id_from_arrows. rww right_id_from_arrows. rwi is_mor_from_arrows H; ee. cp property_hyp. uh H2; ee. exact (H4 _ _ _ H1). uh H; ee; am. ap iff_eq; ir. assert (lema : are_composable from_arrows u v). am. uh H; ee. rwi is_mor_from_arrows H. rwi is_mor_from_arrows H0. ee. cp property_hyp. uh H6; ee. util (H9 (source v) (source u) (target u) u v). wrr is_ob_from_arrows. wrr is_ob_from_arrows. wrr is_ob_from_arrows. am. rww H1. util (inc_homs_source (a:= (source v)) (u:= (comps u v))). am. sh (target u). ee; am. util (inc_homs_target (a:= (target u)) (u:= (comps u v))). am. sh (source v). ee; am. assert (is_mor from_arrows u). rw is_mor_from_arrows; ee; am. assert (is_mor from_arrows v). rw is_mor_from_arrows; ee; am. uhg; ee. am. rw is_mor_from_arrows; ee. rw is_ob_from_arrows. rww comp_from_arrows. rw H15. wrr is_ob_from_arrows. rww comp_from_arrows. rw H16. am. rww comp_from_arrows. rw H15. rw H16. am. rww comp_from_arrows. rww comp_from_arrows. uh H; ee; am. uh H; uh H0; ee. cp H; cp H3; cp H1. rwi is_mor_from_arrows H5; rwi is_mor_from_arrows H6; rwi is_mor_from_arrows H7; ee. cp property_hyp. uh H14; ee. util (H17 (source v) (source u) (target u) u v). wrr is_ob_from_arrows. wrr is_ob_from_arrows. wrr is_ob_from_arrows. am. rww H4. util (H17 (source w) (source v) (source u) v w). wrr is_ob_from_arrows. wrr is_ob_from_arrows. wrr is_ob_from_arrows. rww H4. rww H2. sy. rww comp_from_arrows. rww comp_from_arrows. rww comp_from_arrows. rww comp_from_arrows. apply H21 with (source w) (source v) (source u) (target u). wrr is_ob_from_arrows. wrr is_ob_from_arrows. wrr is_ob_from_arrows. wrr is_ob_from_arrows. am. rww H4. rww H2. rww comp_from_arrows. ap inc_homs_is_mor. sh (source v). sh (target u). ee. wrr is_ob_from_arrows. wrr is_ob_from_arrows. am. ap inc_homs_source. am. sh (target u). ee; try am. wrr H2. rww comp_from_arrows. rww comp_from_arrows. ap inc_homs_is_mor. sh (source w); sh (source u). ee. wrr is_ob_from_arrows. wrr is_ob_from_arrows. am. sy; ap inc_homs_target. am. sh (source w). ee; try am. rww comp_from_arrows. uf from_arrows. ap Notations.create_like. Qed.
imports: Arith ordinal nat_trans