Definition rep_internal_sfib : UU := (∏ (x : B), street_fib (post_comp x p)) × (∏ (x y : B) (h : y --> x), preserves_cartesian (post_comp x p) (post_comp y p) (pre_comp e h)).
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.DisplayedCats.StreetFibration. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence.