Lemma comm_comm_eq_id (A B C:category) : bifunctor_comm A B C ∙ bifunctor_comm B A C = functor_identity _.
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.