Proposition locally_groupoid_cat_to_bicat : locally_groupoid cat_to_bicat. Proof. intros x y f g α. refine (!α ,, _ ,, _). - apply isaprop_2cells_cat_to_bicat. - apply isaprop_2cells_cat_to_bicat. Defined.
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.