proposition: Lemma Teta_1_o_Teta : AreIsos (Teta dxc) (Teta_1 dxc).
proof: Proof. unfold AreIsos, RIso_law in |- *; split; simpl in |- *; unfold Ext in |- *; simpl in |- *. unfold Teta_arrow, Id_fun, Teta_1_arrow in |- *. unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_l_ob in |- *. intros f. apply Trans with (A_eta ad (OB_l dxc) o FMor G (FMor F f) o FMor G (A_eps ad (Ob_r dxc))). apply Comp_l. unfold Comp_Functor in |- *; simpl in |- *; unfold Comp_FOb in |- *; apply FComp. apply Trans with ((A_eta ad (OB_l dxc) o FMor G (FMor F f)) o FMor G (A_eps ad (Ob_r dxc))). apply Ass. apply Trans with ((f o A_eta ad (G (Ob_r dxc))) o FMor G (A_eps ad (Ob_r dxc))). apply Comp_r; apply Sym; apply (Prf_NT_law (A_eta ad) f). apply Trans with (f o A_eta ad (G (Ob_r dxc)) o FMor G (A_eps ad (Ob_r dxc))). apply Ass1. apply Trans with (f o Id (G (Ob_r dxc))). apply Comp_l; apply (Prf_Adj1_law1 ad (Ob_r dxc)). apply Idr1. unfold Teta_1_arrow, Teta_arrow, Id_fun in |- *. unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_r_ob in |- *; intro f. apply Trans with ((FMor F (A_eta ad (OB_l dxc)) o FMor F (FMor G f)) o A_eps ad (Ob_r dxc)). apply Comp_r; apply FComp. apply Trans with (FMor F (A_eta ad (OB_l dxc)) o FMor F (FMor G f) o A_eps ad (Ob_r dxc)). apply Ass1. apply Trans with (FMor F (A_eta ad (OB_l dxc)) o A_eps ad (F (OB_l dxc)) o f). apply Comp_l; apply (Prf_NT_law (A_eps ad) f). apply Trans with ((FMor F (A_eta ad (OB_l dxc)) o A_eps ad (F (OB_l dxc))) o f). apply Ass. apply Trans with (Id (F (OB_l dxc)) o f). apply Comp_r; apply (Prf_Adj1_law2 ad (OB_l dxc)). apply Idl. Qed.
imports: IdCAT Adj_UA