Definition fiber_hset_twosided_disp_cat {C₁ C₂ : category} {D : twosided_disp_cat C₁ C₂} (HD : discrete_twosided_disp_cat D) (x : C₁) (y : C₂) : hSet. Proof. use make_hSet. - exact (D x y). - exact (isaset_discrete_twosided_cat_ob HD x y). 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.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration.