proposition: Lemma hcompose_vee_nt2 : 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) (fmor (target u) r) (ntrans u (source u1)) ) (comp (otarget u) (fmor (target u) s) (ntrans u (target u1)) ) (comp (otarget u) (fmor (target u) t) (ntrans u (source v1)) ).
proof: Proof. ir. rw Nat_Trans.hcompose_other. uf hcompose1. rw source_vee_nt. util (htrans_right_vee_functor (y:=u) (a:=a) (u:=u1) (v:=v1)). 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:=target u)). am. rww functor_axioms_target. rww source_target. rw H3. rw target_target. rw vcompose_vee_nt. reflexivity. wr target_target. ap vee_nt_hypothesis_for_htrans_left. rw source_target. rw H1. am. am. rww functor_axioms_target. ap vee_nt_hypothesis_for_htrans_right. am. rw H1. uh H; uhg; xd. tv. tv. uhg. ee. am. app vee_nt_axioms. rww otarget_vee_nt. Qed.
imports: Arith cat_examples cardinal fc_limits