proposition: Lemma vident_twoarrow_functor : forall a u v, twoarrow_hypothesis a u v -> vident (twoarrow_functor a u v) = twoarrow_nt a u v u v (id a (source u)) (id a (target u)).
proof: Proof. ir. cp twoarrow_cat_axioms. cp (twoarrow_functor_axioms H). cp H; uh H; ee. assert (ob a (source u)). rww ob_source. assert (ob a (target u)). rww ob_target. assert (twoarrow_nt_hypothesis a u v u v (id a (source u)) (id a (target u))). uhg; ee. uh H; ee; am. am. am. am. am. app mor_id. app mor_id. rww source_id. rww target_id. rww source_id. rww target_id. am. am. am. am. rww left_id. rww right_id. rww left_id. rww right_id. sy; am. sy; am. ap Nat_Trans.axioms_extensionality. rww vident_axioms. ap twoarrow_nt_axioms. am. rww source_vident. rww source_twoarrow_nt. rww target_vident. rww target_twoarrow_nt. ir. rwi osource_vident H9. rwi source_twoarrow_functor H9. rw ntrans_vident. rww target_twoarrow_functor. rwi ob_twoarrow_cat_or H9. nin H9. rw H9. rw fob_twoarrow_functor_R. rw ntrans_twoarrow_nt_R. reflexivity. am. rw H9. rw fob_twoarrow_functor_R. rw ntrans_twoarrow_nt_R. reflexivity. am. rw source_twoarrow_functor. am. Qed.
imports: Arith cat_examples cardinal fc_limits