proposition: Lemma PsiUA_1_tau_nt_law : NT_law (F:=FunSET2_l CoadjointUA) (G:=FunSET2_r F) PsiUA_1_tau.
proof: Proof. unfold NT_law, PsiUA_1_tau, PsiUA_1_arrow in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. intros d1xc1 d2xc2 fxg h. unfold FunSET2_r_mor1, FunSET2_l_mor1 in |- *. unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_r_ob in |- *. apply Trans with (((FMor F (HOM_l fxg) o FMor F h) o FMor F (FMor CoadjointUA (Hom_r fxg))) o CoUA_mor (UA_of (Ob_r d2xc2))). apply Comp_r. apply Trans with (FMor F (HOM_l fxg o h) o FMor F (FMor CoadjointUA (Hom_r fxg))). apply FComp. apply Comp_r; apply FComp. apply Trans with ((FMor F (HOM_l fxg) o FMor F h) o FMor F (FMor CoadjointUA (Hom_r fxg)) o CoUA_mor (UA_of (Ob_r d2xc2))). apply Ass1. apply Trans with (FMor F (HOM_l fxg) o FMor F h o FMor F (FMor CoadjointUA (Hom_r fxg)) o CoUA_mor (UA_of (Ob_r d2xc2))). apply Ass1. apply Trans with (FMor F (HOM_l fxg) o (FMor F h o CoUA_mor (UA_of (Ob_r d1xc1))) o Hom_r fxg). apply Comp_l. apply Trans with (FMor F h o CoUA_mor (UA_of (Ob_r d1xc1)) o Hom_r fxg). apply Comp_l. unfold FMor at 2 in |- *; simpl in |- *; unfold CoadjointUA_mor, CoadjointUA_ob in |- *. apply CoUA_diag. apply Ass. apply Ass. Qed.
imports: Adj_UA