proposition: Lemma Unit_UAlaw2 : UA_law2 Unit_arrow Unit_arrow_diese.
proof: Proof. unfold UA_law2, UA_eq, Unit_arrow_diese, Unit_arrow in |- *. intros c1 f f' H. apply Trans with (ApAphi_inv ad (ApAphi ad (Id (F d)) o FMor G f')). apply Sym. apply Trans with (ApAphi_inv ad (ApAphi ad (Id (F d))) o f'). apply (Adj_eq5 ad f' (ApAphi ad (Id (F d)))). apply Trans with (Id (F d) o f'). apply Comp_r; apply (Idr_inv (NTa_areIso ad (Build_POb1 d (F d))) (Id (F d))). apply Idl. apply Aphi_invPres; apply H. Qed.
imports: CoUniversalArrow Adjunction