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