Lemma comm_comm_iso_id (A B C:category) : Precategories.nat_iso (bifunctor_comm A B C ∙ bifunctor_comm B A C) (functor_identity _). Proof. intros. unshelve refine (makeNatiso _ _). { intro F. { unshelve refine (makeNatiso _ _). { intro a. unshelve refine (makeNatiso _ _). { intro b. exact (identity_z_iso _). } { abstract (intros b b' f; simpl; rewrite id_right, id_left; reflexivity) using _L_. } } abstract (intros a a' f; apply nat_trans_eq; [ apply homset_property | intro b; simpl; now rewrite id_left, id_right]) using _M_. } } { abstract (intros F F' p; simpl; apply nat_trans_eq; [ exact (homset_property [B,C]) | intro a; apply nat_trans_eq; [ apply homset_property | intro b; simpl; now rewrite id_right, id_left]]) using _N_. } 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.