Lemma reverse_three_args_idempotent {C D E : category} : functor_composite (reverse_three_args(C:=C)(D:=D)(E:=E))(reverse_three_args(C:=E)(D:=D)(E:=C)) = functor_identity _. Proof. apply functor_eq. - repeat (apply has_homsets_precategory_binproduct; try apply homset_property). - use functor_data_eq. + cbn. intro cde. apply idpath. + intros cde1 cde2 f. cbn. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat.