proposition: Lemma CoUnit_coUAlaw2 : CoUA_law2 CoUnit_arrow CoUnit_arrow_diese.
proof: Proof. unfold CoUA_law2, CoUA_eq, CoUnit_arrow_diese, CoUnit_arrow in |- *. intros d1 f g H. apply Trans with (ApAphi ad (FMor F g o ApAphi_inv ad (Id (G c)))). apply Trans with (g o ApAphi ad (ApAphi_inv ad (Id (G c)))). apply Trans with (g o Id (G c)). apply Idr. apply Comp_l; apply Sym. apply (Idl_inv (NTa_areIso ad (Build_POb1 (G c) c)) (Id (G c))). apply Sym; apply (Adj_eq4 ad g (ApAphi_inv ad (Id (G c)))). apply AphiPres; apply H. Qed.
imports: CoUniversalArrow Adjunction