Definition core_indexed_cat_data : indexed_cat_data C. Proof. use make_indexed_cat_data. - exact (λ x, univalent_core (Φ x)). - exact (λ x y f, core_functor (Φ $ f)). - intros x. use make_nat_trans. + exact (λ xx, indexed_cat_id_z_iso Φ xx). + intros xx yy ff ; cbn. use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ]. cbn. apply (nat_trans_ax (indexed_cat_id Φ x)). - intros x y z f g. use make_nat_trans. + exact (λ xx, indexed_cat_comp_z_iso Φ f g xx). + intros xx yy ff ; cbn. use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ]. cbn. apply (nat_trans_ax (indexed_cat_comp Φ f g)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.