proposition: Lemma Adj_eq4 : ApAphi ad (FMor F h o f) =_S h o ApAphi ad f.
proof: Proof. apply Trans with (ApAphi ad ((FMor F h o f) o Id c)). apply AphiPres. apply Idr. apply Trans with ((h o ApAphi ad f) o FMor G (Id c)). apply (Adj_eq1 ad h (Id c) f). apply Trans with ((h o ApAphi ad f) o Id (G c)). apply Comp_l. apply FId. apply Idr1. Qed.
imports: NatIso HomFunctor2