Lemma DCM_associator_law : disp_associator_law DCM_associator_data DCM_associatorinv_data. 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.
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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations.