proposition: Lemma PhiUA_tau_nt_law : NT_law (F:=FunSET2_r AdjointUA) (G:=FunSET2_l G) PhiUA_tau.
proof: Proof. unfold NT_law, PhiUA_tau, PhiUA_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_l_ob in |- *. apply Trans with (UA_mor (UA_of (OB_l d2xc2)) o FMor G (FMor AdjointUA (HOM_l fxg) o h) o FMor G (Hom_r fxg)). apply Comp_l; apply FComp. apply Trans with ((UA_mor (UA_of (OB_l d2xc2)) o FMor G (FMor AdjointUA (HOM_l fxg) o h)) o FMor G (Hom_r fxg)). apply Ass. apply Comp_r. apply Trans with (UA_mor (UA_of (OB_l d2xc2)) o FMor G (FMor AdjointUA (HOM_l fxg)) o FMor G h). apply Comp_l; apply FComp. apply Trans with ((UA_mor (UA_of (OB_l d2xc2)) o FMor G (FMor AdjointUA (HOM_l fxg))) o FMor G h). apply Ass. apply Trans with ((HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))) o FMor G h). apply Comp_r; unfold FMor at 2 in |- *; simpl in |- *; unfold AdjointUA_mor, AdjointUA_ob in |- *. apply UA_diag. apply Ass1. Qed.
imports: Adj_UA