Definition disp_depprod_disp_prebicat_ops : disp_prebicat_ops (disp_depprod_cat_data,, disp_depprod_disp_2cell_struct). Proof. repeat split. - exact (λ a b f aa bb ff i, disp_id2 (ff i)). - exact (λ a b f aa bb ff i, disp_lunitor (ff i)). - exact (λ a b f aa bb ff i, disp_runitor (ff i)). - exact (λ a b f aa bb ff i, disp_linvunitor (ff i)). - exact (λ a b f aa bb ff i, disp_rinvunitor (ff i)). - exact (λ a b c d f g h aa bb cc dd ff gg hh i, disp_rassociator (ff i) (gg i) (hh i)). - exact (λ a b c d f g h aa bb cc dd ff gg hh i, disp_lassociator (ff i) (gg i) (hh i)). - exact (λ a b f g h x y aa bb ff gg hh xx yy i, xx i •• yy i). - exact (λ a b c f g1 g2 x aa bb cc ff gg1 gg2 xx i, ff i ◃◃ xx i). - exact (λ a b c f1 f2 g x aa bb cc ff1 ff2 gg xx i, xx i ▹▹ gg i). Defined.
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.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.