Proposition is_univalent_cat_of_setcategory : is_univalent cat_of_setcategory. Proof. intros C D. use weqhomot. - exact (weqfibtototal _ _ is_catiso_weq_is_z_isomorphism ∘ catiso_is_path_cat _ _ ∘ path_setcategory _ _)%weq. - intro p. induction p. use z_iso_eq. use subtypePath. { intro. apply isaprop_is_functor. apply homset_property. } apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Section FromIso. End FromIso.