proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Projection UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Monoidal.Displayed.TransportLemmas UniMath.CategoryTheory.Monoidal.Structure.Symmetric