proposition: Lemma functor_swap {C D : precategory} {E : category} : functor C [D,E] → functor D [C,E].
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Adjunctions.Core