Proposition is_univalent_2_0_cat_to_bicat (HC : is_univalent C) : is_univalent_2_0 cat_to_bicat. Proof. use locally_posetal_bicat_univalent_2_0. - exact is_discrete_cat_to_bicat. - refine (transportf is_univalent _ HC). use category_eq. apply idpath. 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.