proposition: Lemma disp_binprod_axioms : disp_cat_axioms _ disp_binprod_data.
proof: Proof. repeat split. - intros [a a'] [b b'] [f f'] [x x'] [y y'] [ff ff']. simpl in *. apply dirprodeq. * simpl in *. etrans. apply id_left_disp. etrans. 2: { apply disp_binprod_transportf_pr1. } apply transportf_paths. apply C. * simpl in *. etrans. apply id_left_disp. etrans. 2: { apply disp_binprod_transportf_pr2. } apply transportf_paths. apply C'. - intros [a a'] [b b'] [f f'] [x x'] [y y'] [ff ff']. simpl in *. apply dirprodeq. * simpl in *. etrans. apply id_right_disp. etrans. 2: { apply disp_binprod_transportf_pr1. } apply transportf_paths. apply C. * simpl in *. etrans. apply id_right_disp. etrans. 2: { apply disp_binprod_transportf_pr2. } apply transportf_paths. apply C'. - intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'] [x x'] [y y'] [z z'] [w w'] [u u'] [v v'] [r r']. simpl in *. apply dirprodeq. * simpl. etrans. apply assoc_disp. etrans. 2: { apply disp_binprod_transportf_pr1. } apply transportf_paths. apply C. * simpl. etrans. apply assoc_disp. etrans. 2: { apply disp_binprod_transportf_pr2. } apply transportf_paths. apply C'. - intros. apply isasetdirprod. * apply D. * apply D'. 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