Definition functor_cat_swap_id (C D : precategory) (E : category) : nat_trans (functor_composite (functor_cat_swap D C E) (functor_cat_swap C D E)) (functor_identity [D,[C,E]]). Proof. set (hsE := homset_property E). use tpair. + intros F. use tpair. - intro c. use tpair. * now intro f; apply identity. * abstract (now intros a b f; rewrite id_left, id_right). - abstract (now intros a b f; apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right). + abstract (now intros a b f; apply nat_trans_eq; [apply functor_category_has_homsets|]; intro c; apply (nat_trans_eq hsE); intro d; simpl; rewrite id_left, id_right). 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.