Proposition core_indexed_cat_laws : indexed_cat_laws core_indexed_cat_data. Proof. repeat split. - intros x y f xx ; cbn in *. use subtypePath. { intro. apply isaprop_is_z_isomorphism. } cbn. refine (indexed_cat_lunitor Φ f xx @ _). apply maponpaths. refine (_ @ !(@idtoiso_core (Φ y) _ _ _)). apply idpath. - intros x y f xx ; cbn in *. use subtypePath. { intro. apply isaprop_is_z_isomorphism. } cbn. refine (indexed_cat_runitor Φ f xx @ _). apply maponpaths. refine (_ @ !(@idtoiso_core (Φ y) _ _ _)). apply idpath. - intros w x y z f g h ww ; cbn in *. use subtypePath. { intro. apply isaprop_is_z_isomorphism. } cbn. refine (_ @ indexed_cat_lassociator Φ f g h ww). apply maponpaths. refine (@idtoiso_core (Φ z) _ _ _ @ _). apply idpath. Qed.
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.