Definition section_disp_bicat_data {B : bicat} (D : disp_bicat B) : UU := ∑ (s_ob : ∏ (x : B), D x) (s_mor : ∏ (x y : B) (f : x --> y), s_ob x -->[ f ] s_ob y), (∏ (x y : B) (f g : x --> y) (τ : f ==> g), s_mor _ _ f ==>[ τ ] s_mor _ _ g) × (∏ (x : B), disp_invertible_2cell (id2_invertible_2cell _) (id_disp _) (s_mor _ _ (id₁ x))) × (∏ (x y z : B) (f : x --> y) (g : y --> z), disp_invertible_2cell (id2_invertible_2cell _) (s_mor _ _ f ;; s_mor _ _ g) (s_mor _ _ (f · g))).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. 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.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.