proposition: Lemma CoUnit_coUAlaw1 : CoUA_law1 CoUnit_arrow CoUnit_arrow_diese.
proof: Proof. unfold CoUA_law1, CoUA_eq, CoUnit_arrow_diese, CoUnit_arrow in |- *. intros d1 f. apply Trans with (ApAphi_inv ad (ApAphi ad f o Id (G c))). apply Sym; apply (Adj_eq6 ad (ApAphi ad f) (Id (G c))). apply Trans with (ApAphi_inv ad (ApAphi ad f)). apply Aphi_invPres; apply Idr1. apply (Idr_inv (NTa_areIso ad (Build_POb1 d1 c)) f). Qed.
imports: CoUniversalArrow Adjunction