proposition: Lemma Teta_1_tau_NT_law : NT_law (F:=FunSET2_l G) (G:=FunSET2_r F) Teta_1_tau.
proof: Proof. unfold NT_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. intros d1xc1 d2xc2 fxg h. unfold Teta_1_arrow, 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 h) o FMor F (FMor G (Hom_r fxg))) o A_eps ad (Ob_r d2xc2)). apply Comp_r; apply FComp. apply Trans with (FMor F (HOM_l fxg o h) o FMor F (FMor G (Hom_r fxg)) o A_eps ad (Ob_r d2xc2)). apply Ass1. apply Trans with ((FMor F (HOM_l fxg) o FMor F h) o FMor F (FMor G (Hom_r fxg)) o A_eps ad (Ob_r d2xc2)). apply Comp_r; apply FComp. apply Trans with (FMor F (HOM_l fxg) o FMor F h o FMor F (FMor G (Hom_r fxg)) o A_eps ad (Ob_r d2xc2)). apply Ass1. apply Trans with (FMor F (HOM_l fxg) o (FMor F h o A_eps ad (Ob_r d1xc1)) o Hom_r fxg). apply Comp_l. apply Trans with (FMor F h o A_eps ad (Ob_r d1xc1) o Hom_r fxg). apply Comp_l; apply (Prf_NT_law (A_eps ad) (Hom_r fxg)). apply Ass. apply Ass. Qed.
imports: IdCAT Adj_UA