Lemma make_disp_symm_braiding_nat_left {B : symmetric M} {c : disp_braiding_data DM B} (p_nat : disp_sym_moncat_laws_tensored_nat c) : disp_braiding_law_naturality_left DM c. Proof. intro ; intros. use precomp_disp_id_left_inj. set (q := transportb_transpose_right (p_nat _ _ _ _ _ _ xx xx yy1 yy2 (id_disp xx) gg)). unfold dispfunctoronmorphisms1 in q. set (tq := assoc_disp_var (id_disp xx ⊗⊗^{ DM}_{r} yy1) (xx ⊗⊗^{ DM}_{l} gg) (c x y2 xx yy2)) in q. set (q' := transportb_transpose_right (! tq @ q)). rewrite disp_bifunctor_rightid in q'. unfold transportb in q'. rewrite (mor_disp_transportf_postwhisker _ (id_disp (xx ⊗⊗_{ DM} yy1))) in q'. set (q'' := transportb_transpose_right q'). refine (_ @ ! q''). clear q'' q' tq q. unfold transportb. rewrite ! transport_f_f. etrans. 2: { apply maponpaths. apply pathsinv0, assoc_disp. } unfold transportb. rewrite transport_f_f. rewrite mor_disp_transportf_prewhisker. use transportf_transpose_right. unfold transportb. rewrite transport_f_f. rewrite id_left_disp. unfold transportb. rewrite transport_f_f. rewrite disp_bifunctor_leftid. unfold transportb. rewrite ! mor_disp_transportf_prewhisker. use transportf_transpose_right. unfold transportb. rewrite transport_f_f. rewrite id_right_disp. use transportf_transpose_right. unfold transportb. rewrite transport_f_f. use transportf_set. apply homset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TransportLemmas. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations. Import DisplayedMonoidalNotations.