proposition: Lemma disp_assoc_axioms : disp_functor_axioms disp_assoc_data.
proof: Proof. split. - intros x xx. cbn. apply dirprod_paths. + cbn. apply dirprod_paths. * cbn. etrans. 2 : { apply maponpaths. apply (disp_binprod_transportf_pr1 (DA ⊠⊠ DB) DC). } etrans. 2 : { apply (disp_binprod_transportf_pr1 DA DB). } apply pathsinv0. apply transportf_set. apply A. * cbn. etrans. 2 : { apply maponpaths. apply (disp_binprod_transportf_pr1 (DA ⊠⊠ DB) DC). } etrans. 2 : { apply (disp_binprod_transportf_pr2 DA DB). } apply pathsinv0. apply transportf_set. apply B. + cbn. etrans. 2 : { apply (disp_binprod_transportf_pr2 (DA ⊠⊠ DB) DC). } apply pathsinv0. apply transportf_set. apply C. - intros. cbn. apply dirprod_paths. + cbn. apply dirprod_paths. * cbn. etrans. 2 : { apply maponpaths. apply (disp_binprod_transportf_pr1 (DA ⊠⊠ DB) DC). } etrans. 2 : { apply (disp_binprod_transportf_pr1 DA DB). } apply pathsinv0. apply transportf_set. apply A. * cbn. etrans. 2 : { apply maponpaths. apply (disp_binprod_transportf_pr1 (DA ⊠⊠ DB) DC). } etrans. 2 : { apply (disp_binprod_transportf_pr2 DA DB). } apply pathsinv0. apply transportf_set. apply B. + cbn. etrans. 2 : { apply (disp_binprod_transportf_pr2 (DA ⊠⊠ DB) DC). } apply pathsinv0. apply transportf_set. apply C. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.catiso UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions