proposition: Lemma Unit_and_CoUnit_law1 : Adj1_law1 Unit_NT CoUnit_NT.
proof: Proof. unfold Adj1_law1, 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 c. apply Trans with (ApAphi ad (Id (F (G c)) o ApAphi_inv ad (Id (G c)))). apply Sym; apply (Adj_eq3 ad (ApAphi_inv ad (Id (G c))) (Id (F (G c)))). apply Trans with (ApAphi ad (ApAphi_inv ad (Id (G c)))). apply AphiPres; apply Idl. apply (Idl_inv (NTa_areIso ad (Build_POb1 (G c) c)) (Id (G c))). Qed.
imports: IdCAT Adj_UA