Definition comm_functor_data_2 (I A B:category) : functor_data [I,[A,B]] [A,[I,B]]. Proof. unshelve refine (_,,_). { intros D. unshelve refine (_,,_). { unshelve refine (_,,_). { intros a. exact (comm_functor D a). } intros a a' f; simpl. unshelve refine (_,,_). { simpl; intro i. exact (D ◾ i ▭ f). } { intros i j r; simpl; eqn_logic. } } { split; [ intros a; simpl; apply nat_trans_eq; [ apply homset_property | intros i; simpl; apply functor_id ] | intros a b g r s; simpl; apply nat_trans_eq; [ apply homset_property | simpl; intros i; apply functor_comp ] ]. } } { intros D D' p. simpl. unshelve refine (_,,_). { intros a. simpl. unshelve refine (_,,_). { exact (λ i, p ◽ i ◽ a). } { exact (λ i j e, maponpaths (λ v, v ◽ a) (nat_trans_ax p _ _ e)). } } { intros a b f; apply nat_trans_eq; [ apply homset_property | intros i; simpl; apply nat_trans_ax]. } } 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.