fact: Definition indexed_cat (C : category) : UU := ∑ (F : indexed_cat_data C), indexed_cat_isos F × indexed_cat_laws F.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations