proposition: Lemma Unit_and_CoUnit_law2 : Adj1_law2 Unit_NT CoUnit_NT.
proof: Proof. unfold Adj1_law2, Unit_NT, CoUnit_NT in |- *; simpl in |- *. unfold Unit_tau, CoUnit_tau in |- *; simpl in |- *. unfold Unit_arrow, CoUnit_arrow, Id_CAT_ob in |- *. intro d. apply Trans with (ApAphi_inv ad (ApAphi ad (Id (F d)) o Id (G (F d)))). apply Sym; apply (Adj_eq6 ad (ApAphi ad (Id (F d))) (Id (G (F d)))). apply Trans with (ApAphi_inv ad (ApAphi ad (Id (F d)))). apply Aphi_invPres; apply Idr1. apply (Idr_inv (NTa_areIso ad (Build_POb1 d (F d))) (Id (F d))). Qed.
imports: IdCAT Adj_UA