proposition: Lemma Adj_eq5 : ApAphi_inv ad (g o FMor G k) =_S ApAphi_inv ad g o k.
proof: Proof. apply Trans with (ApAphi_inv ad ((Id d o g) o FMor G k)). apply Aphi_invPres. apply Comp_r. apply Idl1. apply Trans with ((FMor F (Id d) o ApAphi_inv ad g) o k). apply (Adj_eq2 ad (Id d) k g). apply Comp_r. apply Trans with (Id (F d) o ApAphi_inv ad g). apply Comp_r. apply FId. apply Idl. Qed.
imports: NatIso HomFunctor2