proposition: Lemma Teta_tau_NT_law : NT_law (F:=FunSET2_r F) (G:=FunSET2_l G) Teta_tau.
proof: Proof. unfold NT_law, Teta_tau, Teta_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 (A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg) o h) o FMor G (Hom_r fxg)). apply Comp_l; unfold FOb at 1 in |- *; simpl in |- *; unfold Comp_FOb in |- *; apply FComp. apply Trans with ((A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg) o h)) o FMor G (Hom_r fxg)). apply Ass. apply Comp_r. apply Trans with (A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg)) o FMor G h). apply Comp_l. unfold FOb at 1 in |- *; simpl in |- *; unfold Comp_FOb in |- *; apply FComp. apply Trans with ((A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg))) o FMor G h). apply Ass. apply Trans with ((HOM_l fxg o A_eta ad (OB_l d1xc1)) o FMor G h). apply Comp_r; apply Sym. apply (Prf_NT_law (A_eta ad) (HOM_l fxg)). apply Ass1. Qed.
imports: IdCAT Adj_UA