Proposition is_discrete_cat_to_bicat : is_discrete_bicat cat_to_bicat. Proof. repeat split. - exact is_univalent_2_1_cat_to_bicat. - exact locally_groupoid_cat_to_bicat. - exact isaprop_2cells_cat_to_bicat. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Discreteness. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.