proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat