Definition comm_functor {I A B : category} : [I, [A, B] ] -> A -> [I,B]. Proof. intros D a. exists (comm_functor_data D a). exact (isfunctor_comm_functor_data D a). 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.