proposition: Lemma vident_vee_functor : forall a u v, vee_hypothesis a u v -> vident (vee_functor a u v) = vee_nt a u v u v (id a (source u)) (id a (target u)) (id a (source v)).
proof: Proof. ir. cp vee_cat_axioms. cp (vee_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 (ob a (source v)). rww ob_source. assert (vee_nt_hypothesis a u v u v (id a (source u)) (id a (target u)) (id a (source v))). uhg; ee. uh H; ee; am. am. am. am. am. app mor_id. app mor_id. app mor_id. rww source_id. rww target_id. rww source_id. rww target_id. rww source_id. rww target_id. am. am. rww left_id. rww right_id. rww left_id. rww right_id. sy; am. ap Nat_Trans.axioms_extensionality. rww vident_axioms. ap vee_nt_axioms. am. rww source_vident. rww source_vee_nt. rww target_vident. rww target_vee_nt. ir. rwi osource_vident H9. rwi source_vee_functor H9. rw ntrans_vident. rww target_vee_functor. rwi ob_vee_cat_ex H9. nin H9. nin x0. rw H9. rw fob_vee_functor_R. rw ntrans_vee_nt_R. reflexivity. am. rw H9. rw fob_vee_functor_R. rw ntrans_vee_nt_R. reflexivity. am. rw H9. rw fob_vee_functor_R. rw ntrans_vee_nt_R. reflexivity. am. rw source_vee_functor. am. Qed.
imports: Arith cat_examples cardinal fc_limits