Lemma functor_swap {C D : precategory} {E : category} : functor C [D,E] → functor D [C,E]. Proof. intros F. use tpair. - use tpair. + intro d; simpl. { use tpair. - use tpair. + intro c. apply (pr1 (F c) d). + intros a b f; apply (# F f). - abstract (split; [ now intro x; simpl; rewrite (functor_id F) | now intros a b c f g; simpl; rewrite (functor_comp F)]). } + intros a b f; simpl. { use tpair. - intros x; apply (# (pr1 (F x)) f). - abstract (intros c d g; simpl; apply pathsinv0, nat_trans_ax). } - abstract (split; [ intros d; apply (nat_trans_eq (homset_property E)); intro c; simpl; apply functor_id | intros a b c f g; apply (nat_trans_eq (homset_property E)); intro x; simpl; apply functor_comp]). 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.