Lemma disp_binprod_axioms : disp_cat_axioms _ disp_binprod_data. 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.
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.