Lemma is_functor_Fun1 : is_functor Fun1_functor_data. Proof. split; [ intro F | intros F G H α β ]; use (nat_trans_eq has_homsets_HSET); intro X; use funextsec; intro f; [ set (idax := id_right f); rewrite <- (functor_id (exp (Yon c)) F) in idax; use idax | set (compax := assoc f (# (exp (Yon c)) α) (# (exp (Yon c)) β)); rewrite <- (functor_comp (exp (Yon c)) α β) in compax; use compax ]. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.YonedaBinproducts. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Presheaf.