proposition: Lemma CoUnit_nt_law : NT_law (F:=G o_F F) (G:=Id_CAT C) CoUnit_tau.
proof: Proof. unfold NT_law, CoUnit_tau in |- *; simpl in |- *. unfold CoUnit_arrow in |- *. unfold FMor at 1 2 in |- *; simpl in |- *. unfold Comp_FMor, Comp_FOb, Id_CAT_ob in |- *. intros c1 c2 f. apply Trans with (ApAphi_inv ad (FMor G f o Id (G c2))). apply Sym; apply (Adj_eq6 ad (FMor G f) (Id (G c2))). apply Trans with (ApAphi_inv ad (Id (G c1) o FMor G f)). apply Aphi_invPres; apply Idrl. apply (Adj_eq5 ad f (Id (G c1))). Qed.
imports: IdCAT Adj_UA