Definition bifunctor_comm (A B C:category) : [A,[B,C]] ⟶ [B,[A,C]]. Proof. exists (comm_functor_data_2 A B C). apply isfunctor_comm_functor_data_2. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.RepresentableFunctors.Precategories. Require Import UniMath.MoreFoundations.Tactics.