proposition: Lemma is_univalent_indexed_set_cat : is_univalent indexed_set_cat.
proof: Proof. intros a b. use weqhomot. - exact (indexed_set_cat_iso_weq _ _ ∘ indexed_set_cat_id_iso_weq _ _ ∘ invweq (weqfunextsec _ _ _)). - intro e. induction e. now apply z_iso_eq. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits