proposition: Lemma hcompose_vee_nt1 : forall u a u1 v1 u2 v2 r s t, vee_nt_hypothesis a u1 v1 u2 v2 r s t -> Nat_Trans.axioms u -> osource u = a -> hcompose u (vee_nt a u1 v1 u2 v2 r s t) = vee_nt (otarget u) (fmor (source u) u1) (fmor (source u) v1) (fmor (target u) u2) (fmor (target u) v2) (comp (otarget u) (ntrans u (source u2)) (fmor (source u) r)) (comp (otarget u) (ntrans u (target u2)) (fmor (source u) s)) (comp (otarget u) (ntrans u (source v2)) (fmor (source u) t)).
proof: Proof. ir. uf hcompose. rw target_vee_nt. util (htrans_right_vee_functor (y:=u) (a:=a) (u:=u2) (v:=v2)). am. uh H; uhg; xd. am. rw H2. util (htrans_left_vee_nt (a:=a) (u1:=u1) (v1:=v1) (u2:=u2) (v2:=v2) (r:=r) (s:=s) (t:=t) (f:=source u)). am. rww functor_axioms_source. am. rw H3. rw target_source. rw vcompose_vee_nt. reflexivity. ap vee_nt_hypothesis_for_htrans_right. am. rw H1. uh H; uhg; xd. wr target_source. ap vee_nt_hypothesis_for_htrans_left. rw source_source; rw H1. am. rww functor_axioms_source. am. tv. tv. am. Qed.
imports: Arith cat_examples cardinal fc_limits