fact: Definition indexed_cat_on_ob {C : category} (F : indexed_cat_data C) (x : C) : univalent_category := pr1 F x.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations