proposition: Lemma Unit_nt_law : NT_law (F:=Id_CAT D) (G:=F o_F G) Unit_tau.
proof: Proof. unfold NT_law, Unit_tau in |- *; simpl in |- *. unfold Unit_arrow in |- *. unfold FMor at 1 2 in |- *; simpl in |- *. unfold Comp_FMor, Comp_FOb, Id_CAT_ob in |- *; intros d1 d2 f. apply Trans with (ApAphi ad (FMor F f o Id (F d2))). apply Sym; apply (Adj_eq4 ad f (Id (F d2))). apply Trans with (ApAphi ad (Id (F d1) o FMor F f)). apply AphiPres; apply Idrl. apply (Adj_eq3 ad (FMor F f) (Id (F d1))). Qed.
imports: IdCAT Adj_UA