Lemma form_adjunction_functor_cat_swap (C D : precategory) (E : category) : form_adjunction _ _ (id_functor_cat_swap C D E) (functor_cat_swap_id C D E). Proof. set (hsE := homset_property E). split; intro F. + apply (nat_trans_eq (functor_category_has_homsets _ _ hsE) (pr1 (pr1 (functor_cat_swap C D E) F)) (pr1 (pr1 (functor_cat_swap C D E) F))). now intro d; apply (nat_trans_eq hsE); intro c; apply id_right. + apply (nat_trans_eq (functor_category_has_homsets _ _ hsE) (pr1 (pr1 (functor_cat_swap D C E) F)) (pr1 (pr1 (functor_cat_swap D C E) F))). now intro d; apply (nat_trans_eq hsE); intro c; apply id_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.whiskering.