Proposition is_univalent_2_1_cat_to_bicat : is_univalent_2_1 cat_to_bicat. Proof. intros x y f g. use isweqimplimpl. - exact (λ p, pr1 p). - apply homset_property. - use isaproptotal2. + intro. apply isaprop_is_invertible_2cell. + intros. apply homset_property. 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.