proposition: Lemma PhiUA_1_tau_nt_law : NT_law (F:=FunSET2_l G) (G:=FunSET2_r AdjointUA) PhiUA_1_tau.
proof: Proof. unfold NT_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. intros d1xc1 d2xc2 fxg h. unfold PhiUA_1_arrow, FunSET2_r_mor1 in |- *. unfold FMor at 1 in |- *; simpl in |- *. unfold AdjointUA_mor, FunSET2_r_ob in |- *; simpl in |- *; unfold AdjointUA_ob in |- *. apply UA_unic1. apply Trans with (UA_mor (UA_of (OB_l d2xc2)) o FMor G (UA_diese (UA_of (OB_l d2xc2)) (HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))) o UA_diese (UA_of (OB_l d1xc1)) 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 (UA_diese (UA_of (OB_l d2xc2)) (HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))) o UA_diese (UA_of (OB_l d1xc1)) h)) o FMor G (Hom_r fxg)). apply Ass. apply Trans with ((UA_mor (UA_of (OB_l d2xc2)) o FMor G (UA_diese (UA_of (OB_l d2xc2)) (HOM_l fxg o UA_mor (UA_of (OB_l d1xc1)))) o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)) o FMor G (Hom_r fxg)). apply Comp_r; apply Comp_l; apply FComp. apply Trans with (((UA_mor (UA_of (OB_l d2xc2)) o FMor G (UA_diese (UA_of (OB_l d2xc2)) (HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))))) o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)) o FMor G (Hom_r fxg)). apply Comp_r; apply Ass. apply Trans with (((HOM_l fxg o UA_mor (UA_of (OB_l d1xc1))) o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)) o FMor G (Hom_r fxg)). apply Comp_r; apply Comp_r; apply UA_diag. unfold FunSET2_l_mor1 in |- *; apply Comp_r. apply Trans with (HOM_l fxg o UA_mor (UA_of (OB_l d1xc1)) o FMor G (UA_diese (UA_of (OB_l d1xc1)) h)). apply Ass1. apply Comp_l; apply UA_diag. Qed.
imports: Adj_UA