Definition reverse_three_args {C D E : category} : ((C × D) × E) ⟶ ((E × D) × C). Proof. use (functor_composite (precategory_binproduct_unassoc _ _ _)). use (functor_composite binswap_pair_functor). exact (pair_functor binswap_pair_functor (functor_identity _)). Defined.
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.