proposition: Lemma DCM_associator_law : disp_associator_law DCM_associator_data DCM_associatorinv_data.
proof: Proof. repeat split; try red; intros. - unfold DCM_associator_data. cbn. rewrite dispPostcompWithBinProductArrow. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. + rewrite id_right_disp. rewrite transport_b_b. etrans; [apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. rewrite dispBinProductPr1Commutes. apply transportf_comp_lemma. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. apply transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductOfArrowsPr1. apply transportf_comp_lemma. rewrite id_right_disp. rewrite transport_b_b. etrans; [| apply pathsinv0, mor_disp_transportf_postwhisker]. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. + etrans; [apply mor_disp_transportf_postwhisker |]. rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. rewrite transport_f_f. etrans; [apply maponpaths, mor_disp_transportf_prewhisker |]. rewrite transport_f_f. rewrite dispPrecompWithBinProductArrow. rewrite transport_f_b. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. * etrans; [ apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr1. rewrite id_right_disp. rewrite transport_b_b. apply transportf_comp_lemma. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. rewrite dispBinProductPr1Commutes. rewrite transport_f_b. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductOfArrowsPr1. rewrite id_right_disp. rewrite transport_b_b. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite transport_b_f. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. * etrans; [ apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr2. rewrite transport_f_b. apply transportf_comp_lemma. rewrite dispBinProductOfArrowsPr2. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. apply transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductPr2Commutes. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite transport_b_f. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - unfold DCM_associator_data. cbn. rewrite dispPostcompWithBinProductArrow. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. + rewrite dispPrecompWithBinProductArrow. rewrite transport_f_b. etrans; [ apply mor_disp_transportf_postwhisker |]. rewrite dispBinProductPr1Commutes. rewrite transport_f_b. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductOfArrowsPr1. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite transport_b_f. etrans. 2: { rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr1. rewrite transport_f_f. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. rewrite assoc_disp. rewrite transport_f_b. apply idpath. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. + etrans; [ apply mor_disp_transportf_postwhisker |]. rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. rewrite transport_f_f. etrans; [apply maponpaths, mor_disp_transportf_prewhisker |]. rewrite transport_f_f. rewrite dispPrecompWithBinProductArrow. rewrite transport_f_b. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. * rewrite id_right_disp. rewrite transport_f_b. etrans; [ apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite dispBinProductPr1Commutes. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductOfArrowsPr1. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite transport_b_f. apply transportf_comp_lemma. rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr2. rewrite id_right_disp. rewrite transport_b_b. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_prewhisker]. rewrite transport_f_f. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. * etrans; [ apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr2. rewrite transport_f_b. apply transportf_comp_lemma. rewrite id_left_disp. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. rewrite id_right_disp. rewrite transport_f_b. rewrite dispBinProductPr2Commutes. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - unfold DCM_associator_data. cbn. rewrite dispPostcompWithBinProductArrow. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. + rewrite dispPrecompWithBinProductArrow. rewrite transport_f_b. etrans; [ apply mor_disp_transportf_postwhisker |]. rewrite dispBinProductPr1Commutes. rewrite transport_f_b. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductOfArrowsPr1. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite transport_b_f. etrans. 2: { rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr1. rewrite transport_f_f. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. rewrite id_right_disp. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. apply idpath. } apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. rewrite id_right_disp. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. + etrans; [apply mor_disp_transportf_postwhisker |]. rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. rewrite transport_f_f. etrans; [apply maponpaths, mor_disp_transportf_prewhisker |]. rewrite transport_f_f. rewrite dispPrecompWithBinProductArrow. rewrite transport_f_b. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. * etrans; [apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr1. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_prewhisker]. rewrite transport_f_f. apply transportf_comp_lemma. etrans. 2: { rewrite assoc_disp. rewrite dispBinProductPr1Commutes. unfold transportb. rewrite mor_disp_transportf_postwhisker. rewrite transport_f_f. apply idpath. } apply pathsinv0, transportf_comp_lemma. etrans. 2: { rewrite assoc_disp. rewrite dispBinProductOfArrowsPr1. apply maponpaths. apply pathsinv0, mor_disp_transportf_postwhisker. } rewrite transport_b_f. etrans. 2: { rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr2. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. rewrite assoc_disp. rewrite transport_f_f. rewrite transport_f_b. apply idpath. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. * etrans; [apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp_var. do 2 rewrite dispBinProductOfArrowsPr2. rewrite transport_f_b. rewrite id_right_disp. rewrite transport_f_b. apply transportf_comp_lemma. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. rewrite id_right_disp. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_prewhisker]. rewrite dispBinProductPr2Commutes. rewrite transport_f_f. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - unfold DCM_associator_data, DCM_associatorinv_data. cbn. etrans. { apply pathsinv0. simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). + change (αinv^{M}_{ x, y, z} · α^{M}_{ x, y, z} · BinProductPr1 C (CP x (y ⊗_{M} z)) = BinProductPr1 C (CP x (y ⊗_{M} z))). cbn. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. apply BinProductPr1Commutes. + rewrite assoc_disp_var. rewrite dispBinProductPr1Commutes. etrans; [apply maponpaths, mor_disp_transportf_prewhisker |]. rewrite transport_f_f. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductPr1Commutes. unfold transportb. rewrite mor_disp_transportf_postwhisker. rewrite dispBinProductPr1Commutes. rewrite transport_f_f. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. + change( αinv^{M}_{ x, y, z} · α^{M}_{ x, y, z} · BinProductPr2 C (CP x (y ⊗_{M} z)) = BinProductPr2 C (CP x (y ⊗_{M} z))). cbn. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite precompWithBinProductArrow. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr1Commutes. rewrite BinProductPr2Commutes. apply pathsinv0, BinProductArrowUnique; apply idpath. + rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. etrans; [apply maponpaths, mor_disp_transportf_prewhisker |]. rewrite transport_f_f. apply pathsinv0, transportf_comp_lemma. rewrite dispPrecompWithBinProductArrow. apply transportf_comp_lemma. apply dispBinProductArrowUnique. * etrans; [apply mor_disp_transportf_postwhisker |]. apply transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductPr1Commutes. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite dispBinProductPr2Commutes. rewrite transport_b_f. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. * etrans; [apply mor_disp_transportf_postwhisker |]. apply transportf_comp_lemma. rewrite dispBinProductPr2Commutes. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - unfold DCM_associator_data, DCM_associatorinv_data. cbn. etrans. { apply pathsinv0. simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). + change (α^{M}_{ x, y, z} · αinv^{M}_{ x, y, z} · BinProductPr1 C (CP (x ⊗_{M} y) z) = BinProductPr1 C (CP (x ⊗_{M} y) z)). cbn. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite precompWithBinProductArrow. apply pathsinv0, BinProductArrowUnique. * apply pathsinv0, BinProductPr1Commutes. * rewrite assoc. rewrite BinProductPr2Commutes. apply pathsinv0, BinProductPr1Commutes. + rewrite assoc_disp_var. rewrite dispBinProductPr1Commutes. apply pathsinv0, transportf_comp_lemma. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. rewrite dispPrecompWithBinProductArrow. rewrite transport_f_b. apply transportf_comp_lemma. apply dispBinProductArrowUnique. * etrans; [apply mor_disp_transportf_postwhisker |]. apply transportf_comp_lemma. rewrite dispBinProductPr1Commutes. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. * etrans; [apply mor_disp_transportf_postwhisker |]. apply transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductPr2Commutes. etrans; [| apply maponpaths, pathsinv0, mor_disp_transportf_postwhisker]. rewrite dispBinProductPr1Commutes. rewrite transport_b_f. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. + change (α^{M}_{ x, y, z} · αinv^{M}_{ x, y, z} · BinProductPr2 C (CP (x ⊗_{M} y) z) = BinProductPr2 C (CP (x ⊗_{M} y) z)). cbn. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. apply BinProductPr2Commutes. + rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. etrans; [apply maponpaths, mor_disp_transportf_prewhisker |]. rewrite transport_f_f. apply pathsinv0, transportf_comp_lemma. rewrite assoc_disp. rewrite dispBinProductPr2Commutes. unfold transportb. rewrite mor_disp_transportf_postwhisker. rewrite dispBinProductPr2Commutes. rewrite transport_f_f. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Binproducts UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal