proposition: Theorem left_adjoint_impl `(L : C ⟶ D) : ∀ R : D ⟶ C, L ⊣ R -> ∀ {E} (G : E ⟶ C) (H : E ⟶ D), [[[E,D]]](L ◯ G, H) ≊ [[[E,C]]](G, R ◯ H).
proof: Proof. intros. simpl. isomorphism; simpl. - construct. + transform. * intros. apply X; simpl. now apply X0. * simpl. rewrite <- to_adj_nat_l. rewrite <- to_adj_nat_r. now srewrite (@naturality _ _ _ _ X0 _ _ f). * simpl. rewrite <- to_adj_nat_l. rewrite <- to_adj_nat_r. now srewrite (@naturality _ _ _ _ X0 _ _ f). + simpl. proper. apply to_adj_respects. now apply X0. - construct. + transform. * intros. apply X; simpl. now apply X0. * simpl. rewrite <- from_adj_nat_l. rewrite <- from_adj_nat_r. now srewrite (@naturality _ _ _ _ X0 _ _ f). * simpl. rewrite <- from_adj_nat_l. rewrite <- from_adj_nat_r. now srewrite (@naturality _ _ _ _ X0 _ _ f). + simpl. proper. apply from_adj_respects. now apply X0. - simpl. now apply from_adj_comp_law. - simpl. now apply to_adj_comp_law. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Theory.Adjunction Category.Instance.Fun Category.Instance.Sets