Lemma are_adjoint_functor_cat_swap (C D : precategory) (E : category) : are_adjoints (@functor_cat_swap C D E) (@functor_cat_swap D C E). Proof. use tpair. - split; [ apply id_functor_cat_swap | apply functor_cat_swap_id ]. - apply form_adjunction_functor_cat_swap. Defined.
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.