proposition: 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: 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.
imports: UniMath.Foundations.Preamble UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.RepresentableFunctors.Precategories UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core